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

autfilt: add --is-very-weak

Browse source 
* bin/autfilt.cc: Implement --is-very-weak.
* tests/core/strength.test: Test it.
* NEWS: Mention it.
This commit is contained in:
Alexandre Duret-Lutz 2016-12-28 08:24:08 +01:00
parent 12f6c8cf10
commit 6a11e149b7
3 changed files with 46 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

2
NEWS
View file

@ -11,6 +11,8 @@ New in spot 2.2.2.dev (Not yet released)
alternating automata, but in any case they should display a alternating automata, but in any case they should display a
diagnostic: if you see a crash, please report it. diagnostic: if you see a crash, please report it.
* autfilt has a new --is-very-weak filter.
Library: Library:
* A twa is required to have at least one state, the initial state. * A twa is required to have at least one state, the initial state.

9
bin/autfilt.cc
View file

@ -110,6 +110,7 @@ enum {
OPT_IS_UNAMBIGUOUS, OPT_IS_UNAMBIGUOUS,
OPT_IS_WEAK, OPT_IS_WEAK,
OPT_IS_INHERENTLY_WEAK, OPT_IS_INHERENTLY_WEAK,
OPT_IS_VERY_WEAK,
OPT_KEEP_STATES, OPT_KEEP_STATES,
OPT_MASK_ACC, OPT_MASK_ACC,
OPT_MERGE, OPT_MERGE,
@ -179,6 +180,8 @@ static const argp_option options[] =
"keep only weak automata", 0 }, "keep only weak automata", 0 },
{ "is-inherently-weak", OPT_IS_INHERENTLY_WEAK, nullptr, 0, { "is-inherently-weak", OPT_IS_INHERENTLY_WEAK, nullptr, 0,
"keep only inherently weak automata", 0 }, "keep only inherently weak automata", 0 },
{ "is-very-weak", OPT_IS_VERY_WEAK, nullptr, 0,
"keep only very-weak automata", 0 },
{ "intersect", OPT_INTERSECT, "FILENAME", 0, { "intersect", OPT_INTERSECT, "FILENAME", 0,
"keep automata whose languages have an non-empty intersection with" "keep automata whose languages have an non-empty intersection with"
" the automaton from FILENAME", 0 }, " the automaton from FILENAME", 0 },
@ -412,6 +415,7 @@ static bool opt_is_unambiguous = false;
static bool opt_is_terminal = false; static bool opt_is_terminal = false;
static bool opt_is_weak = false; static bool opt_is_weak = false;
static bool opt_is_inherently_weak = false; static bool opt_is_inherently_weak = false;
static bool opt_is_very_weak = false;
static bool opt_is_stutter_invariant = false; static bool opt_is_stutter_invariant = false;
static bool opt_invert = false; static bool opt_invert = false;
static range opt_states = { 0, std::numeric_limits<int>::max() }; static range opt_states = { 0, std::numeric_limits<int>::max() };
@ -658,6 +662,9 @@ parse_opt(int key, char* arg, struct argp_state*)
case OPT_IS_INHERENTLY_WEAK: case OPT_IS_INHERENTLY_WEAK:
opt_is_inherently_weak = true; opt_is_inherently_weak = true;
break; break;
case OPT_IS_VERY_WEAK:
opt_is_very_weak = true;
break;
case OPT_IS_STUTTER_INVARIANT: case OPT_IS_STUTTER_INVARIANT:
opt_is_stutter_invariant = true; opt_is_stutter_invariant = true;
break; break;
@ -1061,6 +1068,8 @@ namespace
matched &= is_unambiguous(aut); matched &= is_unambiguous(aut);
if (opt_is_terminal) if (opt_is_terminal)
matched &= is_terminal_automaton(aut); matched &= is_terminal_automaton(aut);
else if (opt_is_very_weak)
matched &= is_very_weak_automaton(aut);
else if (opt_is_weak) else if (opt_is_weak)
matched &= is_weak_automaton(aut); matched &= is_weak_automaton(aut);
else if (opt_is_inherently_weak) else if (opt_is_inherently_weak)

35
tests/core/strength.test
View file

@ -590,6 +590,41 @@ EOF
diff out expected diff out expected
autfilt -q expected autfilt -q expected
autfilt --is-very-weak in >out
cat >expected <<EOF
HOA: v1
name: "a U b"
States: 2
Start: 1
AP: 2 "a" "b"
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels state-acc deterministic
properties: very-weak
--BODY--
State: 0 {0}
[t] 0
State: 1
[1] 0
[0&!1] 1
--END--
HOA: v1
States: 2
Start: 1
AP: 1 "a"
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels state-acc colored
properties: deterministic very-weak
--BODY--
State: 0 {0}
[t] 1
State: 1 {0}
[!0] 1
--END--
EOF
diff out expected
cat >input <<EOF cat >input <<EOF
/* This Büchi automaton is not terminal, because of the /* This Büchi automaton is not terminal, because of the