ltlfilt: support --pi1 --sigma1 --delta1 --pi2 --sigma2

* bin/ltlfilt.cc: Implement those option.
* tests/core/hierarchy.test: Add a quick test.
* NEWS: Mention it.

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.
 

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<int>::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))
         {

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 |