Rewrite "(Xc) M b" as "b & X(b U c)", plus three similar rules.

* src/ltlvisit/simplify.hh (ltl_simplifier_options): New option
reduce_size_stricly.
* src/ltlvisit/simplify.cc (simplify_visitor): Implement these
rules.
* src/ltltest/reduc.cc: Check with reduce_size_strictly unset or
set, but only use the latter result to check sizes.
* src/ltltest/reduccmp.test: Test them.
* doc/tl/tl.tex: Document them.

doc/tl/tl.tex

@@ -96,6 +96,9 @@
 \newcommand{\nsere}[1]{\texttt{!\{}#1\texttt{\}}}
 \newcommand{\seren}[1]{\texttt{\{}#1\texttt{\}!}}
 
+% rewriting rules that enlarge the formula
+\newcommand{\equiV}{\stackrel{\star}{\equiv}}
+
 \def\limplies{\rightarrow}
 \def\simp{\rightrightharpoons}
 \def\Simp{\stackrel{+}{\simp}}
@@ -1088,11 +1091,11 @@ presented by~\citet{chang.92.icalp}, but other presentations have been
 done including negation~\citep{cerna.03.mfcs} and weak
 until~\citep{schneider.01.lpar}.
 
-The following grammar rules describes extend the aforementioned
+The following grammar rules extend the aforementioned work slightly by
-work slightly by dealing with PSL operators.  These are the
+dealing with PSL operators.  These are the rules used by Spot to
-rules used by Spot to decide upon
+decide upon construction to which class a formula belongs (see the
-construction to which class a formula belongs (see the methods
+methods \texttt{is\_syntactic\_safety()},
-\texttt{is\_syntactic\_safety()}, \texttt{is\_syntactic\_guarantee()},
+\texttt{is\_syntactic\_guarantee()},
 \texttt{is\_syntactic\_obligation()},
 \texttt{is\_syntactic\_recurrence()}, and
 \texttt{is\_syntactic\_persistence()} listed on
@@ -1231,12 +1234,12 @@ Section~\ref{sec:unabbbool}.  Therefore it is never necessary to apply
 `\verb|ltl_simplifier::negative_normal_form|`.
 
 If the option `\verb|nenoform_stop_on_boolean|' is set, the above
-recursive rewritings will not be applied to subformul\ae{} that are
+recursive rewritings are not applied to Boolean subformul\ae{}.  For
-Boolean formul\ae.  For instance calling
+instance calling `\verb|ltl_simplifier::negative_normal_form|` on
-`\verb|ltl_simplifier::negative_normal_form|` on $\NOT\F\G(a \XOR b)$
+$\NOT\F\G(a \XOR b)$ will produce $\G\F(((\NOT a)\AND(\NOT
-will produce $\G\F(((\NOT a)\AND(\NOT b))\OR(a\AND b))$ if
+b))\OR(a\AND b))$ if `\verb|nenoform_stop_on_boolean|' is unset, while
-`\verb|nenoform_stop_on_boolean|' is unset, while it will produce
+it will produce $\G\F(\NOT(a \XOR b))$ if
-$\G\F(\NOT(a \XOR b))$ if `\verb|nenoform_stop_on_boolean|' is set.
+`\verb|nenoform_stop_on_boolean|' is set.
 
 \section{Simplifications}
 
@@ -1264,7 +1267,11 @@ The goals in most of these simplification are to:
 \subsection{Basic Simplifications}
 
 These simplifications are enabled with
-\verb|ltl_simplifier_options::reduce_basics|'.
+\verb|ltl_simplifier_options::reduce_basics|'.  A couple of them may
+enlarge the size of the formula: they are denoted using $\equiV$
+instead of $\equiv$, and they can be disabled by setting the
+\verb|ltl_simplifier_options::reduce_size_strictly|' option to
+\texttt{true}.
 
 \subsubsection{Basic Simplifications for Temporal Operators}
 \label{sec:basic-simp-ltl}
@@ -1280,20 +1287,24 @@ from left to right, as usual):
   \G(f_1\OR\ldots\OR f_n \OR \G\F(g_1)\OR\ldots\OR \G\F(g_m)) & \equiv \G(f_1\OR\ldots\OR f_n)\OR \G\F(g_1\OR\ldots\OR g_m)
 \end{align*}
 
-Note that the latter rewriting rules for $\G$ has no dual:
+Note that the latter three rewriting rules for $\G$ have no dual:
-rewriting $\F(f \AND \G\F g)$ to $\F(f) \AND \G\F(g)$ (instance as
+rewriting $\F(f \AND \G\F g)$ to $\F(f) \AND \G\F(g)$ (as suggested
-suggested by~\citet{somenzi.00.cav}) goes against our goal of moving
+by~\citet{somenzi.00.cav}) goes against our goal of moving the $\F$
-the $\F$ operator in front of the formula.  Conceptually, it is also
+operator in front of the formula.  Conceptually, it is also easier to
-easier to understand $\F(f \AND \G\F g)$: has long as $f$ has not been
+understand $\F(f \AND \G\F g)$: has long as $f$ has not been verified,
-verified, there is no need to worry about the $\G\F g$ term.
+there is no need to worry about the $\G\F g$ term.
+
+Here are the basic rewriting rules for binary operators (excluding
+$\OR$ and $\AND$ which are considered in Spot as $n$-ary operators).
+$b$ denotes a Boolean formula.
 
-Here are the basic rewriting rules for binary operators (excluding $\OR$ and
-$\AND$ which are considered in Spot as $n$-ary operators):
 \begin{align*}
   \1 \U f             & \equiv \F f            & f \W \0             & \equiv \G f            \\
   f \M \1             & \equiv \F f            & \0 \R f             & \equiv \G f            \\
   (\X f)\U (\X g)     & \equiv \X(f\U g)       & (\X f)\W(\X g)      & \equiv \X(f\W g)       \\
   (\X f)\M (\X g)     & \equiv \X(f\M g)       & (\X f)\R(\X g)      & \equiv \X(f\R g)       \\
+  (\X f)\U b          & \equiV b\OR \X(b\M f)  & (\X f)\W b          & \equiV b\OR \X(f\R b)  \\
+  (\X f)\M b          & \equiV b\AND \X(b\U f) & (\X f)\R b          & \equiV b\AND \X(f\W b) \\
   f \U(\G f)          & \equiv \G f            & f \W(\G f)          & \equiv \G f            \\
   f \M(\F f)          & \equiv \F f            & f \R(\F f)          & \equiv \F f            \\
   f \U (g \OR \G(f))  & \equiv f\W g           & f \W (g \OR \G(f))  & \equiv f\W g           \\
@@ -1341,7 +1352,7 @@ The above rules are applied even if more terms are presents in the
 operator's arguments.  For instance $\F\G(a)\AND \G(b) \AND \F\G(c) \AND
 \X(d)$ will be rewritten as $\X(d \AND \F\G(a\AND c))\AND \G(b)$.
 
-The following more complicated rules are generalization of $f\AND
+The following more complicated rules are generalizations of $f\AND
 \X\G f\equiv \G f$ and $f\OR \X\F f\equiv \F f$:
 \begin{align*}
   f\AND \X(\G(f\AND g\ldots)\AND h\ldots) &\equiv \G(f) \AND \X(\G(g\ldots)\AND h\ldots) \\
@@ -1351,7 +1362,7 @@ The latter rule for $f\OR \X(\F(f)\OR h\ldots)$ is only applied if all
 $\F$-formul\ae{} can be removed from the argument of $\X$ with the
 rewriting.  For instance $a \OR b \OR c\OR \X(\F(a\OR b)\OR \F(c)\OR \G d)$
 will be rewritten to $\F(a \OR b \OR c) \OR \X\G d$ but
-$b \OR c\OR \X(\F(a\OR b)\OR \F(c)\OR \G d)$ would only become
+$b \OR c\OR \X(\F(a\OR b)\OR \F(c)\OR \G d)$ will only become
 $b \OR c\OR \X(\F(a\OR b\OR c)\OR \G d)$.
 
 Finally the following rule is applied only when no other terms are present
@@ -1503,6 +1514,7 @@ sometimes generalized to support operators such as $\M$ and $\W$.
 
 \appendix
 \chapter{Defining LTL with only one of $\U$, $\W$, $\R$, or $\M$}
+\label{sec:ltl-equiv}
 
 The operators \samp{F}, \samp{G}, \samp{U}, \samp{R}, \samp{M}, and
 \samp{W} can all be defined using only Boolean operators, \samp{X},

src/ltltest/reduc.cc

@@ -1,5 +1,5 @@
-// Copyright (C) 2008, 2009, 2010, 2011 Laboratoire de Recherche et
+// Copyright (C) 2008, 2009, 2010, 2011, 2012 Laboratoire de Recherche
-// Développement de l'Epita (LRDE).
+// et Développement de l'Epita (LRDE).
 // Copyright (C) 2004, 2006, 2007 Laboratoire d'Informatique de Paris
 // 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
 // Université Pierre et Marie Curie.
@@ -141,6 +141,8 @@ main(int argc, char** argv)
   }
 
   spot::ltl::ltl_simplifier* simp = new spot::ltl::ltl_simplifier(o);
+  o.reduce_size_strictly = true;
+  spot::ltl::ltl_simplifier* simp_size = new spot::ltl::ltl_simplifier(o);
 
   spot::ltl::formula* f1 = 0;
   spot::ltl::formula* f2 = 0;
@@ -202,24 +204,35 @@ main(int argc, char** argv)
     spot::ltl::formula* ftmp1;
 
     ftmp1 = f1;
-    f1 = simp->negative_normal_form(f1, false);
+    f1 = simp_size->negative_normal_form(f1, false);
     ftmp1->destroy();
 
     int length_f1_before = spot::ltl::length(f1);
     std::string f1s_before = spot::ltl::to_string(f1);
 
-    ftmp1 = f1;
+    spot::ltl::formula* input_f = f1;
-    f1 = simp->simplify(f1);
+    f1 = simp_size->simplify(input_f);
-
+    if (!simp_size->are_equivalent(input_f, f1))
-    if (!simp->are_equivalent(ftmp1, f1))
       {
 	std::cerr << "Incorrect reduction from `" << f1s_before
 		  << "' to `" << spot::ltl::to_string(f1) << "'."
 		  << std::endl;
 	exit_code = 3;
       }
+    else
+      {
+	spot::ltl::formula* maybe_larger = simp->simplify(input_f);
+	if (!simp->are_equivalent(input_f, maybe_larger))
+	  {
+	    std::cerr << "Incorrect reduction (reduce_size_strictly=0) from `"
+		      << f1s_before << "' to `" << spot::ltl::to_string(f1)
+		      << "'." << std::endl;
+	    exit_code = 3;
+	  }
+	maybe_larger->destroy();
+      }
 
-    ftmp1->destroy();
+    input_f->destroy();
 
     int length_f1_after = spot::ltl::length(f1);
     std::string f1s_after = spot::ltl::to_string(f1);
@@ -228,7 +241,7 @@ main(int argc, char** argv)
     if (f2)
       {
 	ftmp1 = f2;
-	f2 = simp->negative_normal_form(f2, false);
+	f2 = simp_size->negative_normal_form(f2, false);
 	ftmp1->destroy();
 	f2s = spot::ltl::to_string(f2);
       }
@@ -282,6 +295,7 @@ main(int argc, char** argv)
   }
  end:
 
+  delete simp_size;
   delete simp;
 
   if (fin)

src/ltltest/reduccmp.test

@@ -1,6 +1,6 @@
 #! /bin/sh
-# Copyright (C) 2009, 2010, 2011, 2012 Laboratoire de Recherche et Developpement
+# Copyright (C) 2009, 2010, 2011, 2012 Laboratoire de Recherche et
-# de l'Epita (LRDE).
+# 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
 # et Marie Curie.
@@ -105,6 +105,13 @@ for x in ../reduccmp ../reductaustr; do
      run 0 $x 'Xa & Xb' 'X(a & b)'
      run 0 $x 'Xa | Xb' 'X(a | b)'
 
+     run 0 $x 'X(a) M X(b)' 'X(a M b)'
+     run 0 $x 'X(a) W X(b)' 'X(a W b)'
+     run 0 $x 'X(a) M b' 'b & X(b U a)'
+     run 0 $x 'X(a) R b' 'b & X(b W a)'
+     run 0 $x 'X(a) U b' 'b | X(b M a)'
+     run 0 $x 'X(a) W b' 'b | X(b R a)'
+
      run 0 $x '(a U b) & (c U b)' '(a & c) U b'
      run 0 $x '(a R b) & (a R c)' 'a R (b & c)'
      run 0 $x '(a U b) | (a U c)' 'a U (b | c)'

src/ltlvisit/simplify.cc

@@ -1747,6 +1747,24 @@ namespace spot
 			      }
 			  }
 		      }
+		    // If b is Boolean:
+		    // (Xc) U b = b | X(b M c)
+		    // (Xc) W b = b | X(b R c)
+		    if (!opt_.reduce_size_strictly
+			&& fu1 && fu1->op() == unop::X && b->is_boolean())
+		      {
+			formula* c = fu1->child()->clone();;
+			fu1->destroy();
+			formula* x =
+			  unop::instance(unop::X,
+					 binop::instance(op == binop::U
+							 ? binop::M
+							 : binop::R,
+							 b->clone(), c));
+			result_ =
+			  recurse_destroy(multop::instance(multop::Or, b, x));
+			return;
+		      }
 		  }
 		else if (op == binop::M || op == binop::R)
 		  {
@@ -1791,6 +1809,25 @@ namespace spot
 			      }
 			  }
 		      }
+
+		    // If b is Boolean:
+		    // (Xc) R b = b & X(b W c)
+		    // (Xc) M b = b & X(b U c)
+		    if (!opt_.reduce_size_strictly
+			&& fu1 && fu1->op() == unop::X && b->is_boolean())
+		      {
+			formula* c = fu1->child()->clone();;
+			fu1->destroy();
+			formula* x =
+			  unop::instance(unop::X,
+					 binop::instance(op == binop::M
+							 ? binop::U
+							 : binop::W,
+							 b->clone(), c));
+			result_ =
+			  recurse_destroy(multop::instance(multop::And, b, x));
+			return;
+		      }
 		  }
 	      }
 	    case binop::Xor:

src/ltlvisit/simplify.hh

@@ -1,5 +1,5 @@
-// Copyright (C) 2011 Laboratoire de Recherche et Developpement de
+// Copyright (C) 2011, 2012 Laboratoire de Recherche et Developpement
-// l'Epita (LRDE).
+// de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
 //
@@ -37,15 +37,15 @@ namespace spot
 			     bool event_univ = true,
 			     bool containment_checks = false,
 			     bool containment_checks_stronger = false,
-			     bool nenoform_stop_on_boolean = false)
+			     bool nenoform_stop_on_boolean = false,
+			     bool reduce_size_strictly = false)
 	: reduce_basics(basics),
 	  synt_impl(synt_impl),
 	  event_univ(event_univ),
 	  containment_checks(containment_checks),
 	  containment_checks_stronger(containment_checks_stronger),
-	  // If true, Boolean subformulae will not be put into
+	  nenoform_stop_on_boolean(nenoform_stop_on_boolean),
-	  // negative normal form.
+	  reduce_size_strictly(reduce_size_strictly)
-	  nenoform_stop_on_boolean(nenoform_stop_on_boolean)
       {
       }
 
@@ -57,6 +57,10 @@ namespace spot
       // If true, Boolean subformulae will not be put into
       // negative normal form.
       bool nenoform_stop_on_boolean;
+      // If true, some rules that produce slightly larger formulae
+      // will be disabled.  Those larger formulae are normally easier
+      // to translate, so we recommend to set this to false.
+      bool reduce_size_strictly;
     };
 
     // fwd declaration to hide technical details.