Commit 4c0500a8 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz

autfilt: add --stutter-invariant

* bin/autfilt.cc: Implement the option.
* NEWS: Mention it.
* tests/core/readsave.test, tests/core/stutter-tgba.test: Add some
tests.
parent 5a2bc9f9
......@@ -23,6 +23,9 @@ New in spot 2.0.3a (not yet released)
* autfilt can filter automata by count of nondeterministsic states
with --nondet-states=RANGE.
* autfilt can filter automata representing stutter-invariant
properties with --is-stutter-invariant.
* autfilt has two new options to highlight non-determinism:
--highlight-nondet-states=NUM and --highlight-nondet-states=NUM
where NUM is a color number. Additionally --highlight-nondet=NUM
......
......@@ -100,8 +100,9 @@ enum {
OPT_IS_COMPLETE,
OPT_IS_DETERMINISTIC,
OPT_IS_EMPTY,
OPT_IS_UNAMBIGUOUS,
OPT_IS_STUTTER_INVARIANT,
OPT_IS_TERMINAL,
OPT_IS_UNAMBIGUOUS,
OPT_IS_WEAK,
OPT_IS_INHERENTLY_WEAK,
OPT_KEEP_STATES,
......@@ -163,10 +164,12 @@ static const argp_option options[] =
"keep deterministic automata", 0 },
{ "is-empty", OPT_IS_EMPTY, nullptr, 0,
"keep automata with an empty language", 0 },
{ "is-unambiguous", OPT_IS_UNAMBIGUOUS, nullptr, 0,
"keep only unambiguous automata", 0 },
{ "is-stutter-invariant", OPT_IS_STUTTER_INVARIANT, nullptr, 0,
"keep automata representing stutter-invariant properties", 0 },
{ "is-terminal", OPT_IS_TERMINAL, nullptr, 0,
"keep only terminal automata", 0 },
{ "is-unambiguous", OPT_IS_UNAMBIGUOUS, nullptr, 0,
"keep only unambiguous automata", 0 },
{ "is-weak", OPT_IS_WEAK, nullptr, 0,
"keep only weak automata", 0 },
{ "is-inherently-weak", OPT_IS_INHERENTLY_WEAK, nullptr, 0,
......@@ -365,6 +368,7 @@ static bool opt_is_unambiguous = false;
static bool opt_is_terminal = false;
static bool opt_is_weak = false;
static bool opt_is_inherently_weak = false;
static bool opt_is_stutter_invariant = false;
static bool opt_invert = false;
static range opt_states = { 0, std::numeric_limits<int>::max() };
static range opt_edges = { 0, std::numeric_limits<int>::max() };
......@@ -596,12 +600,15 @@ parse_opt(int key, char* arg, struct argp_state*)
case OPT_IS_INHERENTLY_WEAK:
opt_is_inherently_weak = true;
break;
case OPT_IS_UNAMBIGUOUS:
opt_is_unambiguous = true;
case OPT_IS_STUTTER_INVARIANT:
opt_is_stutter_invariant = true;
break;
case OPT_IS_TERMINAL:
opt_is_terminal = true;
break;
case OPT_IS_UNAMBIGUOUS:
opt_is_unambiguous = true;
break;
case OPT_IS_WEAK:
opt_is_weak = true;
break;
......@@ -944,6 +951,12 @@ namespace
matched = false;
break;
}
if (opt_is_stutter_invariant)
{
check_stutter_invariance(aut);
assert(aut->prop_stutter_invariant().is_known());
matched &= aut->prop_stutter_invariant().is_true();
}
// Drop or keep matched automata depending on the --invert option
if (matched == opt_invert)
......
......@@ -930,6 +930,7 @@ State: 1
EOF
test `autfilt -c --is-inherently-weak input7` = 1
test `autfilt -c --is-weak input7` = 0
test `autfilt -c --is-stutter-invariant input7` = 1
autfilt --check input7 -H >output7
cat >expected7 <<EOF
HOA: v1
......
......@@ -86,6 +86,7 @@ run 0 $ltl2tgba -H1.1 --check=stutter 'F(a & X(a & b))' > input.2
grep '!stutter-invariant' input.2
# HOA v1 has no name, so we use "stutter-sensitive"
run 0 $autfilt --check=stutter input > input.2
test `autfilt -c -v --is-stutter-invariant input` = 1
grep stutter-sensitive input.2
$ltl2tgba 'F(a & X(!a & Gb))' > input
......@@ -93,6 +94,7 @@ grep stutter-invariant input && exit 1
grep deterministic input && exit 1
# This will involve a complementation
run 0 $autfilt --check=stutter input > input.2
test `autfilt -c --is-stutter-invariant input` = 1
grep ' stutter-invariant' input.2
$ltl2tgba 'F(a & X(a & Gb))' > input
......@@ -100,5 +102,6 @@ grep stutter input && exit 1
grep deterministic input && exit 1
# This will involve a complementation
run 0 $autfilt -H1.1 --check=stutter input > input.2
test `autfilt -c --is-stutter-invariant input` = 0
grep '!deterministic' input.2
grep '!stutter-invariant' input.2
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment