genltl: three new families --sejk-{j,k,patterns}

These correspond to the first three blocks of table 1 in S. Sickert,
J. Esparza, S. Jaax, and J. Křetínský: Limit-Deterministic Büchi
Automata for Linear Temporal Logic.  CAV'16.  LNCS 9780.

For #353.

* spot/gen/formulas.cc, spot/gen/formulas.hh, bin/genltl.cc: Implement
the new families.
* tests/core/genltl.test: Test it.
* bin/man/genltl.x, NEWS: Document it.

NEWS

@@ -22,6 +22,12 @@ New in spot 2.5.3.dev  (not yet released)
     product to avoid exceeding the number of supported
     acceptance sets.
 
+  - genltl learned to generate three new families of formulas:
+      --sejk-j=RANGE         (GFa1&...&GFan) -> (GFb1&...&GFbn)
+      --sejk-k=RANGE         (GFa1|FGb1)&...&(GFan|FGbn)
+      --sejk-patterns[=RANGE]   φ₁,φ₂,φ₃ from Sikert et al's [CAV'16]
+                             paper (range should be included in 1..3)
+
   Library:
 
   - spot::twa_graph::merge_states() is a new method that merges states

bin/genltl.cc

@@ -141,6 +141,13 @@ static const argp_option options[] =
     { "sb-patterns", gen::LTL_SB_PATTERNS, "RANGE", OPTION_ARG_OPTIONAL,
       "Somenzi and Bloem [CAV'00] patterns "
       "(range should be included in 1..27)", 0 },
+    { "sejk-j", gen::LTL_SEJK_J, "RANGE", 0,
+      "(GFa1&...&GFan) -> (GFb1&...&GFbn)", 0 },
+    { "sejk-k", gen::LTL_SEJK_K, "RANGE", 0,
+      "(GFa1|FGb1)&...&(GFan|FGbn)", 0 },
+    { "sejk-patterns", gen::LTL_SEJK_PATTERNS, "RANGE", OPTION_ARG_OPTIONAL,
+      "φ₁,φ₂,φ₃ from Sikert et al's [CAV'16] paper "
+      "(range should be included in 1..3)", 0 },
     { "tv-f1", gen::LTL_TV_F1, "RANGE", 0,
       "G(p -> (q | Xq | ... | XX...Xq)", 0 },
     { "tv-f2", gen::LTL_TV_F2, "RANGE", 0,

bin/man/genltl.x

@@ -62,6 +62,11 @@ sb
 F. Somenzi and R. Bloem: Efficient Büchi Automata for LTL Formulae.
 Proceedings of CAV'00.  LNCS 1855.
 .TP
+sejk
+S. Sickert, J. Esparza, S. Jaax, and J. Křetínský: Limit-Deterministic
+Büchi Automata for Linear Temporal Logic.
+Proceedings of CAV'16.  LNCS 9780.
+.TP
 tv
 D. Tabakov and M. Y. Vardi: Optimized Temporal Monitors for SystemC.
 Proceedings of RV'10.  LNCS 6418.

spot/gen/formulas.cc

@@ -1139,6 +1139,41 @@ namespace spot
 
         return res;
       }
+
+      static formula
+      sejk_j(std::string a, std::string b, int n)
+      {
+        return formula::Implies(GF_n(a, n), GF_n(b, n));
+      }
+
+      static formula
+      sejk_k(std::string a, std::string b, int n)
+      {
+        formula result = formula::tt();
+        for (int i = 1; i <= n; ++i)
+          {
+            formula ai = formula::ap(a + std::to_string(i));
+            formula bi = formula::ap(b + std::to_string(i));
+            result = formula::And({result,
+                                   formula::Or({G_(F_(ai)), F_(G_(bi))})});
+          }
+        return result;
+      }
+
+      static formula
+      sejk_pattern(int n)
+      {
+        static const char* formulas[] = {
+          "GF(Fa | Gb | FG(a | Xb))",
+          "FG(Ga | F!b | GF(a & Xb))",
+          "GF(Fa | GXb | FG(a | XXb))",
+        };
+
+        constexpr unsigned max = (sizeof formulas)/(sizeof *formulas);
+        if (n < 1 || (unsigned) n > max)
+          bad_number("sejk-patterns", n, max);
+        return spot::relabel(parse_formula(formulas[n - 1]), Pnn);
+      }
     }
 
     formula ltl_pattern(ltl_pattern_id pattern, int n)
@@ -1222,6 +1257,12 @@ namespace spot
           return ltl_counter("b", "m", n, true);
         case LTL_SB_PATTERNS:
           return sb_pattern(n);
+        case LTL_SEJK_J:
+          return sejk_j("a", "b", n);
+        case LTL_SEJK_K:
+          return sejk_k("a", "b", n);
+        case LTL_SEJK_PATTERNS:
+          return sejk_pattern(n);
         case LTL_TV_F1:
           return tv_f1("p", "q", n);
         case LTL_TV_F2:
@@ -1281,6 +1322,9 @@ namespace spot
           "rv-counter-carry-linear",
           "rv-counter-linear",
           "sb-patterns",
+          "sejk-j",
+          "sejk-k",
+          "sejk-patterns",
           "tv-f1",
           "tv-f2",
           "tv-g1",
@@ -1346,6 +1390,11 @@ namespace spot
           return 0;
         case LTL_SB_PATTERNS:
           return 27;
+        case LTL_SEJK_J:
+        case LTL_SEJK_K:
+          return 0;
+        case LTL_SEJK_PATTERNS:
+          return 3;
         case LTL_TV_F1:
         case LTL_TV_F2:
         case LTL_TV_G1:
@@ -1358,8 +1407,6 @@ namespace spot
           break;
         }
       throw std::runtime_error("unsupported pattern");
-
     }
-
   }
 }

spot/gen/formulas.hh

@@ -174,6 +174,35 @@
 //   pages     = {180--194},
 //   doi       = {10.4204/EPTCS.256.13}
 // }
+//
+// @InProceedings{sickert.16.cav,
+//   author = {Salomon Sickert and Javier Esparza and Stefaan Jaax
+//             and Jan K{\v{r}}et{\'i}nsk{\'y}},
+//   title = {Limit-Deterministic {B\"u}chi Automata for Linear Temporal Logic}
+//   booktitle = {Proceedings of the 28th International Conference on
+//                Computer Aided Verification (CAV'16)},
+//   year = 2016,
+//   publisher = {Springer-Verlag}
+//   series = {Lecture Notes in Computer Science},
+//   volume    = {9780},
+//   pages     = {312--332},
+//   doi       = {10.1007/978-3-319-41540-6_17}
+// }
+//
+// @InProceedings{kretisnky.12.cav,
+//   author       = {Jan K{\v{r}}et{\'i}nsk{\'y} and Javier Esparza},
+//   title        = {Deterministic Automata for the {(F,G)}-Fragment of
+//                   {LTL}},
+//   booktitle    = {24th International Conference on Computer Aided
+//                   Verification (CAV'12)},
+//   year         = 2012,
+//   pages        = {7--22},
+//   doi          = {10.1007/978-3-642-31424-7_7},
+//   url          = {https://doi.org/10.1007/978-3-642-31424-7_7},
+//   isbn         = {978-3-642-31424-7},
+//   publisher    = {Springer},
+// }
+
 
 namespace spot
 {
@@ -215,6 +244,9 @@ namespace spot
       LTL_RV_COUNTER_CARRY_LINEAR,
       LTL_RV_COUNTER_LINEAR,
       LTL_SB_PATTERNS,
+      LTL_SEJK_J,
+      LTL_SEJK_K,
+      LTL_SEJK_PATTERNS,
       LTL_TV_F1,
       LTL_TV_F2,
       LTL_TV_G1,

tests/core/genltl.test

@@ -29,7 +29,8 @@ s/[=[].*/=1/p
 res=`genltl $opts --format="--%F=%L"`
 test "$opts" = "$res"
 
-run 0 genltl --dac=1..5 --eh=1..5 --pos --neg --format="%F:%L %f" >output
+run 0 genltl --dac=1..5 --eh=1..5 --sejk-p --pos --neg \
+             --format="%F:%L %f" >output
 cat >expected <<EOF
 dac-patterns:1 G!p0
 !dac-patterns:1 !G!p0
@@ -51,6 +52,12 @@ eh-patterns:4 F(p0 & XGp1)
 !eh-patterns:4 !F(p0 & XGp1)
 eh-patterns:5 F(p0 & X(p1 & XFp2))
 !eh-patterns:5 !F(p0 & X(p1 & XFp2))
+sejk-patterns:1 GF(Fp0 | Gp1 | FG(p0 | Xp1))
+!sejk-patterns:1 !GF(Fp0 | Gp1 | FG(p0 | Xp1))
+sejk-patterns:2 FG(Gp0 | F!p1 | GF(p0 & Xp1))
+!sejk-patterns:2 !FG(Gp0 | F!p1 | GF(p0 & Xp1))
+sejk-patterns:3 GF(Fp0 | GXp1 | FG(p0 | XXp1))
+!sejk-patterns:3 !GF(Fp0 | GXp1 | FG(p0 | XXp1))
 EOF
 diff expected output
 
@@ -204,3 +211,7 @@ test "`cat err`" = "genltl: no pattern p-patterns=0, supported range is 1..20"
 genltl --sb-patterns=0 2> err && exit 1
 test $? = 2
 test "`cat err`" = "genltl: no pattern sb-patterns=0, supported range is 1..27"
+
+genltl --sejk-patterns=0 2> err && exit 1
+test $? = 2
+test "`cat err`" = "genltl: no pattern sejk-patterns=0, supported range is 1..3"