alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

sat-minimize: check for unused options

Browse source 
Fixes #179.

* spot/twaalgos/dtwasat.cc: Add the check.
* tests/core/minusx.test: Test it.
* NEWS: Mention it.
This commit is contained in:
Alexandre Duret-Lutz 2016-06-22 21:15:15 +02:00
parent e419150c30
commit e80b443bc8
3 changed files with 15 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

7
NEWS
View file

@ -40,9 +40,10 @@ New in spot 2.0.2a (not yet released)
appearing in these three papers: Dwyer et al (FMSP'98), Etessami & appearing in these three papers: Dwyer et al (FMSP'98), Etessami &
Holzmann (Concur'00), Somenzi & Bloem (CAV'00). Holzmann (Concur'00), Somenzi & Bloem (CAV'00).
* Arguments passed to -x that are not used are now reported as they * Arguments passed to -x (in ltl2tgba, ltl2tgta, autfilt, dstar2tgba)
might be typos. (This ocurred a couple of times in our that are not used are now reported as they might be typos.
test-suite.) This ocurred a couple of times in our test-suite. A similar
check is done the the arguments of autfilt --sat-minimize=...
Library: Library:

6
spot/twaalgos/dtwasat.cc
View file

@ -1296,6 +1296,10 @@ namespace spot
int max_states = om.get("max-states", -1); int max_states = om.get("max-states", -1);
auto accstr = om.get_str("acc"); auto accstr = om.get_str("acc");
bool colored = om.get("colored", 0); bool colored = om.get("colored", 0);
int preproc = om.get("preproc", 3);
// No more om.get() below this.
om.report_unused_options();
// Assume we are going to use the input automaton acceptance... // Assume we are going to use the input automaton acceptance...
bool user_supplied_acc = false; bool user_supplied_acc = false;
@ -1327,7 +1331,7 @@ namespace spot
target_is_buchi = acccond.is_buchi(); target_is_buchi = acccond.is_buchi();
} }
if (int preproc = om.get("preproc", 3)) if (preproc)
{ {
postprocessor post; postprocessor post;
auto sba = (state_based && a->prop_state_acc()) ? auto sba = (state_based && a->prop_state_acc()) ?

6
tests/core/minusx.test
View file

@ -28,3 +28,9 @@ ltl2tgba -F- -x ba-simul,foo,bar </dev/null 2>error && exit 1
grep -v 'ba-simul' error grep -v 'ba-simul' error
grep -- "- 'foo'" error grep -- "- 'foo'" error
grep -- "- 'bar'" error grep -- "- 'bar'" error
# Likewise for --sat-minimise
ltl2tgba -f FGa | autfilt -D |
autfilt --sat-minimize='acc="co-Buchi",other' 2>error && exit 1
grep "autfilt: option 'other' was not used" error