genltl: introduce --eil-gsi

Based on a mail from Edmond Irani Liu.  The test case also serves for
the previous patch.

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

NEWS

@@ -51,6 +51,13 @@ New in spot 2.10.6.dev  (not yet released)
     include each other, and are used to show a regression (in speed)
     present in Spot 2.10.x and fixed in 2.11.
 
+  - genltl learned --eil-gsi to generate a familly a function whose
+    translation and simplification used to be very slow.  In particular
+
+       genltl --eil-gsi=23 | ltlfilt --from-ltlf | ltl2tgba
+
+     was reported as taking 9 days.  This is now instantaneous.
+
   Library:
 
   - The new function suffix_operator_normal_form() implements
@@ -149,7 +156,8 @@ New in spot 2.10.6.dev  (not yet released)
     and q₃ can be merged (taking the union of their outgoing
     transitions).  This is cheap function is automatically called by
     spot::translate() after translation of a formula to GBA, before
-    further simplification.
+    further simplification.  This was introduced to help with automata
+    produced from formulas output by "genltl --eil-gsi" (see above).
 
   - spot::parallel_policy is an object that can be passed to some
     algorithm to specify how many threads can be used if Spot has been

bin/genltl.cc

@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2012, 2013, 2015-2019 Laboratoire de Recherche et
+// Copyright (C) 2012, 2013, 2015-2019, 2022 Laboratoire de Recherche et
 // Développement de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
@@ -84,6 +84,8 @@ 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 },
+    { "eil-gsi", gen::LTL_EIL_GSI, "RANGE", 0,
+      "G[0..n]((a S b) -> c) rewritten using future operators", 0 },
     { "fxg-or", gen::LTL_FXG_OR, "RANGE", 0,
       "F(p0 | XG(p1 | XG(p2 | ... XG(pn))))", 0},
     { "gf-equiv", gen::LTL_GF_EQUIV, "RANGE", 0,

spot/gen/formulas.cc

@@ -1281,6 +1281,21 @@ namespace spot
         }
     }
 
+    // G[0..n]((a S b) -> c) rewritten using future operators,
+    // from Edmond Irani Liu (EIL).  GSI stands for "Globally Since Implies."
+    static formula eil_gsi(int n, std::string a, std::string b, std::string c)
+    {
+      formula fa = formula::ap(a);
+      formula fb = formula::ap(b);
+      formula res = fb;
+      for (int i = 1; i <= n; ++i)
+        {
+          formula tmp = formula::And({formula::strong_X(i, fa), res});
+          res = formula::Or({formula::strong_X(i, fb), tmp});
+        }
+      return formula::Implies(res, formula::strong_X(n, formula::ap(c)));
+    }
+
     formula ltl_pattern(ltl_pattern_id pattern, int n, int m)
     {
       if (n < 0)
@@ -1317,6 +1332,8 @@ namespace spot
           return dac_pattern(n);
         case LTL_EH_PATTERNS:
           return eh_pattern(n);
+        case LTL_EIL_GSI:
+          return eil_gsi(n, "a", "b", "c");
         case LTL_FXG_OR:
           return FXG_or_n("p", n);
         case LTL_GF_EQUIV:
@@ -1418,6 +1435,7 @@ namespace spot
           "ccj-beta-prime",
           "dac-patterns",
           "eh-patterns",
+          "eil-gsi",
           "fxg-or",
           "gf-equiv",
           "gf-equiv-xn",
@@ -1485,6 +1503,7 @@ namespace spot
           return 55;
         case LTL_EH_PATTERNS:
           return 12;
+        case LTL_EIL_GSI:
         case LTL_FXG_OR:
         case LTL_GF_EQUIV:
         case LTL_GF_EQUIV_XN:
@@ -1554,6 +1573,7 @@ namespace spot
         case LTL_CCJ_BETA_PRIME:
         case LTL_DAC_PATTERNS:
         case LTL_EH_PATTERNS:
+        case LTL_EIL_GSI:
         case LTL_FXG_OR:
         case LTL_GF_EQUIV:
         case LTL_GF_EQUIV_XN:

spot/gen/formulas.hh

@@ -1,6 +1,6 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2017, 2018, 2019 Laboratoire de Recherche et Developpement de
+// Copyright (C) 2017-2019, 2022 Laboratoire de Recherche et
-// l'EPITA (LRDE).
+// Developpement de l'EPITA (LRDE).
 //
 // This file is part of Spot, a model checking library.
 //
@@ -56,6 +56,8 @@ namespace spot
       /// 12 formulas from Etessami and Holzmann.
       /// \cite etessami.00.concur
       LTL_EH_PATTERNS,
+      /// Familly sent by Edmond Irani Liu
+      LTL_EIL_GSI,
       /// `F(p0 | XG(p1 | XG(p2 | ... XG(pn))))`
       LTL_FXG_OR,
       /// `(GFa1 & GFa2 & ... & GFan) <-> GFz`

tests/core/genltl.test

@@ -269,3 +269,43 @@ diff range1.ltl range2.ltl
 genltl --sb-patterns=1..20 | ltlfilt -v --nth 10..20 > range1.ltl
 genltl --sb-patterns=1..9 > range2.ltl
 diff range1.ltl range2.ltl
+
+
+# Edmond Irani Liu sent a bug report where formula 23 in this series
+# took 9 days to produce, despite the small size of the resulting
+# automaton.  I (ADL) later found this to be caused by simulation
+# applied on a non-deterministic automaton with many non-deterministic
+# choices going to state that simulate one another, which in turn lead
+# to massive slowdown of the minato_isop algorithm.  As a workaround,
+# I introduced delay_branching_here(), a cheap function that is called
+# before simplification.  In this case, this is enough to determinize
+# the automaton, simplifying simulation-based reduction greatly.
+genltl --eil-gsi=1..25 | ltlfilt --from-ltlf | ltl2tgba --stats=%s,%e >output
+cat >expected <<EOF
+5,9
+7,15
+9,21
+11,27
+13,33
+15,39
+17,45
+19,51
+21,57
+23,63
+25,69
+27,75
+29,81
+31,87
+33,93
+35,99
+37,105
+39,111
+41,117
+43,123
+45,129
+47,135
+49,141
+51,147
+53,153
+EOF
+diff expected output