diff --git a/NEWS b/NEWS index c58454fa5..c427a89b3 100644 --- a/NEWS +++ b/NEWS @@ -1,4 +1,4 @@ -New in spot 2.0.1a (not yet released) +New in spot 2.0.2a (not yet released) Command-line tools: @@ -40,6 +40,10 @@ New in spot 2.0.1a (not yet released) appearing in these three papers: Dwyer et al (FMSP'98), Etessami & Holzmann (Concur'00), Somenzi & Bloem (CAV'00). + * Arguments passed to -x that are not used are now reported as they + might be typos. (This ocurred a couple of times in our + test-suite.) + Library: * The print_hoa() function will now output version 1.1 of the HOA diff --git a/bin/autfilt.cc b/bin/autfilt.cc index cda04b086..404206e68 100644 --- a/bin/autfilt.cc +++ b/bin/autfilt.cc @@ -1031,6 +1031,9 @@ main(int argc, char** argv) hoa_processor processor(post); if (processor.run()) return 2; + + // Diagnose unused -x options + extra_options.report_unused_options(); } catch (const std::runtime_error& e) { diff --git a/bin/dstar2tgba.cc b/bin/dstar2tgba.cc index 97f59be07..b0a3e066b 100644 --- a/bin/dstar2tgba.cc +++ b/bin/dstar2tgba.cc @@ -193,6 +193,9 @@ main(int argc, char** argv) dstar_processor processor(post); if (processor.run()) return 2; + + // Diagnose unused -x options + extra_options.report_unused_options(); } catch (const std::runtime_error& e) { diff --git a/bin/ltl2tgba.cc b/bin/ltl2tgba.cc index 94e69ac80..da84dbb47 100644 --- a/bin/ltl2tgba.cc +++ b/bin/ltl2tgba.cc @@ -168,20 +168,24 @@ main(int argc, char** argv) error(2, 0, "No formula to translate? Run '%s --help' for usage.", program_name); - spot::translator trans(&extra_options); - trans.set_pref(pref | comp | sbacc | unambig); - trans.set_type(type); - trans.set_level(level); - try { + spot::translator trans(&extra_options); + trans.set_pref(pref | comp | sbacc | unambig); + trans.set_type(type); + trans.set_level(level); + trans_processor processor(trans); if (processor.run()) return 2; + + // Diagnose unused -x options + extra_options.report_unused_options(); } catch (const std::runtime_error& e) { error(2, 0, "%s", e.what()); } + return 0; } diff --git a/bin/ltl2tgta.cc b/bin/ltl2tgta.cc index 045c342ea..bc7f07349 100644 --- a/bin/ltl2tgta.cc +++ b/bin/ltl2tgta.cc @@ -230,13 +230,23 @@ main(int argc, char** argv) error(2, 0, "No formula to translate? Run '%s --help' for usage.", program_name); - spot::translator trans(&extra_options); - trans.set_pref(pref | comp | sbacc); - trans.set_type(type); - trans.set_level(level); + try + { + spot::translator trans(&extra_options); + trans.set_pref(pref | comp | sbacc); + trans.set_type(type); + trans.set_level(level); + + trans_processor processor(trans); + if (processor.run()) + return 2; + // Diagnose unused -x options + extra_options.report_unused_options(); + } + catch (const std::runtime_error& e) + { + error(2, 0, "%s", e.what()); + } - trans_processor processor(trans); - if (processor.run()) - return 2; return 0; } diff --git a/spot/misc/optionmap.cc b/spot/misc/optionmap.cc index 0aa7eae57..c092f0fc0 100644 --- a/spot/misc/optionmap.cc +++ b/spot/misc/optionmap.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2008, 2013, 2014, 2015 Laboratoire de Recherche et -// Développement de l'Epita (LRDE). +// Copyright (C) 2008, 2013, 2014, 2015, 2016 Laboratoire de Recherche +// et Développement de l'Epita (LRDE). // Copyright (C) 2005 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. @@ -23,6 +23,7 @@ #include "config.h" #include #include +#include #include #include @@ -69,7 +70,7 @@ namespace spot if (*options != '=') { - options_[name] = (negated ? 0 : 1); + set_(name, !negated); } else if (negated) { @@ -93,8 +94,7 @@ namespace spot while (*options && *options != sep); if (*options != sep) return start - 1; - std::string val(start, options); - options_str_[name] = val; + set_str_(name, std::string(start, options)); if (*options) ++options; } @@ -120,7 +120,7 @@ namespace spot return options; } options = val_end; - options_[name] = val; + set_(name, val); } } } @@ -130,6 +130,7 @@ namespace spot int option_map::get(const char* option, int def) const { + unused_.erase(option); auto it = options_.find(option); return (it == options_.end()) ? def : it->second; } @@ -137,21 +138,28 @@ namespace spot std::string option_map::get_str(const char* option, std::string def) const { + unused_.erase(option); auto it = options_str_.find(option); return (it == options_str_.end()) ? def : it->second; } - int - option_map::operator[](const char* option) const + void option_map::set_(const std::string& option, int val) { - return get(option); + options_[option] = val; + unused_.insert(option); + } + + void option_map::set_str_(const std::string& option, const std::string& val) + { + options_str_[option] = val; + unused_.insert(option); } int option_map::set(const char* option, int val, int def) { int old = get(option, def); - options_[option] = val; + set_(option, val); return old; } @@ -159,7 +167,7 @@ namespace spot option_map::set_str(const char* option, std::string val, std::string def) { std::string old = get_str(option, def); - options_str_[option] = val; + set_str_(option, val); return old; } @@ -168,11 +176,20 @@ namespace spot { options_ = o.options_; options_str_ = o.options_str_; + unused_ = o.unused_; + } + + int + option_map::operator[](const char* option) const + { + unused_.erase(option); + return get(option); } int& option_map::operator[](const char* option) { + unused_.erase(option); return options_[option]; } @@ -185,4 +202,24 @@ namespace spot os << '"' << p.first << "\" = \"" << p.second << "\"\n"; return os; } + + void option_map::report_unused_options() const + { + auto s = unused_.size(); + if (s == 0U) + return; + std::ostringstream os; + if (s == 1U) + { + os << "option '" << *unused_.begin() + << "' was not used (possible typo?)"; + } + else + { + os << "the following options where not used (possible typos?):"; + for (auto opt: unused_) + os << "\n\t- '" << opt << '\''; + } + throw std::runtime_error(os.str()); + } } diff --git a/spot/misc/optionmap.hh b/spot/misc/optionmap.hh index 7e4114b84..18a220515 100644 --- a/spot/misc/optionmap.hh +++ b/spot/misc/optionmap.hh @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2013, 2015 Laboratoire de Recherche et Developpement de -// l'Epita (LRDE) +// Copyright (C) 2013, 2015, 2016 Laboratoire de Recherche et +// Developpement de l'Epita (LRDE) // Copyright (C) 2005 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. @@ -26,6 +26,7 @@ #include #include #include +#include namespace spot { @@ -86,6 +87,9 @@ namespace spot std::string set_str(const char* option, std::string val, std::string def = {}); + /// \brief Raise a runtime_error if some option haven't been used. + void report_unused_options() const; + /// Acquire all the settings of \a o. void set(const option_map& o); @@ -99,5 +103,12 @@ namespace spot private: std::map options_; std::map options_str_; + // Unused values. Initially they will store all options, and they + // will be erased as they are used. The resulting set can be used + // for diagnosing errors. + mutable std::set unused_; + + void set_(const std::string&, int val); + void set_str_(const std::string&, const std::string& val); }; } diff --git a/tests/Makefile.am b/tests/Makefile.am index 858106b57..be1649ff5 100644 --- a/tests/Makefile.am +++ b/tests/Makefile.am @@ -189,6 +189,7 @@ TESTS_kripke = \ TESTS_misc = \ core/bitvect.test \ core/intvcomp.test \ + core/minusx.test \ core/trival.test TESTS_twa = \ diff --git a/tests/core/ltlcross2.test b/tests/core/ltlcross2.test index 93ccde10b..786ed65b2 100755 --- a/tests/core/ltlcross2.test +++ b/tests/core/ltlcross2.test @@ -1,7 +1,7 @@ #!/bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2012, 2013, 2014, 2015 Laboratoire de Recherche et -# Développement de l'Epita (LRDE). +# Copyright (C) 2012, 2013, 2014, 2015, 2016 Laboratoire de Recherche +# et Développement de l'Epita (LRDE). # # This file is part of Spot, a model checking library. # @@ -38,7 +38,7 @@ ltlcross --products=3 --timeout=60 \ "$ltl2tgba --lbtt -x comp-susp,!skel-wdba --small %f >%T" \ "$ltl2tgba --lbtt -x comp-susp,early-susp --small %f >%T" \ "$ltl2tgba --lbtt -x comp-susp,!skel-wdba,!skel-simul --small %f >%T" \ -"$ltl2tgba --spin --ba -x degen-skip=0 %f >%N" \ +"$ltl2tgba --spin --ba -x degen-lskip=0 %f >%N" \ "$ltl2tgba --lbtt --ba --high %f > %T" \ "$ltl2tgba --spin=6 --ba --medium %f > %N" \ "$ltl2tgba --hoa -BDC %f > %H" \ diff --git a/tests/core/minusx.test b/tests/core/minusx.test new file mode 100755 index 000000000..8d16036bd --- /dev/null +++ b/tests/core/minusx.test @@ -0,0 +1,30 @@ +#!/bin/sh +# -*- coding: utf-8 -*- +# Copyright (C) 2016 Laboratoire de Recherche et Développement de +# l'Epita (LRDE). +# +# This file is part of Spot, a model checking library. +# +# Spot is free software; you can redistribute it and/or modify it +# under the terms of the GNU General Public License as published by +# the Free Software Foundation; either version 3 of the License, or +# (at your option) any later version. +# +# Spot is distributed in the hope that it will be useful, but WITHOUT +# ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +# or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +# License for more details. +# +# You should have received a copy of the GNU General Public License +# along with this program. If not, see . + +. ./defs +set -e + +# make sure option -x reports unknown arguments +ltl2tgba -F- -x foo error && exit 1 +grep "ltl2tgba: option 'foo' was not used" error +ltl2tgba -F- -x ba-simul,foo,bar error && exit 1 +grep -v 'ba-simul' error +grep -- "- 'foo'" error +grep -- "- 'bar'" error diff --git a/tests/core/readsave.test b/tests/core/readsave.test index facfe80db..2e5cd032d 100755 --- a/tests/core/readsave.test +++ b/tests/core/readsave.test @@ -278,7 +278,7 @@ autfilt --merge -Hm input --name="%E->%e edges, %T->%t transitions" > output diff output expected -cat < tmp.hoa +cat < tmp.hoa a U b false !b && Xb && GFa