option_map: Diagnose unused option on request
* spot/misc/optionmap.hh, spot/misc/optionmap.cc (report_unused_options, set_, set_set_): New methods. * bin/autfilt.cc, bin/dstar2tgba.cc, bin/ltl2tgba.cc, bin/ltl2tgta.cc: Call report_unused_options(). * tests/core/ltlcross2.test, tests/core/readsave.test: Fix typos in options. * tests/core/minusx.test: New file. * tests/Makefile.am: Add it. * NEWS: Mention this.
This commit is contained in:
Alexandre Duret-Lutz
parent
f7f353db68
commit
e419150c30
11 changed files with 133 additions and 30 deletions
6
NEWS
6
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
|
||||
|
|
|
|||
|
|
@ -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)
|
||||
{
|
||||
|
|
|
|||
|
|
@ -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)
|
||||
{
|
||||
|
|
|
|||
|
|
@ -168,20 +168,24 @@ main(int argc, char** argv)
|
|||
error(2, 0, "No formula to translate? Run '%s --help' for usage.",
|
||||
program_name);
|
||||
|
||||
try
|
||||
{
|
||||
spot::translator trans(&extra_options);
|
||||
trans.set_pref(pref | comp | sbacc | unambig);
|
||||
trans.set_type(type);
|
||||
trans.set_level(level);
|
||||
|
||||
try
|
||||
{
|
||||
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;
|
||||
}
|
||||
|
|
|
|||
|
|
@ -230,6 +230,8 @@ main(int argc, char** argv)
|
|||
error(2, 0, "No formula to translate? Run '%s --help' for usage.",
|
||||
program_name);
|
||||
|
||||
try
|
||||
{
|
||||
spot::translator trans(&extra_options);
|
||||
trans.set_pref(pref | comp | sbacc);
|
||||
trans.set_type(type);
|
||||
|
|
@ -238,5 +240,13 @@ main(int argc, char** argv)
|
|||
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;
|
||||
}
|
||||
|
|
|
|||
|
|
@ -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 <cstring>
|
||||
#include <iostream>
|
||||
#include <sstream>
|
||||
#include <cstdlib>
|
||||
#include <spot/misc/optionmap.hh>
|
||||
|
||||
|
|
@ -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());
|
||||
}
|
||||
}
|
||||
|
|
|
|||
|
|
@ -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 <string>
|
||||
#include <map>
|
||||
#include <iosfwd>
|
||||
#include <set>
|
||||
|
||||
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<std::string, int> options_;
|
||||
std::map<std::string, std::string> 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<std::string> unused_;
|
||||
|
||||
void set_(const std::string&, int val);
|
||||
void set_str_(const std::string&, const std::string& val);
|
||||
};
|
||||
}
|
||||
|
|
|
|||
|
|
@ -189,6 +189,7 @@ TESTS_kripke = \
|
|||
TESTS_misc = \
|
||||
core/bitvect.test \
|
||||
core/intvcomp.test \
|
||||
core/minusx.test \
|
||||
core/trival.test
|
||||
|
||||
TESTS_twa = \
|
||||
|
|
|
|||
|
|
@ -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" \
|
||||
|
|
|
|||
30
tests/core/minusx.test
Executable file
30
tests/core/minusx.test
Executable file
|
|
@ -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 <http://www.gnu.org/licenses/>.
|
||||
|
||||
. ./defs
|
||||
set -e
|
||||
|
||||
# make sure option -x reports unknown arguments
|
||||
ltl2tgba -F- -x foo </dev/null 2>error && exit 1
|
||||
grep "ltl2tgba: option 'foo' was not used" error
|
||||
ltl2tgba -F- -x ba-simul,foo,bar </dev/null 2>error && exit 1
|
||||
grep -v 'ba-simul' error
|
||||
grep -- "- 'foo'" error
|
||||
grep -- "- 'bar'" error
|
||||
|
|
@ -278,7 +278,7 @@ autfilt --merge -Hm input --name="%E->%e edges, %T->%t transitions" > output
|
|||
diff output expected
|
||||
|
||||
|
||||
cat <<EOF | ltl2tgba -x degen-skip=1 -F- --ba -H > tmp.hoa
|
||||
cat <<EOF | ltl2tgba -x degen-lskip=1 -F- --ba -H > tmp.hoa
|
||||
a U b
|
||||
false
|
||||
!b && Xb && GFa
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue