simplify: rewrite GF(a & GFb) as G(Fa & Fb)

Fixes #185.

* spot/tl/simplify.cc: Implement the new rule.
* NEWS, doc/tl/tl.tex: Document it.
* tests/core/reduccmp.test: Test it.

NEWS

@@ -1,5 +1,13 @@
 New in spot 2.1.1a (not yet released)
 
+  Library:
+
+  * New LTL simplification rule:
+
+    - GF(f & q) = G(F(f) & q) if q is
+      purely universal and a pure eventuality.  In particular
+      GF(f & GF(g)) now ultimately simplifies to G(F(f) & F(g)).
+
   Bug fixes:
 
   - Fix spurious uninitialized read reported by valgrind when

doc/tl/tl.tex

@@ -1690,6 +1690,7 @@ $q,\,q_i$           & a pure eventuality that is also purely universal \\
   \G(f_1\OR\ldots\OR f_n \OR q_1 \OR \ldots \OR q_p)&\equiv \G(f_1\OR\ldots\OR f_n)\OR q_1 \OR \ldots \OR q_p \\
   \F(f_1\AND\ldots\AND f_n \AND q_1 \AND \ldots \AND q_p)&\equivEU \F(f_1\AND\ldots\AND f_n)\AND q_1 \AND \ldots \AND q_p \\
   \G(f_1\AND\ldots\AND f_n \AND q_1 \AND \ldots \AND q_p)&\equivEU \G(f_1\AND\ldots\AND f_n)\AND q_1 \AND \ldots \AND q_p \\
+  \G\F(f_1\AND\ldots\AND f_n \AND q_1 \AND \ldots \AND q_p)&\equiv \G(\F(f_1\AND\ldots\AND f_n)\AND q_1 \AND \ldots \AND q_p) \\
   \G(f_1\AND\ldots\AND f_n \AND e_1 \AND \ldots \AND e_m \AND \G(e_{m+1}) \AND \ldots\AND \G(e_p))&\equivEU \G(f_1\AND\ldots\AND f_n)\AND \G(e_1 \AND \ldots \AND e_p) \\
   \G(f_1\AND\ldots\AND f_n \AND \G(g_1) \AND \ldots \AND \G(g_m) &\equiv \G(f_1\AND\ldots\AND f_n\AND g_1 \AND \ldots \AND g_m) \\
   \F(f_1 \OR \ldots \OR f_n \OR u_1 \OR \ldots \OR u_m \OR \F(u_{m+1})\OR\ldots\OR \F(u_p)) &\equivEU \F(f_1\OR \ldots\OR f_n) \OR \F(u_1 \OR \ldots \OR u_p)\\

spot/tl/simplify.cc

@@ -968,6 +968,12 @@ namespace spot
               // So we do not consider this rewriting rule by
               // default.  However if favor_event_univ is set,
               // we want to move the GF out of the F.
+              //
+              // Also if this appears inside a G, we want to
+              // reduce it:
+              //     GF(f1 & GF(f2)) = G(F(f1) & GF(f2))
+              //                     = G(F(f1) & F(f2))
+              // But this is handled by the G case.
               if (opt_.favor_event_univ)
                 // F(f1&f2&FG(f3)&FG(f4)&f5&f6) =
                 //                     F(f1&f2) & FG(f3&f4) & f5 & f6
@@ -1114,6 +1120,19 @@ namespace spot
                             return recurse(unop_unop(op::G, op::F, out));
                         }
                     }
+                  // GF(f1 & f2 & eu1 & eu2) = G(F(f1 & f2) & eu1 & eu2
+                  if (opt_.event_univ && c.is({op::F, op::And}))
+                    {
+                      mospliter s(mospliter::Split_EventUniv,
+                                  c[0], c_);
+                      s.res_EventUniv->
+                        push_back(unop_multop(op::F, op::And,
+                                              std::move(*s.res_other)));
+                      formula res =
+                        formula::G(formula::And(std::move(*s.res_EventUniv)));
+                      if (res != f)
+                        return recurse(res);
+                    }
                 }
               // if a => Ga, keep a.
               if (opt_.containment_checks_stronger

tests/core/reduccmp.test

@@ -403,6 +403,8 @@ G(GFc|GFd|FGe|FGf), F(GF(c|d)|Ge|Gf)
 {e[*0..5]}<>->f, {e[*1..5]}<>->f
 {e[*0..5]}[]->f, {e[*1..5]}[]->f
 {(e+[*0])[*0..5]}[]->f, {e[*1..5]}[]->f
+# issue 185
+GF(a && GF(b) && c), G(F(a & c) & Fb)
 # not reduced
 {a;(b[*2..4];c*;([*0]+{d;e}))*}!, {a;(b[*2..4];c*;([*0]+{d;e}))*}!
 {c[*];e[*]}[]-> a, {c[*];e[*]}[]-> a