From e80b443bc83b536e46dc5a1b9b7f4fdab4597cbc Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 22 Jun 2016 21:15:15 +0200 Subject: [PATCH] sat-minimize: check for unused options Fixes #179. * spot/twaalgos/dtwasat.cc: Add the check. * tests/core/minusx.test: Test it. * NEWS: Mention it. --- NEWS | 7 ++++--- spot/twaalgos/dtwasat.cc | 6 +++++- tests/core/minusx.test | 6 ++++++ 3 files changed, 15 insertions(+), 4 deletions(-) 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