Add implication-based rewritings from Babiak et al. (TACAS'12)

* src/ltlvisit/simplify.cc: Implement them here, and augment them
to support M, and W operators.
* src/ltltest/reduccmp.test: Add some tests.
* doc/tl/tl.tex (Simplifications Based on Implications): Document
these rules.
* doc/tl/tl.bib (babiak.12.tacas): New entry.

doc/tl/tl.bib

 
+@InProceedings{	  babiak.12.tacas,
+  author	= {Thom{\'a}{\v{s}} Babiak and Mojm{\'i}r
+		  K{\v{r}}et{\'i}nsk{\'y} and Vojt{\v{e}}ch {\v{R}e}eh{\'a}k
+		  and Jan Strej{\v c}ek},
+  title		= {{LTL} to {B\"u}chi Automata Translation: Fast and More
+		  Deterministic},
+  year		= 2012,
+  booktitle	= {Proceedings of the 18th International Conference on Tools
+		  and Algorithms for the Construction and Analysis of Systems
+		  (TACAS'12)},
+  note		= {To appear}
+}
+
 @InProceedings{	  beer.01.cav,
   author	= {Ilan Beer and Shoham Ben-David and Cindy Eisner and Dana
 		  Fisman and Anna Gringauze and Yoav Rodeh},

doc/tl/tl.tex

@@ -1472,8 +1472,8 @@ implication can be done in two ways:
 
 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|ltl_simplifier_options::containment_checks_stronger|''
+Additionally, implications denoted by $f\Simp g$ are only checked if
+the ``\verb|ltl_simplifier_options::containment_checks_stronger|''
 option is set (otherwise the rewriting rule is not applied).
 
 \begin{equation*}
@@ -1487,23 +1487,36 @@ option is set (otherwise the rewriting rule is not applied).
 \text{if}& (\NOT f)\simp g &\text{then}& f\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 \\
+\text{if}& f\simp h        &\text{then}& f\U (g \R (h \U k)) &\equiv g \R (h \U k) \\
+\text{if}& f\simp h        &\text{then}& f\U (g \R (h \W k)) &\equiv g \R (h \W k) \\
+\text{if}& f\simp h        &\text{then}& f\U (g \M (h \U k)) &\equiv g \M (h \U k) \\
+\text{if}& f\simp h        &\text{then}& f\U (g \M (h \W k)) &\equiv g \M (h \W k) \\
 \text{if}& f\simp g        &\text{then}& f\W g &\equiv g \\
 \text{if}& (f\W g)\Simp g  &\text{then}& f\W g &\equiv g \\
 \text{if}& (\NOT f)\simp g &\text{then}& f\W g &\equiv \1 \\
 \text{if}& f\simp g        &\text{then}& f\W (g \W h) &\equiv g \W h \\
+\text{if}& g\simp f        &\text{then}& f\W (g \U h) &\equiv f \W h \\
+\text{if}& g\simp f        &\text{then}& f\W (g \W h) &\equiv f \W 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}& 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 \\
+\text{if}& h\simp f        &\text{then}& (f\R g) \R h &\equiv g \R h \\
+\text{if}& h\simp f        &\text{then}& (f\M g) \R h &\equiv g \R h \\
 \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 \\
 \text{if}& g\simp f        &\text{then}& f\M (g \M h) &\equiv g \M h \\
 \text{if}& f\simp g        &\text{then}& f\M (g \M h) &\equiv f \M h \\
 \text{if}& f\simp g        &\text{then}& f\M (g \R h) &\equiv f \M h \\
+\text{if}& h\simp f        &\text{then}& (f\M g) \M h &\equiv g \M h \\
 \end{array}
 \end{equation*}
 
+The above rules were collected from various
+sources~\cite{somenzi.00.cav,tauriainen.03.a83,babiak.12.tacas} and
+sometimes generalized to support operators such as $\M$ and $\W$.
 
 \appendix
 \chapter{Syntactic Implications}\label{ann:syntimpl}

src/ltltest/reduccmp.test

-#! /bin/sh
-# Copyright (C) 2009, 2010, 2011 Laboratoire de Recherche et Developpement
+ #! /bin/sh
+# Copyright (C) 2009, 2010, 2011, 2012 Laboratoire de Recherche et Developpement
 # de l'Epita (LRDE).
 # Copyright (C) 2004, 2006 Laboratoire d'Informatique de Paris 6 (LIP6),
 # dpartement Systmes Rpartis Coopratifs (SRC), Universit Pierre
@@ -174,6 +174,20 @@ for x in ../reduccmp ../reductaustr; do
      run 0 $x '(a & b) M (a R c)' '(a & b)M c'
      run 0 $x '(a & b) M (a M c)' '(a & b)M c'
 
+     run 0 $x 'a U ((a & b) U c)' 'a U c'
+     run 0 $x '(a&c) U (b R (c U d))' 'b R (c U d)'
+     run 0 $x '(a&c) U (b R (c W d))' 'b R (c W d)'
+     run 0 $x '(a&c) U (b M (c U d))' 'b M (c U d)'
+     run 0 $x '(a&c) U (b M (c W d))' 'b M (c W d)'
+
+     run 0 $x '(a R c) R (b & a)' 'c R (b & a)'
+     run 0 $x '(a M c) R (b & a)' 'c R (b & a)'
+
+     run 0 $x 'a W ((a&b) U c)' 'a W c'
+     run 0 $x 'a W ((a&b) W c)' 'a W c'
+
+     run 0 $x '(a M c) M (b&a)' 'c M (b&a)'
+
      # Eventuality and universality class reductions
      run 0 $x 'Fa M b' 'Fa & b'
      run 0 $x 'GFa M b' 'GFa & b'

src/ltlvisit/simplify.cc

@@ -1272,9 +1272,16 @@ namespace spot
 		    }
 		  // if a => b, then a U (b U c) = (b U c)
 		  // if a => b, then a U (b W c) = (b W c)
+		  // if b => a, then a U (b U c) = (a U c)
+		  // if a => c, then a U (b R (c U d)) = (b R (c U d))
+		  // if a => c, then a U (b R (c W d)) = (b R (c W d))
+		  // if a => c, then a U (b M (c U d)) = (b M (c U d))
+		  // if a => c, then a U (b M (c W d)) = (b M (c W d))
 		  if (b->kind() == formula::BinOp)
 		    {
 		      binop* bo = static_cast<binop*>(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)
 		      if ((bo->op() == binop::U || bo->op() == binop::W)
 			  && c_->implication(a, bo->first()))
 			{
@@ -1282,6 +1289,32 @@ namespace spot
 			  result_ = b;
 			  return;
 			}
+		      // if b => a, then a U (b U c) = (a U c)
+		      if (bo->op() == binop::U
+			  && c_->implication(bo->first(), a))
+			{
+			  result_ = recurse_destroy
+			    (binop::instance(binop::U,
+					     a, bo->second()->clone()));
+			  b->destroy();
+			  return;
+			}
+		      // if a => c, then a U (b R (c U d)) = (b R (c U d))
+		      // if a => c, then a U (b R (c W d)) = (b R (c W d))
+		      // if a => c, then a U (b M (c U d)) = (b M (c U d))
+		      // if a => c, then a U (b M (c W d)) = (b M (c W d))
+		      if ((bo->op() == binop::R || bo->op() == binop::M)
+			  && bo->second()->kind() == formula::BinOp)
+			{
+			  binop* cd = static_cast<binop*>(bo->second());
+			  if ((cd->op() == binop::U || cd->op() == binop::W)
+			      && c_->implication(a, cd->first()))
+			    {
+			      a->destroy();
+			      result_ = b;
+			      return;
+			    }
+			}
 		    }
 		  break;
 
@@ -1317,13 +1350,30 @@ namespace spot
 		      if (bo->op() == binop::R
 			  && c_->implication(a, bo->first()))
 			{
-			  b->destroy();
 			  result_ = recurse_destroy
 			    (binop::instance(binop::R, a,
 					     bo->second()->clone()));
+			  b->destroy();
+			  return;
+			}
+		    }
+		  if (a->kind() == formula::BinOp)
+		    {
+		      // if b => a then (a R c) R b = c R b
+		      // if b => a then (a M c) R b = c R b
+		      binop* bo = static_cast<binop*>(a);
+		      if ((bo->op() == binop::R || bo->op() == binop::M)
+			  && c_->implication(b, bo->first()))
+			{
+			  result_ = recurse_destroy
+			    (binop::instance(binop::R,
+					     bo->second()->clone(),
+					     b));
+			  a->destroy();
 			  return;
 			}
 		    }
+
 		  break;
 
 		case binop::W:
@@ -1347,9 +1397,12 @@ namespace spot
 		    }
 		  // if a => b, then a W (b W c) = (b W c)
 		  // (Beware: even if a => b we do not have a W (b U c) = b U c)
+		  // if b => a, then a W (b U c) = (a W c)
+		  // if b => a, then a W (b W c) = (a W c)
 		  if (b->kind() == formula::BinOp)
 		    {
 		      binop* bo = static_cast<binop*>(b);
+		      // if a => b, then a W (b W c) = (b W c)
 		      if (bo->op() == binop::W
 			  && c_->implication(a, bo->first()))
 			{
@@ -1357,6 +1410,17 @@ namespace spot
 			  result_ = b;
 			  return;
 			}
+		      // if b => a, then a W (b U c) = (a W c)
+		      // if b => a, then a W (b W c) = (a W c)
+		      if ((bo->op() == binop::U || bo->op() == binop::W)
+			  && c_->implication(bo->first(), a))
+			{
+			  result_ = recurse_destroy
+			    (binop::instance(binop::W,
+					     a, bo->second()->clone()));
+			  b->destroy();
+			  return;
+			}
 		    }
 		  break;
 
@@ -1400,6 +1464,21 @@ namespace spot
 			  return;
 			}
 		    }
+		  if (a->kind() == formula::BinOp)
+		    {
+		      // if b => a then (a M c) M b = c M b
+		      binop* bo = static_cast<binop*>(a);
+		      if (bo->op() == binop::M
+			  && c_->implication(b, bo->first()))
+			{
+			  result_ = recurse_destroy
+			    (binop::instance(binop::M,
+					     bo->second()->clone(),
+					     b));
+			  a->destroy();
+			  return;
+			}
+		    }
 		  break;
 		}
 	      trace << "bo: no inclusion-based rules matched" << std::endl;