diff --git a/NEWS b/NEWS index 700942091..5f09664f9 100644 --- a/NEWS +++ b/NEWS @@ -6,6 +6,9 @@ New in spot 2.12.0.dev (not yet released) edges leading to dead-ends. See the description of restrict_dead_end_edges_here() below. + - ltlfilt learned --pi1, --sigma1, --delta1, --pi2, --sigma2, and + --delta2 to filter according to classes Π₁,Σ₁,Δ₁,Π₂,Σ₂, and Δ₂. + Library: - restrict_dead_end_edges_here() can reduce non-determinism (but @@ -112,7 +115,7 @@ New in spot 2.12 (2024-05-16) - EXPL: explicit splitting of each state as before - SEMISYM: The outgoing transition of each state are encoded as a bdd; Works better for larger number of input APs - - FULLYSYM: The automaton is first translated into a + - FULLYSYM: The automaton is first translated into a fully symbolic version, then split. - AUTO: Let the heuristic decide what to do. diff --git a/bin/ltlfilt.cc b/bin/ltlfilt.cc index 0403ea76c..f56074d78 100644 --- a/bin/ltlfilt.cc +++ b/bin/ltlfilt.cc @@ -74,6 +74,8 @@ enum { OPT_BSIZE_MAX, OPT_BSIZE_MIN, OPT_DEFINE, + OPT_DELTA1, + OPT_DELTA2, OPT_DROP_ERRORS, OPT_EQUIVALENT_TO, OPT_EXCLUSIVE_AP, @@ -89,6 +91,7 @@ enum { OPT_NNF, OPT_OBLIGATION, OPT_PERSISTENCE, + OPT_PI2, OPT_RECURRENCE, OPT_REJECT_WORD, OPT_RELABEL, @@ -97,6 +100,7 @@ enum { OPT_REMOVE_WM, OPT_REMOVE_X, OPT_SAFETY, + OPT_SIGMA2, OPT_SIZE, OPT_SIZE_MAX, OPT_SIZE_MIN, @@ -184,15 +188,22 @@ static const argp_option options[] = { "suspendable", OPT_SUSPENDABLE, nullptr, 0, "synonym for --universal --eventual", 0 }, { "syntactic-safety", OPT_SYNTACTIC_SAFETY, nullptr, 0, - "match syntactic-safety formulas", 0 }, + "match syntactic-safety (a.k.a. Π₁) formulas", 0 }, + { "pi1", 0, nullptr, OPTION_ALIAS, nullptr, 0 }, { "syntactic-guarantee", OPT_SYNTACTIC_GUARANTEE, nullptr, 0, - "match syntactic-guarantee formulas", 0 }, + "match syntactic-guarantee (a.k.a. Σ₁) formulas", 0 }, + { "sigma1", 0, nullptr, OPTION_ALIAS, nullptr, 0 }, { "syntactic-obligation", OPT_SYNTACTIC_OBLIGATION, nullptr, 0, "match syntactic-obligation formulas", 0 }, + { "delta1", OPT_DELTA1, nullptr, 0, + "match Δ₁ formulas", 0 }, { "syntactic-recurrence", OPT_SYNTACTIC_RECURRENCE, nullptr, 0, "match syntactic-recurrence formulas", 0 }, + { "pi2", OPT_PI2, nullptr, 0, "match Π₂ formulas", 0 }, { "syntactic-persistence", OPT_SYNTACTIC_PERSISTENCE, nullptr, 0, "match syntactic-persistence formulas", 0 }, + { "sigma2", OPT_SIGMA2, nullptr, 0, "match Σ₂ formulas", 0 }, + { "delta2", OPT_DELTA2, nullptr, 0, "match Δ₂ formulas", 0 }, { "syntactic-stutter-invariant", OPT_SYNTACTIC_SI, nullptr, 0, "match stutter-invariant formulas syntactically (LTL-X or siPSL)", 0 }, { "nox", 0, nullptr, OPTION_ALIAS, nullptr, 0 }, @@ -312,6 +323,10 @@ static bool syntactic_guarantee = false; static bool syntactic_obligation = false; static bool syntactic_recurrence = false; static bool syntactic_persistence = false; +static bool delta1 = false; +static bool delta2 = false; +static bool sigma2 = false; +static bool pi2 = false; static bool syntactic_si = false; static bool safety = false; static bool guarantee = false; @@ -441,6 +456,12 @@ parse_opt(int key, char* arg, struct argp_state*) case OPT_DEFINE: opt->output_define.reset(new output_file(arg ? arg : "-")); break; + case OPT_DELTA1: + delta1 = true; + break; + case OPT_DELTA2: + delta2 = true; + break; case OPT_DROP_ERRORS: error_style = drop_errors; break; @@ -501,6 +522,9 @@ parse_opt(int key, char* arg, struct argp_state*) case OPT_OBLIGATION: obligation = true; break; + case OPT_PI2: + pi2 = true; + break; case OPT_PERSISTENCE: persistence = true; break; @@ -564,6 +588,9 @@ parse_opt(int key, char* arg, struct argp_state*) case OPT_AP_N: ap_n = parse_range(arg, 0, std::numeric_limits::max()); break; + case OPT_SIGMA2: + sigma2 = true; + break; case OPT_SUSPENDABLE: universal = true; eventual = true; @@ -745,8 +772,12 @@ namespace matched &= !syntactic_safety || f.is_syntactic_safety(); matched &= !syntactic_guarantee || f.is_syntactic_guarantee(); matched &= !syntactic_obligation || f.is_syntactic_obligation(); + matched &= !delta1 || f.is_delta1(); matched &= !syntactic_recurrence || f.is_syntactic_recurrence(); + matched &= !pi2 || f.is_pi2(); matched &= !syntactic_persistence || f.is_syntactic_persistence(); + matched &= !sigma2 || f.is_sigma2(); + matched &= !delta2 || f.is_delta2(); matched &= !syntactic_si || f.is_syntactic_stutter_invariant(); if (matched && (ap_n.min > 0 || ap_n.max >= 0)) { diff --git a/tests/core/hierarchy.test b/tests/core/hierarchy.test index 330b49070..2f7089332 100755 --- a/tests/core/hierarchy.test +++ b/tests/core/hierarchy.test @@ -21,16 +21,22 @@ set -e +test 11 -eq `genltl --dac | ltlfilt --pi1 -c` test 11 -eq `genltl --dac | ltlfilt --syntactic-safety -c` test 37 -eq `genltl --dac | ltlfilt --safety -c` test 'Fp0' = `genltl --dac | ltlfilt --syntactic-guarantee` test 'Fp0' = `genltl --dac | ltlfilt --guarantee` +test 'Fp0' = `genltl --dac | ltlfilt --sigma1` +test 23 -eq `genltl --dac | ltlfilt --delta1 -c` test 25 -eq `genltl --dac | ltlfilt --syntactic-obligation -c` test 40 -eq `genltl --dac | ltlfilt --obligation -c` +test 42 -eq `genltl --dac | ltlfilt --pi2 -c` test 47 -eq `genltl --dac | ltlfilt --syntactic-recurrence -c` test 52 -eq `genltl --dac | ltlfilt --recurrence -c` +test 29 -eq `genltl --dac | ltlfilt --sigma2 -c` test 29 -eq `genltl --dac | ltlfilt --syntactic-persistence -c` test 41 -eq `genltl --dac | ltlfilt --persistence -c` +test 48 -eq `genltl --dac | ltlfilt --delta2 -c` test 'G!p0 | F(p0 & (!p1 W p2))' = "`genltl --dac | ltlfilt -v --obligation | ltlfilt --persistence`" test 12 -eq `genltl --dac |