tl: eight new simplification rules

* NEWS, doc/tl/tl.tex: Document the rules.
* spot/tl/simplify.cc: Implement them.
* tests/core/reduccmp.test: Test them.
* tests/core/det.test, tests/core/ltl2tgba2.test,
tests/python/stutter-inv.ipynb, tests/core/385.test: Adjust.

NEWS

@@ -112,13 +112,21 @@ New in spot 2.7.5.dev (not yet released)
   - spot::relabel_apply() makes it easier to reverse the effect
     of spot::relabel() or spot::relabel_bse() on formula.
 
-  - The LTL simplifier learned the following optional rules:
+  - The LTL simplifier learned the following rules:
     F(G(a | Fb)) = FGa | GFb  (if option "favor_event_univ")
     G(F(a | Gb)) = GFa | FGb  (if option "favor_event_univ")
     F(G(a & Fb) = FGa & GFb   (unless option "reduce_size_strictly")
     G(F(a & Gb)) = GFa & FGb  (unless option "reduce_size_strictly")
     GF(f) = GF(dnf(f))        (unless option "reduce_size_strictly")
     FG(f) = FG(cnf(f))        (unless option "reduce_size_strictly")
+    (f & g) R h = f R h       if h implies g
+    (f & g) M h = f M h       if h implies g
+    (f | g) W h = f W h       if g implies h
+    (f | g) U h = f U h       if g implies h
+    Gf | F(g & eventual) = f W (g & eventual)    if !f implies g
+    Ff & G(g | universal) = f M (g | universal)  if f implies !g
+    f U (g & eventual) = F(g & eventual)         if !f implies g
+    f R (g | universal) = G(g | universal)       if f implies !g
 
   - cleanup_parity() and colorize_parity() were cleaned up a bit,
     resulting in fewer colors used in some cases.  In particular,

doc/tl/tl.tex

@@ -1857,6 +1857,7 @@ are counted as one.
 \text{if~} & f\simp h        &  & \text{~then~} & (f\U g) \U h        & \equiv g \U h             \\
 \text{if~} & f\simp h        &  & \text{~then~} & (f\W g) \U h        & \equiv g \U h             \\
 \text{if~} & g\simp h        &  & \text{~then~} & (f\U g) \U h        & \equiv (f \U g) \OR h     \\
+\text{if~} & g\simp h        &  & \text{~then~} & (f\OR g) \U h       & \equiv f \U h             \\
 \text{if~} & (\NOT f)\simp g &  & \text{~then~} & f\W g               & \equiv \1                 \\
 \text{if~} & \flessg         &  & \text{~then~} & f\W g               & \equiv f                  \\
 \text{if~} & f\simp g        &  & \text{~then~} & f\W g               & \equiv g                  \\
@@ -1868,6 +1869,7 @@ are counted as one.
 \text{if~} & f\simp h        &  & \text{~then~} & (f\W g) \W h        & \equiv g \W h             \\
 \text{if~} & g\simp h        &  & \text{~then~} & (f\W g) \W h        & \equiv (f \W g) \OR h     \\
 \text{if~} & g\simp h        &  & \text{~then~} & (f\U g) \W h        & \equiv (f \U g) \OR h     \\
+\text{if~} & g\simp h        &  & \text{~then~} & (f\OR g) \W h       & \equiv f \W h             \\
 \text{if~} & \flessg         &  & \text{~then~} & f\R g               & \equiv f                  \\
 \text{if~} & g\simp f        &  & \text{~then~} & f\R g               & \equiv g                  \\
 \text{if~} & g\simp \NOT f   &  & \text{~then~} & f\R g               & \equiv \G g               \\
@@ -1879,6 +1881,7 @@ are counted as one.
 \text{if~} & h\simp f        &  & \text{~then~} & (f\M g) \R h        & \equiv g \R h             \\
 \text{if~} & g\simp h        &  & \text{~then~} & (f\R g) \R h        & \equiv (f \AND g) \R h    \\
 \text{if~} & g\simp h        &  & \text{~then~} & (f\M g) \R h        & \equiv (f \AND g) \R h    \\
+\text{if~} & h\simp g        &  & \text{~then~} & (f\AND g) \R h      & \equiv f \R h             \\
 \text{if~} & \flessg         &  & \text{~then~} & f\M g               & \equiv f                  \\
 \text{if~} & g\simp f        &  & \text{~then~} & f\M g               & \equiv g                  \\
 \text{if~} & g\simp \NOT f   &  & \text{~then~} & f\M g               & \equiv \0                 \\
@@ -1888,6 +1891,7 @@ are counted as one.
 \text{if~} & h\simp f        &  & \text{~then~} & (f\M g) \M h        & \equiv g \M h             \\
 \text{if~} & h\simp f        &  & \text{~then~} & (f\R g) \M h        & \equiv g \M h             \\
 \text{if~} & g\simp h        &  & \text{~then~} & (f\M g) \M h        & \equiv (f \AND g) \M h    \\
+\text{if~} & h\simp g        &  & \text{~then~} & (f\AND g) \M h      & \equiv f \M h             \\
 \end{alignat*}
 \endgroup
 
@@ -1895,6 +1899,17 @@ Many of the above rules were collected from the
 literature~\cite{somenzi.00.cav,tauriainen.03.tr,babiak.12.tacas} and
 sometimes generalized to support operators such as $\M$ and $\W$.
 
+The following rules mix implication-based checks with formulas that
+are pure eventualities ($e$) or that are purely universal ($u$).
+
+\allowdisplaybreaks
+\begin{alignat*}{3}
+\text{if~} & (\NOT f)\simp g  &  & \text{~then~} & f \U (g \AND e)        & \equiv \F(g \AND e)    \\
+\text{if~} & f\simp \NOT g    &  & \text{~then~} & f \R (g \OR u)         & \equiv \G(g \OR e)     \\
+\text{if~} & (\NOT f) \simp g &  & \text{~then~} & \G(f) \OR \F(g \AND e) & \equiv f \W (g \AND e) \\
+\text{if~} & f \simp\NOT g    &  & \text{~then~} & \F(f) \AND \G(g \OR e) & \equiv f \M (g \OR e)  \\
+\end{alignat*}
+
 \appendix
 \chapter{Defining LTL with only one of $\U$, $\W$, $\R$, or $\M$}
 \label{sec:ltl-equiv}

spot/tl/simplify.cc

@@ -2160,6 +2160,31 @@ namespace spot
                 // if c => b, then (a U c) U b = (a U c) | b
                 if (a.is(op::U) && c_->implication(a[1], b))
                   return recurse(formula::Or({a, b}));
+                // if g => h, then (f|g) U h = f U h
+                if (a.is(op::Or))
+                  {
+                    unsigned n = a.size();
+                    for (unsigned child = 0; child < n; ++child)
+                      if (c_->implication(a[child], b))
+                        return recurse(formula::U(a.all_but(child), b));
+                  }
+                // a U (b & e) = F(b & e) if !b => a
+                if (b.is(op::And))
+                  for (formula c: b)
+                    if (c.is_eventual())
+                      {
+                        // We know there is one pure eventuality
+                        // formula but we might have more.  So lets
+                        // extract everything else.
+                        vec rest;
+                        rest.reserve(c.size());
+                        for (formula cc: b)
+                          if (!cc.is_eventual())
+                            rest.emplace_back(cc);
+                        if (c_->implication_neg(formula::And(rest), a, false))
+                          return recurse(formula::F(b));
+                        break;
+                      }
                 break;
 
               case op::R:
@@ -2198,6 +2223,31 @@ namespace spot
                         return recurse(formula::R(ac, b));
                       }
                   }
+                // if h => g, then (f&g) R h = f R h
+                if (a.is(op::And))
+                  {
+                    unsigned n = a.size();
+                    for (unsigned child = 0; child < n; ++child)
+                      if (c_->implication(b, a[child]))
+                        return recurse(formula::R(a.all_but(child), b));
+                  }
+                // a R (b | u) = G(b | u) if b => !a
+                if (b.is(op::Or))
+                  for (formula c: b)
+                    if (c.is_universal())
+                      {
+                        // We know there is one purely universal
+                        // formula but we might have more.  So lets
+                        // extract everything else.
+                        vec rest;
+                        rest.reserve(c.size());
+                        for (formula cc: b)
+                          if (!cc.is_universal())
+                            rest.emplace_back(cc);
+                        if (c_->implication_neg(formula::Or(rest), a, true))
+                          return recurse(formula::G(b));
+                        break;
+                      }
                 break;
 
               case op::W:
@@ -2234,6 +2284,14 @@ namespace spot
                 // if c => b, then (a U c) W b = (a U c) | b
                 if (a.is(op::U, op::W) && c_->implication(a[1], b))
                   return recurse(formula::Or({a, b}));
+                // if g => h, then (f|g) W h = f M h
+                if (a.is(op::Or))
+                  {
+                    unsigned n = a.size();
+                    for (unsigned child = 0; child < n; ++child)
+                      if (c_->implication(a[child], b))
+                        return recurse(formula::W(a.all_but(child), b));
+                  }
                 break;
 
               case op::M:
@@ -2265,6 +2323,14 @@ namespace spot
                   return
                     recurse(formula::M(formula::And({a[0], a[1]}),
                                        b));
+                // if h => g, then (f&g) M h = f M h
+                if (a.is(op::And))
+                  {
+                    unsigned n = a.size();
+                    for (unsigned child = 0; child < n; ++child)
+                      if (c_->implication(b, a[child]))
+                        return recurse(formula::M(a.all_but(child), b));
+                  }
                 break;
 
               default:
@@ -2680,6 +2746,7 @@ namespace spot
                   // F(a) & (a M b) = a M b
                   // F(b) & (a W b) = a U b
                   // F(b) & (a U b) = a U b
+                  // F(c) & G(phi | e) = c M (phi | e)  if c => !phi.
                   typedef std::unordered_map<formula, vec::iterator> fmap_t;
                   fmap_t uwmap; // associates "b" to "a U b" or "a W b"
                   fmap_t rmmap; // associates "a" to "a R b" or "a M b"
@@ -2762,6 +2829,43 @@ namespace spot
                               assert(j->second->is(op::M));
                             }
                         }
+                      if (opt_.synt_impl | opt_.containment_checks)
+                        {
+                          // if the input looks like o1|u1|u2|o2,
+                          // return o1 | o2.  The input must have at
+                          // least on universal formula.
+                          auto extract_not_un =
+                            [&](formula f) {
+                              if (f.is(op::Or))
+                                for (auto u: f)
+                                  if (u.is_universal())
+                                    {
+                                      vec phi;
+                                      phi.reserve(f.size());
+                                      for (auto uu: f)
+                                        if (!uu.is_universal())
+                                          phi.push_back(uu);
+                                      return formula::Or(phi);
+                                    }
+                              return formula(nullptr);
+                            };
+
+                          // F(c) & G(phi | e) = c M (phi | e)  if  c => !phi.
+                          for (auto in_g = s.res_G->begin();
+                               in_g != s.res_G->end();)
+                            {
+                              if (formula phi = extract_not_un(*in_g))
+                                if (c_->implication_neg(phi, c, true))
+                                  {
+                                    s.res_other->push_back(formula::M(c,
+                                                                      *in_g));
+                                    in_g = s.res_G->erase(in_g);
+                                    superfluous = true;
+                                    continue;
+                                  }
+                              ++in_g;
+                            }
+                        }
                       if (superfluous)
                         f = nullptr;
                     }
@@ -3273,6 +3377,7 @@ namespace spot
                   // G(a) | (a W b) = a W b
                   // G(b) | (a R b) = a R b.
                   // G(b) | (a M b) = a R b.
+                  // G(c) | F(phi & e) = c W (phi & e)  if  !c => phi.
                   typedef std::unordered_map<formula, vec::iterator> fmap_t;
                   fmap_t uwmap; // associates "a" to "a U b" or "a W b"
                   fmap_t rmmap; // associates "b" to "a R b" or "a M b"
@@ -3355,6 +3460,43 @@ namespace spot
                               assert(j->second->is(op::R));
                             }
                         }
+                      if (opt_.synt_impl | opt_.containment_checks)
+                        {
+                          // if the input looks like o1&e1&e2&o2,
+                          // return o1 & o2.  The input must have at
+                          // least on eventual formula.
+                          auto extract_not_ev =
+                            [&](formula f) {
+                              if (f.is(op::And))
+                                for (auto e: f)
+                                  if (e.is_eventual())
+                                    {
+                                      vec phi;
+                                      phi.reserve(f.size());
+                                      for (auto ee: f)
+                                        if (!ee.is_eventual())
+                                          phi.push_back(ee);
+                                      return formula::And(phi);
+                                    }
+                              return formula(nullptr);
+                            };
+
+                          // G(c) | F(phi & e) = c W (phi & e)  if  !c => phi.
+                          for (auto in_f = s.res_F->begin();
+                               in_f != s.res_F->end();)
+                            {
+                              if (formula phi = extract_not_ev(*in_f))
+                                if (c_->implication_neg(c, phi, false))
+                                  {
+                                    s.res_other->push_back(formula::W(c,
+                                                                      *in_f));
+                                    in_f = s.res_F->erase(in_f);
+                                    superfluous = true;
+                                    continue;
+                                  }
+                              ++in_f;
+                            }
+                        }
                       if (superfluous)
                         f = nullptr;
                     }

tests/core/385.test

@@ -36,7 +36,7 @@ EOF
 # Some of the following are still not optimal.
 cat >expected <<EOF
 1,GF(!a | !d | !e)
-6,G(Gc | F(a | (!c & F!e)))
+6,G(Fa | (c W (!c & F!e)))
 2,Ge | G(Fd & FGe & Fc)
 1,F(G(Fb & FGc) | Ge)
 4,G(F!d | (!c & G!b))

tests/core/det.test

@@ -26,7 +26,7 @@ cat >formulas <<'EOF'
 1,5,X(((a & b) R (!a U !c)) R b)
 1,8,XXG(Fa U Xb)
 1,5,(!a M !b) W F!c
-1,3,(b & Fa & GFc) R a
+1,3,(b & GFc) R a
 1,2,(a R (b W a)) W G(!a M (b | c))
 1,11,(Fa W b) R (!a | Fc)
 1,6,X(G(!a M !b) | G(a | G!a))

tests/core/ltl2tgba2.test

@@ -77,7 +77,7 @@ dac-patterns,37, 4,56, 4,56, 4,56, 4,56
 dac-patterns,38, 4,56, 4,56, 4,56, 4,56
 dac-patterns,39, 4,112, 4,112, 4,112, 4,112
 dac-patterns,40, 3,88, 3,88, 3,88, 3,88
-dac-patterns,41, 6,54, 6,54, 7,56, 7,56
+dac-patterns,41, 4,32, 4,32, 4,32, 4,32
 dac-patterns,42, 6,96, 6,96, 6,96, 6,96
 dac-patterns,43, 5,80, 5,80, 5,80, 5,80
 dac-patterns,44, 10,300, 10,300, 13,372, 13,372

tests/core/reduccmp.test

@@ -298,17 +298,36 @@ a W ((a&b) W c), a W c
 (a R b) M (c&a), b M (c&a)
 (a M b) M (c&a), b M (c&a)
 
-(a R (b&c)) R (c), (a&b&c) R c
+(x M y) M y, x M y
-(a M (b&c)) R (c), (a&b&c) R c
+(x R y) R y, x R y
+(x & y) M y, x M y
+(x & y) R y, x R y
+
+(a R (b&c)) R (c), (a&b) R c
+(a M (b&c)) R (c), (a&b) R c
 # not reduced
 (a R (b&c)) M (c), (a R (b&c)) M (c)
-(a M (b&c)) M (c), (a&b&c) M c
+(a M (b&c)) M (c), (a&b) M c
 (a W (c&b)) W b, (a W (c&b)) | b
 (a U (c&b)) W b, (a U (c&b)) | b
 (a U (c&b)) U b, (a U (c&b)) | b
 # not reduced
 (a W (c&b)) U b, (a W (c&b)) U b
 
+!x U (x & Fa), F(x & Fa)
+!x R (x | Ga), G(x | Ga)
+!x U ((x | c) & Fa & Fb), F((x | c) & Fa & Fb)
+!x R ((x & c) | Ga | Gb), G((x & c) | Ga | Gb)
+
+G!f | F((f|g) & Fa & Fb), !f W ((f | g) & Fa & Fb)
+F!f & G((f&g) | Ga | Gb), !f M ((f & g) | Ga | Gb)
+
+(x|b) W (x|a), b W (x|a)
+(x|b) U (x|a), b U (x|a)
+
+!x U ((x | c) & Fa & Fb), F((x | c) & Fa & Fb)
+!x R ((x & c) | Ga | Gb), G((x & c) | Ga | Gb)
+
 # Eventuality and universality class reductions
 Fa M b, Fa & b
 GFa M b, GFa & b

tests/python/stutter-inv.ipynb

@@ -302,7 +302,7 @@
        "</svg>\n"
       ],
       "text/plain": [
-       "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f691c29f3f0> >"
+       "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fc090629840> >"
       ]
      },
      "metadata": {},
@@ -603,7 +603,7 @@
        "</svg>\n"
       ],
       "text/plain": [
-       "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f691c31c360> >"
+       "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fc090629db0> >"
       ]
      },
      "metadata": {},
@@ -812,7 +812,7 @@
        "</svg>\n"
       ],
       "text/plain": [
-       "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f691c31c360> >"
+       "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fc090629db0> >"
       ]
      },
      "metadata": {},
@@ -964,7 +964,7 @@
        "</svg>\n"
       ],
       "text/plain": [
-       "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f691c29f840> >"
+       "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fc0905b5960> >"
       ]
      },
      "metadata": {},
@@ -1062,7 +1062,7 @@
        "</svg>\n"
       ],
       "text/plain": [
-       "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f691c29f690> >"
+       "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fc0905b5840> >"
       ]
      },
      "metadata": {},
@@ -1272,7 +1272,7 @@
        "</svg>\n"
       ],
       "text/plain": [
-       "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f691c29f7e0> >"
+       "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fc0905c34e0> >"
       ]
      },
      "metadata": {},
@@ -1401,7 +1401,7 @@
        "</svg>\n"
       ],
       "text/plain": [
-       "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f691c29f780> >"
+       "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fc0905c3570> >"
       ]
      },
      "metadata": {},
@@ -1532,7 +1532,7 @@
        "</svg>\n"
       ],
       "text/plain": [
-       "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f691c29f810> >"
+       "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fc0905c3f90> >"
       ]
      },
      "metadata": {},
@@ -1792,7 +1792,7 @@
        "</svg>\n"
       ],
       "text/plain": [
-       "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f691c23bb10> >"
+       "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fc0905c3240> >"
       ]
      },
      "metadata": {},
@@ -2106,7 +2106,7 @@
        "</svg>\n"
       ],
       "text/plain": [
-       "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f691c23bb10> >"
+       "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fc0905c3240> >"
       ]
      },
      "metadata": {},
@@ -2192,7 +2192,7 @@
       "G!p0 | (!p0 U (p0 & (F(p1 & XFp2) -> (!p      4        2          1\n",
       "G((p0 & Fp1) -> (!(!p1 & p2 & X(!p1 U (!      4        1          1\n",
       "G(p0 -> ((!(!p1 & p2 & X(!p1 U (!p1 & p3      3        0          1\n",
-      "G((p0 & XFp1) -> XF(p1 & Fp2))                6        1          1\n",
+      "G((p0 & XFp1) -> XF(p1 & Fp2))                4        0          1\n",
       "Fp0 -> (((p1 & X(!p0 U p2)) -> X(!p0 U (      6        2          1\n",
       "G(p0 -> G((p1 & XFp2) -> X(!p2 U (p2 & F      5        0          1\n",
       "G((p0 & Fp1) -> (((p2 & X(!p1 U p3)) ->      10        2          1\n",
@@ -2318,7 +2318,7 @@
     {
      "data": {
       "text/plain": [
-       "55.749128919860624"
+       "55.78947368421053"
       ]
      },
      "execution_count": 31,