ltlfilt: introduce --suspendable
* bin/ltlfilt.cc: Add the option. * tests/core/ltlfilt.test: Use it. * NEWS: Mention it.
This commit is contained in:
parent
465536d1fe
commit
4b8910d3f9
3 changed files with 15 additions and 0 deletions
3
NEWS
3
NEWS
|
|
@ -31,6 +31,9 @@ New in spot 2.6.0.dev (not yet released)
|
||||||
with arbitrary acceptance condition into a parity automaton,
|
with arbitrary acceptance condition into a parity automaton,
|
||||||
based on a last-appearance record (LAR) construction.
|
based on a last-appearance record (LAR) construction.
|
||||||
|
|
||||||
|
- "ltlfilt --suspendable" is now a synonym for
|
||||||
|
"ltlfilt --universal --eventual".
|
||||||
|
|
||||||
New in spot 2.6 (2018-07-04)
|
New in spot 2.6 (2018-07-04)
|
||||||
|
|
||||||
Command-line tools:
|
Command-line tools:
|
||||||
|
|
|
||||||
|
|
@ -100,6 +100,7 @@ enum {
|
||||||
OPT_SIZE_MIN,
|
OPT_SIZE_MIN,
|
||||||
OPT_SKIP_ERRORS,
|
OPT_SKIP_ERRORS,
|
||||||
OPT_STUTTER_INSENSITIVE,
|
OPT_STUTTER_INSENSITIVE,
|
||||||
|
OPT_SUSPENDABLE,
|
||||||
OPT_SYNTACTIC_GUARANTEE,
|
OPT_SYNTACTIC_GUARANTEE,
|
||||||
OPT_SYNTACTIC_OBLIGATION,
|
OPT_SYNTACTIC_OBLIGATION,
|
||||||
OPT_SYNTACTIC_PERSISTENCE,
|
OPT_SYNTACTIC_PERSISTENCE,
|
||||||
|
|
@ -167,6 +168,8 @@ static const argp_option options[] =
|
||||||
{ "eventual", OPT_EVENTUAL, nullptr, 0, "match pure eventualities", 0 },
|
{ "eventual", OPT_EVENTUAL, nullptr, 0, "match pure eventualities", 0 },
|
||||||
{ "universal", OPT_UNIVERSAL, nullptr, 0,
|
{ "universal", OPT_UNIVERSAL, nullptr, 0,
|
||||||
"match purely universal formulas", 0 },
|
"match purely universal formulas", 0 },
|
||||||
|
{ "suspendable", OPT_SUSPENDABLE, nullptr, 0,
|
||||||
|
"synonym for --universal --eventual", 0 },
|
||||||
{ "syntactic-safety", OPT_SYNTACTIC_SAFETY, nullptr, 0,
|
{ "syntactic-safety", OPT_SYNTACTIC_SAFETY, nullptr, 0,
|
||||||
"match syntactic-safety formulas", 0 },
|
"match syntactic-safety formulas", 0 },
|
||||||
{ "syntactic-guarantee", OPT_SYNTACTIC_GUARANTEE, nullptr, 0,
|
{ "syntactic-guarantee", OPT_SYNTACTIC_GUARANTEE, nullptr, 0,
|
||||||
|
|
@ -507,6 +510,10 @@ parse_opt(int key, char* arg, struct argp_state*)
|
||||||
case OPT_AP_N:
|
case OPT_AP_N:
|
||||||
ap_n = parse_range(arg, 0, std::numeric_limits<int>::max());
|
ap_n = parse_range(arg, 0, std::numeric_limits<int>::max());
|
||||||
break;
|
break;
|
||||||
|
case OPT_SUSPENDABLE:
|
||||||
|
universal = true;
|
||||||
|
eventual = true;
|
||||||
|
break;
|
||||||
case OPT_SYNTACTIC_SAFETY:
|
case OPT_SYNTACTIC_SAFETY:
|
||||||
syntactic_safety = true;
|
syntactic_safety = true;
|
||||||
break;
|
break;
|
||||||
|
|
|
||||||
|
|
@ -84,6 +84,11 @@ GFa | FGb
|
||||||
F(GFa | Gb)
|
F(GFa | Gb)
|
||||||
EOF
|
EOF
|
||||||
|
|
||||||
|
checkopt --suspendable <<EOF
|
||||||
|
GFa | FGb
|
||||||
|
F(GFa | Gb)
|
||||||
|
EOF
|
||||||
|
|
||||||
checkopt --stutter-invariant <<EOF
|
checkopt --stutter-invariant <<EOF
|
||||||
GFa | FGb
|
GFa | FGb
|
||||||
F(GFa | Gb)
|
F(GFa | Gb)
|
||||||
|
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue