Commit 79a62ae1 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

ltlfilt: introduce --suspendable

* bin/ltlfilt.cc: Add the option.
* tests/core/ltlfilt.test: Use it.
* NEWS: Mention it.
parent d5ffdb60
New in spot 2.6.0.dev (not yet released) New in spot 2.6.0.dev (not yet released)
Nothing yet. Command-line tools:
- "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)
......
...@@ -100,6 +100,7 @@ enum { ...@@ -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[] = ...@@ -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*) ...@@ -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 ...@@ -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)
......
Supports Markdown
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