simplifier: new LTL simplifications

if e is pure eventuality and g => e, then e U g = Fg
if u is purely universal and u => g, then u R g = Gg

Fixes #93.

* doc/tl/tl.tex, NEWS: Document the rules.
* spot/tl/simplify.cc: Implement them.
* tests/core/reduccmp.test: Test them.
* tests/core/det.test: Adjust.

NEWS

@@ -111,6 +111,10 @@ New in spot 2.0.3a (not yet released)
     implies that "autfilt --check=stutter" will now label all
     automata, not just deterministic automata.
 
+  * New LTL simplification rules:
+    - if e is pure eventuality and g => e, then e U g = Fg
+    - if u is purely universal and u => g, then u R g = Gg
+
   Python:
 
   * The __format__() method for formula supports the same

doc/tl/tl.tex

@@ -1720,7 +1720,9 @@ In the following rewritings rules, $f\simp g$ means that $g$ was
 proved to be implied by $f$ using either of the above two methods.
 Additionally, implications denoted by $f\Simp g$ are only checked if
 the ``\verb|tl_simplifier_options::containment_checks_stronger|''
-option is set (otherwise the rewriting rule is not applied).
+option is set (otherwise the rewriting rule is not applied).  As in
+the previous section, formulas $e$ and $u$ represent respectively
+pure eventualities and purely universal formulas.
 
 \begin{equation*}
 \begin{array}{cccr@{\,}l}
@@ -1731,6 +1733,7 @@ option is set (otherwise the rewriting rule is not applied).
 \text{if}& f\simp g        &\text{then}& f\U g &\equiv g \\
 \text{if}& (f\U g)\Simp g  &\text{then}& f\U g &\equiv g \\
 \text{if}& (\NOT f)\simp g &\text{then}& f\U g &\equiv \F g \\
+\text{if}& g\simp e        &\text{then}& e\U g &\equiv \F g \\
 \text{if}& f\simp g        &\text{then}& f\U (g \U h) &\equiv g \U h \\
 \text{if}& f\simp g        &\text{then}& f\U (g \W h) &\equiv g \W h \\
 \text{if}& g\simp f        &\text{then}& f\U (g \U h) &\equiv f \U h \\
@@ -1753,6 +1756,7 @@ option is set (otherwise the rewriting rule is not applied).
 \text{if}& g\simp h        &\text{then}& (f\U g) \W h &\equiv (f \U g) \OR h \\
 \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 \\
+\text{if}& u\simp g        &\text{then}& u\R g &\equiv \G g \\
 \text{if}& g\simp f        &\text{then}& f\R (g \R h) &\equiv g \R h \\
 \text{if}& g\simp f        &\text{then}& f\R (g \M h) &\equiv g \M h \\
 \text{if}& f\simp g        &\text{then}& f\R (g \R h) &\equiv f \R h \\
@@ -1771,8 +1775,8 @@ option is set (otherwise the rewriting rule is not applied).
 \end{array}
 \end{equation*}
 
-The above rules were collected from various
+Many of the above rules were collected from the
-sources~\cite{somenzi.00.cav,tauriainen.03.a83,babiak.12.tacas} and
+literature~\cite{somenzi.00.cav,tauriainen.03.a83,babiak.12.tacas} and
 sometimes generalized to support operators such as $\M$ and $\W$.
 
 \appendix

spot/tl/simplify.cc

@@ -1644,7 +1644,9 @@ namespace spot
                         && c_->contained(bo, b)))
                   return b;
                 // if !a => b, then a U b = Fb
-                if (c_->implication_neg(a, b, false))
+                // if a eventual && b => a, then a U b = Fb
+                if (c_->implication_neg(a, b, false)
+                    || (a.is_eventual() && c_->implication(b, a)))
                   return recurse(formula::F(b));
                 // if a => b, then a U (b U c) = (b U c)
                 // if a => b, then a U (b W c) = (b W c)
@@ -1677,7 +1679,9 @@ namespace spot
                 if (c_->implication(b, a))
                   return b;
                 // if b => !a, then a R b = Gb
-                if (c_->implication_neg(b, a, true))
+                // if a universal && a => b, then a R b = Gb
+                if (c_->implication_neg(b, a, true)
+                    || (a.is_universal() && c_->implication(a, b)))
                   return recurse(formula::G(b));
                 // if b => a, then a R (b R c) = b R c
                 // if b => a, then a R (b M c) = b M c

tests/core/det.test

@@ -38,7 +38,7 @@ cat >formulas <<'EOF'
 1,5,a M G(F!b | X!a)
 1,4,G!a R XFb
 1,4,XF(!a | GFb)
-1,6,G(F!a U !a) U Xa
+1,6,GF!a U Xa
 1,5,(a | G(a M !b)) W Fc
 1,6,Fa W Xb
 1,10,X(a R ((!b & F!c) M X!a))

tests/core/reduccmp.test

@@ -1,6 +1,6 @@
 #! /bin/sh
 # -*- coding: utf-8 -*-
-# Copyright (C) 2009, 2010, 2011, 2012, 2013, 2014 Laboratoire de
+# Copyright (C) 2009, 2010, 2011, 2012, 2013, 2014, 2016 Laboratoire de
 # Recherche et Developpement de l'Epita (LRDE).
 # Copyright (C) 2004, 2006 Laboratoire d'Informatique de Paris 6 (LIP6),
 # département Systèmes Répartis Coopératifs (SRC), Université Pierre
@@ -104,6 +104,16 @@ b U GFa, GFa
 Ga, Ga
 
 a U XXXFb, XXXFb
+
+# issue 93
+GFa U Ga, FGa
+FGa U Ga, FGa
+GFa U a, GFa U a
+Fa U a, Fa
+GFa R Fa, GFa
+FGa R Fa, GFa
+FGa R a, FGa R a
+Ga R a, Ga
 EOF
 
 cp common.txt nottau.txt