genltl: add --gxf-and and --fxg-or

As suggested in #263.

* spot/gen/formulas.cc, spot/gen/formulas.hh, bin/genltl.cc: Implement
these options.
* tests/core/genltl.test: Use them.
* NEWS: Mention them.

NEWS

@@ -21,6 +21,13 @@ New in spot 2.3.5.dev (not yet released)
     transforming automata (in the same way as we have ltlcross for
     LTL translators).
 
+  - genltl learned two generate to new families of formulas:
+      --fxg-or=RANGE         F(p0 | XG(p1 | XG(p2 | ... XG(pn))))
+      --gxf-and=RANGE        G(p0 & XF(p1 & XF(p2 & ... XF(pn))))
+    The later is a generalization of --eh-pattern=9, for which a
+    single state TGBA always exists (but previous version of Spot
+    would build larger automata).
+
   - autfilt learned to build the union (--sum) or the intersection
     (--sum-and) of two languages by putting two automata side-by-side
     and fiddling with the initial states.  This complements the already

bin/genltl.cc

@@ -84,12 +84,16 @@ static const argp_option options[] =
     { "eh-patterns", gen::LTL_EH_PATTERNS, "RANGE", OPTION_ARG_OPTIONAL,
       "Etessami and Holzmann [Concur'00] patterns "
       "(range should be included in 1..12)", 0 },
+    { "fxg-or", gen::LTL_FXG_OR, "RANGE", 0,
+      "F(p0 | XG(p1 | XG(p2 | ... XG(pn))))", 0},
     { "gh-q", gen::LTL_GH_Q, "RANGE", 0,
       "(F(p1)|G(p2))&(F(p2)|G(p3))&...&(F(pn)|G(p{n+1}))", 0 },
     { "gh-r", gen::LTL_GH_R, "RANGE", 0,
       "(GF(p1)|FG(p2))&(GF(p2)|FG(p3))&... &(GF(pn)|FG(p{n+1}))", 0 },
     { "go-theta", gen::LTL_GO_THETA, "RANGE", 0,
       "!((GF(p1)&GF(p2)&...&GF(pn)) -> G(q->F(r)))", 0 },
+    { "gxf-and", gen::LTL_GXF_AND, "RANGE", 0,
+      "G(p0 & XF(p1 & XF(p2 & ... XF(pn))))", 0},
     { "hkrss-patterns", gen::LTL_HKRSS_PATTERNS,
       "RANGE", OPTION_ARG_OPTIONAL,
       "Holeček et al. patterns from the Liberouter project "

spot/gen/formulas.cc

@@ -41,6 +41,40 @@ namespace spot
   {
     namespace
     {
+      // G(p_0 & XF(p_1 & XF(p_2 & ... XF(p_n))))
+      // This is a generalization of eh-pattern=9
+      static formula
+      GXF_and_n(std::string name, int n)
+      {
+        formula result = formula::tt();
+
+        for (; n >= 0; --n)
+          {
+            std::ostringstream p;
+            p << name << n;
+            formula f = formula::ap(p.str());
+            result = And_(f, X_(F_(result)));
+          }
+        return G_(result);
+      }
+
+      // F(p_0 | XG(p_1 | XG(p_2 | ... XG(p_n))))
+      // This the dual of the above
+      static formula
+      FXG_or_n(std::string name, int n)
+      {
+        formula result = formula::ff();
+
+        for (; n >= 0; --n)
+          {
+            std::ostringstream p;
+            p << name << n;
+            formula f = formula::ap(p.str());
+            result = Or_(f, X_(G_(result)));
+          }
+        return F_(result);
+      }
+
       // F(p_1 & F(p_2 & F(p_3 & ... F(p_n))))
       static formula
       E_n(std::string name, int n)
@@ -1070,12 +1104,16 @@ namespace spot
           return dac_pattern(n);
         case LTL_EH_PATTERNS:
           return eh_pattern(n);
+        case LTL_FXG_OR:
+          return FXG_or_n("p", n);
         case LTL_GH_Q:
           return Q_n("p", n);
         case LTL_GH_R:
           return R_n("p", n);
         case LTL_GO_THETA:
           return fair_response("p", "q", "r", n);
+        case LTL_GXF_AND:
+          return GXF_and_n("p", n);
         case LTL_HKRSS_PATTERNS:
           return hkrss_pattern(n);
         case LTL_KR_N:
@@ -1139,9 +1177,11 @@ namespace spot
           "ccj-beta-prime",
           "dac-patterns",
           "eh-patterns",
+          "fxg-or",
           "gh-q",
           "gh-r",
           "go-theta",
+          "gxf-and",
           "hkrss-patterns",
           "kr-n",
           "kr-nlogn",
@@ -1190,9 +1230,11 @@ namespace spot
           return 55;
         case LTL_EH_PATTERNS:
           return 12;
+        case LTL_FXG_OR:
         case LTL_GH_Q:
         case LTL_GH_R:
         case LTL_GO_THETA:
+        case LTL_GXF_AND:
           return 0;
         case LTL_HKRSS_PATTERNS:
           return 55;

spot/gen/formulas.hh

@@ -175,9 +175,11 @@ namespace spot
       LTL_CCJ_BETA_PRIME,
       LTL_DAC_PATTERNS,
       LTL_EH_PATTERNS,
+      LTL_FXG_OR,
       LTL_GH_Q,
       LTL_GH_R,
       LTL_GO_THETA,
+      LTL_GXF_AND,
       LTL_HKRSS_PATTERNS,
       LTL_KR_N,
       LTL_KR_NLOGN,

tests/core/genltl.test

@@ -110,7 +110,8 @@ EOF
 diff output expected
 
 
-genltl --kr-n2=1..2 --kr-nlogn=1..2 --kr-n=1..2 --format=%F=%L,%f |
+genltl --kr-n2=1..2 --kr-nlogn=1..2 --kr-n=1..2 --gxf-and=0..3 --fxg-or=0..3 \
+       --format=%F=%L,%f |
     ltl2tgba --low --det -F-/2 --stats='%<,%s' > out
 cat >exp<<EOF
 kv-psi=1,15
@@ -119,6 +120,14 @@ kr-nlogn=1,19
 kr-nlogn=2,147
 kr-n=1,12
 kr-n=2,82
+gxf-and=0,1
+gxf-and=1,1
+gxf-and=2,1
+gxf-and=3,1
+fxg-or=0,2
+fxg-or=1,3
+fxg-or=2,4
+fxg-or=3,5
 EOF
 diff out exp