Add 11 implication-based simplification rules for U,W,R,M.

* src/ltlvisit/simplify.cc: Add them.
* src/ltltest/reduccmp.test: Check them.
* doc/tl/tl.tex: Document them.

doc/tl/tl.tex

@@ -1599,12 +1599,19 @@ option is set (otherwise the rewriting rule is not applied).
 \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 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}& 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}& f\simp h        &\text{then}& (f\U g) \W h &\equiv g \W h \\
+\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 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 \\
@@ -1612,12 +1619,16 @@ option is set (otherwise the rewriting rule is not applied).
 \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 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}& 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 \\
+\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 \\
 \end{array}
 \end{equation*}
 

src/ltltest/reduccmp.test

@@ -229,6 +229,25 @@ for x in ../reduccmp ../reductaustr; do
 
      run 0 $x '(a M c) M (b&a)' 'c M (b&a)'
 
+     run 0 $x '((a&c) U b) U c' 'b U c'
+     run 0 $x '((a&c) W b) U c' 'b U c'
+     run 0 $x '((a&c) U b) W c' 'b W c'
+     run 0 $x '((a&c) W b) W c' 'b W c'
+     run 0 $x '(a R b) R (c&a)' 'b R (c&a)'
+     run 0 $x '(a M b) R (c&a)' 'b R (c&a)'
+     run 0 $x '(a R b) M (c&a)' 'b M (c&a)'
+     run 0 $x '(a M b) M (c&a)' 'b M (c&a)'
+
+     run 0 $x '(a R (b&c)) R (c)' '(a&b&c) R c'
+     run 0 $x '(a M (b&c)) R (c)' '(a&b&c) R c'
+     run 0 $x '(a R (b&c)) M (c)' '(a R (b&c)) M (c)' # not reduced
+     run 0 $x '(a M (b&c)) M (c)' '(a&b&c) M c'
+     run 0 $x '(a W (c&b)) W b' '(a W (c&b)) | b'
+     run 0 $x '(a U (c&b)) W b' '(a U (c&b)) | b'
+     run 0 $x '(a U (c&b)) U b' '(a U (c&b)) | b'
+     run 0 $x '(a W (c&b)) U b' '(a W (c&b)) U b' # not reduced
+
+
      # 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

@@ -1848,6 +1848,29 @@ namespace spot
 			    }
 			}
 		    }
+		  // if a => b, then (a U c) U b = c U b
+		  // if a => b, then (a W c) U b = c U b
+		  // if c => b, then (a U c) U b = (a U c) | b
+		  if (const binop* bo = is_binop(a))
+		    {
+		      if ((bo->op() == binop::U || bo->op() == binop::W)
+			  && c_->implication(bo->first(), b))
+			{
+			  result_ = recurse_destroy
+			    (binop::instance(binop::U,
+					     bo->second()->clone(),
+					     b));
+			  a->destroy();
+			  return;
+			}
+		      else if ((bo->op() == binop::U)
+			       && c_->implication(bo->second(), b))
+			{
+			  result_ = recurse_destroy
+			    (multop::instance(multop::Or, a, b));
+			  return;
+			}
+		    }
 		  break;
 
 		case binop::R:
@@ -1889,20 +1912,35 @@ namespace spot
 			  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
+		  // if c => b, then (a R c) R b = (a & c) R b
+		  // if c => b, then (a M c) R b = (a & c) R b
+		  if (const binop* bo = is_binop(a))
 		    {
-		      // if b => a then (a R c) R b = c R b
+		      if (bo->op() == binop::M || bo->op() == binop::R)
-		      // if b => a then (a M c) R b = c R b
-		      const binop* bo = static_cast<const binop*>(a);
-		      if ((bo->op() == binop::R || bo->op() == binop::M)
-			  && c_->implication(b, bo->first()))
 			{
-			  result_ = recurse_destroy
+			  if (c_->implication(b, bo->first()))
-			    (binop::instance(binop::R,
+			    {
-					     bo->second()->clone(),
+			      result_ = recurse_destroy
-					     b));
+				(binop::instance(binop::R,
-			  a->destroy();
+						 bo->second()->clone(),
-			  return;
+						 b));
+			      a->destroy();
+			      return;
+			    }
+			  else if (c_->implication(bo->second(), b))
+			    {
+			      const formula* ac =
+				multop::instance(multop::And,
+						 bo->first()->clone(),
+						 bo->second()->clone());
+			      a->destroy();
+			      result_ = recurse_destroy
+				(binop::instance(binop::R, ac, b));
+			      return;
+			    }
 			}
 		    }
 
@@ -1954,6 +1992,31 @@ namespace spot
 			  return;
 			}
 		    }
+		  // if a => b, then (a U c) W b = c W b
+		  // if a => b, then (a W c) W b = c W b
+		  // if c => b, then (a W c) W b = (a W c) | b
+		  // if c => b, then (a U c) W b = (a U c) | b
+		  if (const binop* bo = is_binop(a))
+		    {
+		      if ((bo->op() == binop::U || bo->op() == binop::W))
+			{
+			  if (c_->implication(bo->first(), b))
+			    {
+			      result_ = recurse_destroy
+				(binop::instance(binop::W,
+						 bo->second()->clone(),
+						 b));
+			      a->destroy();
+			      return;
+			    }
+			  else if (c_->implication(bo->second(), b))
+			    {
+			      result_ = recurse_destroy
+				(multop::instance(multop::Or, a, b));
+			      return;
+			    }
+			}
+		    }
 		  break;
 
 		case binop::M:
@@ -1996,11 +2059,13 @@ namespace spot
 			  return;
 			}
 		    }
-		  if (a->kind() == formula::BinOp)
+
+		  // if b => a, then (a R c) M b = c M b
+		  // if b => a, then (a M c) M b = c M b
+		  // if c => b, then (a M c) M b = (a & c) M b
+		  if (const binop* bo = is_binop(a))
 		    {
-		      // if b => a then (a M c) M b = c M b
+		      if ((bo->op() == binop::M || bo->op() == binop::R)
-		      const binop* bo = static_cast<const binop*>(a);
-		      if (bo->op() == binop::M
 			  && c_->implication(b, bo->first()))
 			{
 			  result_ = recurse_destroy
@@ -2010,6 +2075,18 @@ namespace spot
 			  a->destroy();
 			  return;
 			}
+		      else if ((bo->op() == binop::M)
+			       && c_->implication(bo->second(), b))
+			{
+			  const formula* ac =
+			    multop::instance(multop::And,
+					     bo->first()->clone(),
+					     bo->second()->clone());
+			  a->destroy();
+			  result_ = recurse_destroy
+			    (binop::instance(binop::M, ac, b));
+			  return;
+			}
 		    }
 		  break;
 		}