diff --git a/NEWS b/NEWS index c427a89b3..007586a24 100644 --- a/NEWS +++ b/NEWS @@ -40,9 +40,10 @@ New in spot 2.0.2a (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.) + * Arguments passed to -x (in ltl2tgba, ltl2tgta, autfilt, dstar2tgba) + that are not used are now reported as they might be typos. + This ocurred a couple of times in our test-suite. A similar + check is done the the arguments of autfilt --sat-minimize=... Library: diff --git a/spot/twaalgos/dtwasat.cc b/spot/twaalgos/dtwasat.cc index 82cd20e86..7c495f97a 100644 --- a/spot/twaalgos/dtwasat.cc +++ b/spot/twaalgos/dtwasat.cc @@ -1296,6 +1296,10 @@ namespace spot int max_states = om.get("max-states", -1); auto accstr = om.get_str("acc"); 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... bool user_supplied_acc = false; @@ -1327,7 +1331,7 @@ namespace spot target_is_buchi = acccond.is_buchi(); } - if (int preproc = om.get("preproc", 3)) + if (preproc) { postprocessor post; auto sba = (state_based && a->prop_state_acc()) ? diff --git a/tests/core/minusx.test b/tests/core/minusx.test index 8d16036bd..41829a2be 100755 --- a/tests/core/minusx.test +++ b/tests/core/minusx.test @@ -28,3 +28,9 @@ ltl2tgba -F- -x ba-simul,foo,bar error && exit 1 grep -v 'ba-simul' error grep -- "- 'foo'" 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