genltl: add --gf-equiv-xn, --gf-implies-xn

* spot/gen/formulas.cc, spot/gen/formulas.hh: Here.
* bin/genltl.cc: Add options.
* tests/core/genltl.test: Test them.
* NEWS: Mention them.

NEWS

@@ -26,7 +26,9 @@ New in spot 2.5.3.dev  (not yet released)
     products to avoid exceeding the number of supported
     acceptance sets.
 
-  - genltl learned to generate four new families of LTL formulas:
+  - genltl learned to generate six new families of LTL formulas:
+      --gf-equiv-xn=RANGE    GF(a <-> X^n(a))
+      --gf-implies-xn=RANGE  GF(a -> X^n(a))
       --sejk-f=RANGE[,RANGE] f(0,j)=(GFa0 U X^j(b)), f(i,j)=(GFai U
                              G(f(i-1,j)))
       --sejk-j=RANGE         (GFa1&...&GFan) -> (GFb1&...&GFbn)

bin/genltl.cc

@@ -88,8 +88,12 @@ static const argp_option options[] =
       "F(p0 | XG(p1 | XG(p2 | ... XG(pn))))", 0},
     { "gf-equiv", gen::LTL_GF_EQUIV, "RANGE", 0,
       "(GFa1 & GFa2 & ... & GFan) <-> GFz", 0},
+    { "gf-equiv-xn", gen::LTL_GF_EQUIV_XN, "RANGE", 0,
+      "GF(a <-> X^n(a))", 0},
     { "gf-implies", gen::LTL_GF_IMPLIES, "RANGE", 0,
       "(GFa1 & GFa2 & ... & GFan) -> GFz", 0},
+    { "gf-implies-xn", gen::LTL_GF_IMPLIES_XN, "RANGE", 0,
+      "GF(a -> X^n(a))", 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,

spot/gen/formulas.cc

@@ -256,8 +256,19 @@ namespace spot
         return result;
       }
 
+      // Builds X(X(...X(p))) with n occurrences of X.
       static formula
-      LTL_GF_equiv_implies(int n, const std::string& a, const std::string& z,
+      X_n(formula p, int n)
+      {
+        assert(n >= 0);
+        formula res = p;
+        while (n--)
+          res = X_(res);
+        return res;
+      }
+
+      static formula
+      GF_equiv_implies(int n, const std::string& a, const std::string& z,
                        bool equiv)
       {
         formula left = GF_n(a, n);
@@ -268,6 +279,19 @@ namespace spot
           return formula::Implies(left, right);
       }
 
+      static formula
+      GF_equiv_implies_xn(int n, const std::string& a, bool equiv)
+      {
+        formula ap = formula::ap(a);
+        formula xn = X_n(ap, n);
+        formula in;
+        if (equiv)
+          in = formula::Equiv(ap, xn);
+        else
+          in = formula::Implies(ap, xn);
+        return G_(F_(in));
+      }
+
       //  (((p1 OP p2) OP p3)...OP pn)   if right_assoc == false
       //  (p1 OP (p2 OP (p3 OP (... pn)  if right_assoc == true
       static formula
@@ -402,17 +426,6 @@ namespace spot
         return Not_(Implies_(fair, resp));
       }
 
-      // Builds X(X(...X(p))) with n occurrences of X.
-      static formula
-      X_n(formula p, int n)
-      {
-        assert(n >= 0);
-        formula res = p;
-        while (n--)
-          res = X_(res);
-        return res;
-      }
-
       // Based on LTLcounter.pl from Kristin Rozier.
       // http://shemesh.larc.nasa.gov/people/kyr/benchmarking_scripts/
       static formula
@@ -1224,9 +1237,13 @@ namespace spot
         case LTL_FXG_OR:
           return FXG_or_n("p", n);
         case LTL_GF_EQUIV:
-          return LTL_GF_equiv_implies(n, "a", "z", true);
+          return GF_equiv_implies(n, "a", "z", true);
+        case LTL_GF_EQUIV_XN:
+          return GF_equiv_implies_xn(n, "a", true);
         case LTL_GF_IMPLIES:
-          return LTL_GF_equiv_implies(n, "a", "z", false);
+          return GF_equiv_implies(n, "a", "z", false);
+        case LTL_GF_IMPLIES_XN:
+          return GF_equiv_implies_xn(n, "a", false);
         case LTL_GH_Q:
           return Q_n("p", n);
         case LTL_GH_R:
@@ -1316,7 +1333,9 @@ namespace spot
           "eh-patterns",
           "fxg-or",
           "gf-equiv",
+          "gf-equiv-xn",
           "gf-implies",
+          "gf-implies-xn",
           "gh-q",
           "gh-r",
           "go-theta",
@@ -1379,7 +1398,9 @@ namespace spot
           return 12;
         case LTL_FXG_OR:
         case LTL_GF_EQUIV:
+        case LTL_GF_EQUIV_XN:
         case LTL_GF_IMPLIES:
+        case LTL_GF_IMPLIES_XN:
         case LTL_GH_Q:
         case LTL_GH_R:
         case LTL_GO_THETA:
@@ -1444,7 +1465,9 @@ namespace spot
         case LTL_EH_PATTERNS:
         case LTL_FXG_OR:
         case LTL_GF_EQUIV:
+        case LTL_GF_EQUIV_XN:
         case LTL_GF_IMPLIES:
+        case LTL_GF_IMPLIES_XN:
         case LTL_GH_Q:
         case LTL_GH_R:
         case LTL_GO_THETA:

spot/gen/formulas.hh

@@ -220,7 +220,9 @@ namespace spot
       LTL_EH_PATTERNS,
       LTL_FXG_OR,
       LTL_GF_EQUIV,
+      LTL_GF_EQUIV_XN,
       LTL_GF_IMPLIES,
+      LTL_GF_IMPLIES_XN,
       LTL_GH_Q,
       LTL_GH_R,
       LTL_GO_THETA,

tests/core/genltl.test

@@ -154,7 +154,8 @@ 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 \
-       --gf-equiv=0..5 --gf-implies=0..5 --format='"%F=%L",%f' |
+       --gf-equiv=0..5 --gf-implies=0..5 --gf-equiv-xn=1..3 --gf-implies-xn=3 \
+       --format='"%F=%L",%f' |
     ltl2tgba -G -D -F-/2 --stats='%<,%s' > out
 cat >exp<<EOF
 "ms-example=0,0",1
@@ -205,12 +206,17 @@ cat >exp<<EOF
 "gf-implies=3",41
 "gf-implies=4",186
 "gf-implies=5",1047
+"gf-equiv-xn=1",2
+"gf-equiv-xn=2",4
+"gf-equiv-xn=3",8
+"gf-implies-xn=3",1
 EOF
 diff out exp
 
 # Running ltl2tgba on one formula at a time should give the same results
 genltl --ms-example=0..4 --ms-phi-r=0..2 --ms-phi-s=0..2 --ms-phi-h=0..4 \
-       --gf-equiv=0..5 --gf-implies=0..5 --format='"%F=%L",%f' |
+       --gf-equiv=0..5 --gf-implies=0..5 --gf-equiv-xn=1..3 --gf-implies-xn=3 \
+       --format='"%F=%L",%f' |
     ltldo -F-/2 'ltl2tgba -G -D' --stats='%<,%s' > out
 diff out exp