genltl: add 4 new families from Müller & Sickert (GandALF'17)

* spot/gen/formulas.cc, spot/gen/formulas.hh, bin/genltl.cc:
Implement them.
* NEWS, bin/man/genltl.x: Document them.
* tests/core/genltl.test: Add some tests.

NEWS

 New in spot 2.4.0.dev (not yet released)
 
-  Nothing yet.
+  Tools:
+
+  - genltl learned to generate 4 new families of formulas, taken
+    from Müller & Sickert's GandALF'17 paper:
+    --ms-example=RANGE     GF(a1&X(a2&X(a3&...)))&F(b1&F(b2&F(b3&...)))
+    --ms-phi-h=RANGE       FG(a|b)|FG(!a|Xb)|FG(a|XXb)|FG(!a|XXXb)|...
+    --ms-phi-r=RANGE       (FGa{n}&GFb{n})|((FGa{n-1}|GFb{n-1})&(...))
+    --ms-phi-s=RANGE       (FGa{n}|GFb{n})&((FGa{n-1}&GFb{n-1})|(...))
 
 New in spot 2.4 (2017-09-06)
 

bin/genltl.cc

@@ -106,6 +106,14 @@ static const argp_option options[] =
     { "kv-psi", gen::LTL_KV_PSI, "RANGE", 0,
       "quadratic formula with doubly exponential DBA", 0 },
     OPT_ALIAS(kr-n2),
+    { "ms-example", gen::LTL_MS_EXAMPLE, "RANGE", 0,
+      "GF(a1&X(a2&X(a3&...)))&F(b1&F(b2&F(b3&...)))", 0 },
+    { "ms-phi-h", gen::LTL_MS_PHI_H, "RANGE", 0,
+      "FG(a|b)|FG(!a|Xb)|FG(a|XXb)|FG(!a|XXXb)|...", 0 },
+    { "ms-phi-r", gen::LTL_MS_PHI_R, "RANGE", 0,
+      "(FGa{n}&GFb{n})|((FGa{n-1}|GFb{n-1})&(...))", 0 },
+    { "ms-phi-s", gen::LTL_MS_PHI_S, "RANGE", 0,
+      "(FGa{n}|GFb{n})&((FGa{n-1}&GFb{n-1})|(...))", 0 },
     { "or-fg", gen::LTL_OR_FG, "RANGE", 0, "FG(p1)|FG(p2)|...|FG(pn)", 0 },
     OPT_ALIAS(ccj-xi),
     { "or-g", gen::LTL_OR_G, "RANGE", 0, "G(p1)|G(p2)|...|G(pn)", 0 },

bin/man/genltl.x

@@ -46,6 +46,10 @@ kv
 O. Kupferman and M. Y. Vardi: From Linear Time to Branching Time.
 ACM Transactions on Computational Logic, 6(2):273-294, 2005.
 .TP
+ms
+D. Müller and S. Sickert: LTL to Deterministic Emerson-Lei Automata.
+Proceedings of GandALF'17.  EPTCS 256.
+.TP
 p
 R. Pelánek: BEEM: benchmarks for explicit model checkers
 Proceedings of Spin'07.  LNCS 4595.

spot/gen/formulas.cc

@@ -41,6 +41,59 @@ namespace spot
   {
     namespace
     {
+      static formula
+      ms_example(const char* a, const char* b, int n)
+      {
+        formula ax = formula::tt();
+        formula fb = formula::tt();
+        for (int i = n; i > 0; --i)
+          {
+            std::ostringstream ans;
+            ans << a << i;
+            ax = And_(formula::ap(ans.str()), X_(ax));
+            ans.str("");
+            ans << b << i;
+            fb = F_(And_(formula::ap(ans.str()), fb));
+          }
+        return And_(G_(F_(ax)), fb);
+      }
+
+      static formula
+      ms_phi_h(const char* a, const char* b, int n)
+      {
+        formula fa = formula::ap(a);
+        formula fb = formula::ap(b);
+        formula out = formula::ff();
+        do
+          {
+            out = Or_(F_(G_(Or_(fa, fb))), out);
+            fa = Not_(fa);
+            fb = X_(fb);
+          }
+        while (n--);
+        return out;
+      }
+
+      static formula
+      ms_phi_rs(const char* a, const char* b, int n, bool r = true)
+      {
+        formula fgan = [=]() {
+          std::ostringstream ans;
+          ans << a << n;
+          return F_(G_(formula::ap(ans.str())));
+        } ();
+        formula gfbn = [=]() {
+          std::ostringstream ans;
+          ans << b << n;
+          return G_(F_(formula::ap(ans.str())));
+        } ();
+        formula top = r ? And_(fgan, gfbn) : Or_(fgan, gfbn);
+        if (n == 0)
+          return top;
+        formula sub = ms_phi_rs(a, b, n - 1, !r);
+        return r ? Or_(sub, top) : And_(sub, top);
+      }
+
       // G(p_0 & XF(p_1 & XF(p_2 & ... XF(p_n))))
       // This is a generalization of eh-pattern=9
       static formula
@@ -1128,6 +1181,14 @@ namespace spot
           return combunop_n("p", n, op::G, false);
         case LTL_OR_GF:
           return GF_n("p", n, false);
+        case LTL_MS_EXAMPLE:
+          return ms_example("a", "b", n);
+        case LTL_MS_PHI_H:
+          return ms_phi_h("a", "b", n);
+        case LTL_MS_PHI_R:
+          return ms_phi_rs("a", "b", n, true);
+        case LTL_MS_PHI_S:
+          return ms_phi_rs("a", "b", n, false);
         case LTL_P_PATTERNS:
           return p_pattern(n);
         case LTL_R_LEFT:
@@ -1186,6 +1247,10 @@ namespace spot
           "kr-n",
           "kr-nlogn",
           "kv-psi",
+          "ms-example",
+          "ms-phi-h",
+          "ms-phi-r",
+          "ms-phi-s",
           "or-fg",
           "or-g",
           "or-gf",
@@ -1241,6 +1306,10 @@ namespace spot
         case LTL_KR_N:
         case LTL_KR_NLOGN:
         case LTL_KV_PSI:
+        case LTL_MS_EXAMPLE:
+        case LTL_MS_PHI_H:
+        case LTL_MS_PHI_R:
+        case LTL_MS_PHI_S:
         case LTL_OR_FG:
         case LTL_OR_G:
         case LTL_OR_GF:

spot/gen/formulas.hh

@@ -160,6 +160,20 @@
 //   series = {Lecture Notes in Computer Science},
 //   publisher = {Springer-Verlag}
 // }
+//
+// @InProceedings{muller.17.gandalf,
+//   author = {David M\"uller and Salomon Sickert},
+//   title = {{LTL} to Deterministic {E}merson-{L}ei Automata},
+//   booktitle = {Proceedings of the 8th International Sumposium on Games,
+//                Automata, Logics and Formal Verification (GandALF'17)},
+//   year = 2017,
+//   publisher = {Springer-Verlag}
+//   series    = {Electronic Proceedings in Theoretical Computer Science},
+//   volume    = {256},
+//   publisher = {Open Publishing Association},
+//   pages     = {180--194},
+//   doi       = {10.4204/EPTCS.256.13}
+// }
 
 namespace spot
 {
@@ -184,6 +198,10 @@ namespace spot
       LTL_KR_N,
       LTL_KR_NLOGN,
       LTL_KV_PSI,
+      LTL_MS_EXAMPLE,
+      LTL_MS_PHI_H,
+      LTL_MS_PHI_R,
+      LTL_MS_PHI_S,
       LTL_OR_FG,
       LTL_OR_G,
       LTL_OR_GF,

tests/core/genltl.test

@@ -134,3 +134,26 @@ diff out exp
 test $(genltl --kr-n2=4 | ltl2tgba --low --stats=%s) -ge 16
 test $(genltl --kr-nlogn=4 | ltl2tgba --low --stats=%s) -ge 16
 test $(genltl --kr-n=4 | ltl2tgba --low --stats=%s) -ge 16
+
+genltl --ms-example=0..4 --ms-phi-r=0..2 --ms-phi-s=0..2 --ms-phi-h=0..4 \
+       --format=%F=%L,%f |
+    ltl2tgba -G -D -F-/2 --stats='%<,%s' > out
+cat >exp<<EOF
+ms-example=0,1
+ms-example=1,2
+ms-example=2,4
+ms-example=3,7
+ms-example=4,12
+ms-phi-r=0,2
+ms-phi-r=1,16
+ms-phi-r=2,25
+ms-phi-s=0,5
+ms-phi-s=1,7
+ms-phi-s=2,1322
+ms-phi-h=0,2
+ms-phi-h=1,4
+ms-phi-h=2,21
+ms-phi-h=3,170
+ms-phi-h=4,1816
+EOF
+diff out exp