unabbreviate: enable removal of R

This implies learning alternative rules for G, and W as well, since
those would use R.

Fixes #103.  Suggested by Joachim Klein.

* src/ltlvisit/unabbrev.cc, src/ltlvisit/unabbrev.hh: Implement the
new rules.
* doc/tl/tl.tex: Document the rules.
* src/tests/unabbrevwm.test: Test them.
* src/bin/ltlfilt.cc, NEWS: Mention that --unabbreviate accepts R.

NEWS

@@ -13,8 +13,9 @@ New in spot 1.99.2a (not yet released)
   * All the unabbreviation functions (unabbreviate_ltl(),
     unabbreviate_logic(), unabbreviate_wm()) have been merged into a
     single unabbreviate() function that takes a string representing
-    the list of rewritting rules to enable.  This function is also
+    the list of operators to remove among "eFGiMRW^" where 'e', 'i',
-    available via ltlfilt --unabbreviate.
+    and '^' stand respectively for <->, ->, and xor.
+    This feature is also available via ltlfilt --unabbreviate.
 
   * In LTL formulas, atomic propositions specified using double-quotes
     can now include \" and \\.  (This is more consistent with the HOA

doc/tl/tl.tex

@@ -1262,19 +1262,25 @@ occurrences of $\XOR$, $\EQUIV$ and $\IMPLIES$.
 ``\texttt{\^{}e}" & f\XOR g &\equiv&  (f\AND\NOT g)\OR (g\AND\NOT f)\\
 ``\texttt{\^{}}"\text{~without~}``\texttt{e}" & f\XOR g &\equiv&  \NOT(f\EQUIV g)\\
 ``\texttt{F}" & \F f&\equiv& \1\U f\\
-``\texttt{G}" & \G f&\equiv& \0\R f \\
+``\texttt{G}"\text{~without~}``\texttt{R}" & \G f&\equiv& \0\R f \\
-``\texttt{W}" & f \W g&\equiv& g \R (g \OR f)\\
+``\texttt{GR}"\text{~without~}``\texttt{W}" & \G f&\equiv& f \W \0 \\
-``\texttt{M}" & f \M g&\equiv& g \U (g \AND f)
+``\texttt{GRW}" & \G f&\equiv& \NOT\F\NOT f \\
+``\texttt{M}" & f \M g&\equiv& g \U (g \AND f) \\
+``\texttt{R}"\text{~without~}``\texttt{W}" & f \R g&\equiv&  g\W (f \AND g)\\
+``\texttt{RW}" & f \R g&\equiv&  g\U ((f \AND g) \OR \G g) \\
+``\texttt{W}"\text{~without~}``\texttt{R}" & f \W g&\equiv& g \R (g \OR f)\\
+``\texttt{WR}" & f \W g&\equiv& f \U (g \OR \G f)\\
 \end{array}
 \]
 
 Among all the possible rewritings (see Appendix~\ref{sec:ltl-equiv})
-for $\W$ and $\M$, those two were chosen because they are easier to
+the default rules for $\R$, $\W$ and $\M$, those were chosen because
-translate in a tableau construction~\cite[Fig.~11]{duret.11.vecos}.
+they are easier to translate in a tableau
+construction~\cite[Fig.~11]{duret.11.vecos}.
 
 Besides the `\verb=unabbreviate()=' function, there is also a class
-`\verb=unabbreviator()= that implement the same functionality, but
+`\verb=unabbreviator()= that implements the same functionality, but
-maintain a cache of abbreviated subformulas.  This is preferable if
+maintains a cache of abbreviated subformulas.  This is preferable if
 you plan to abbreviate many formulas sharing identical subformulas.
 
 \section{LTL simplifier}

src/bin/ltlfilt.cc

@@ -129,9 +129,9 @@ static const argp_option options[] =
       0 },
     { "unabbreviate", OPT_UNABBREVIATE, "STR", OPTION_ARG_OPTIONAL,
       "remove all occurrences of the operators specified by STR, which "
-      "must be a substring of \"eFGiMW^\", where 'e', 'i', and '^' stand "
+      "must be a substring of \"eFGiMRW^\", where 'e', 'i', and '^' stand "
-      "respectively for <->, ->, and xor.  If no argument is passed, all "
+      "respectively for <->, ->, and xor.  If no argument is passed, "
-      "rewriting rules are applied.", 0 },
+      "the subset \"eFGiMW^\" is used.", 0 },
     { "exclusive-ap", OPT_EXCLUSIVE_AP, "AP,AP,...", 0,
       "if any of those APs occur in the formula, add a term ensuring "
       "two of them may not be true at the same time.  Use this option "

src/ltlvisit/unabbrev.cc

@@ -51,6 +51,9 @@ namespace spot
 	    re_m_ = true;
 	    re_some_other_ = true;
 	    break;
+	  case 'R':
+	    re_r_ = true;
+	    re_some_other_ = true;
 	  case 'W':
 	    re_w_ = true;
 	    re_some_other_ = true;
@@ -109,18 +112,44 @@ namespace spot
 	    auto c = run(uo->child());
 	    switch (auto op = uo->op())
 	      {
-		//  F f1 = true U f1
+		//  F f = true U f
 	      case unop::F:
 		if (!re_f_)
 		  goto unop_clone;
 		out = binop::instance(binop::U, constant::true_instance(), c);
 		break;
-		//  G f1 = false R f1
+		//  G f = false R f
+		//  G f = f W false
+		//  G f = !F!f
+		//  G f = !(true U !f)
 	      case unop::G:
 		if (!re_g_)
 		  goto unop_clone;
-		out = binop::instance(binop::R, constant::false_instance(), c);
+		if (!re_r_)
-		break;
+		  {
+		    out = binop::instance(binop::R,
+					  constant::false_instance(), c);
+		    break;
+		  }
+		if (!re_w_)
+		  {
+		    out = binop::instance(binop::W,
+					  c, constant::false_instance());
+		    break;
+		  }
+		{
+		  auto nc = unop::instance(unop::Not, c);
+		  if (!re_f_)
+		    {
+		      out = unop::instance(unop::Not,
+					   unop::instance(unop::F, nc));
+		      break;
+		    }
+		  auto u = binop::instance(binop::U,
+					   constant::true_instance(), nc);
+		  out = unop::instance(unop::Not, u);
+		  break;
+		}
 	      case unop::Not:
 	      case unop::X:
 	      case unop::Closure:
@@ -182,12 +211,29 @@ namespace spot
 		  break;
 		}
 		// f1 W f2 = f2 R (f2 | f1)
+		// f1 W f2 = f1 U (f2 | G f1)
+		// f1 W f2 = f1 U (f2 | !F !f1)
+		// f1 W f2 = f1 U (f2 | !(1 U !f1))
 	      case binop::W:
 		if (!re_w_)
 		  goto binop_clone;
-		out = binop::instance(binop::R, f2,
+		if (!re_r_)
-				      multop::instance(multop::Or,
+		  {
-						       f2->clone(), f1));
+		    out = binop::instance(binop::R, f2,
+					  multop::instance(multop::Or,
+							   f2->clone(), f1));
+		    break;
+		  }
+		f1->clone();
+		out = unop::instance(unop::G, f1);
+		if (re_g_)
+		  {
+		    auto tmp = out;
+		    out = run(out);
+		    tmp->destroy();
+		  }
+		out = binop::instance(binop::U, f1,
+				      multop::instance(multop::Or, f2, out));
 		break;
 		// f1 M f2 = f2 U (g2 & f1)
 	      case binop::M:
@@ -197,8 +243,32 @@ namespace spot
 				      multop::instance(multop::And,
 						       f2->clone(), f1));
 		break;
-	      case binop::U:
+		// f1 R f2 = f2 W (f1 & f2)
+		// f1 R f2 = f2 U ((f1 & f2) | Gf2)
+		// f1 R f2 = f2 U ((f1 & f2) | !F!f2)
+		// f1 R f2 = f2 U ((f1 & f2) | !(1 U !f2))
 	      case binop::R:
+		if (!re_r_)
+		  goto binop_clone;
+		{
+		  auto f12 = multop::instance(multop::And, f1, f2->clone());
+		  if (!re_w_)
+		    {
+		      out = binop::instance(binop::W, f2, f12);
+		      break;
+		    }
+		  out = unop::instance(unop::G, f2->clone());
+		  if (re_g_)
+		    {
+		      auto tmp = out;
+		      out = run(tmp);
+		      tmp->destroy();
+		    }
+		  out = binop::instance(binop::U, f2,
+					multop::instance(multop::Or, f12, out));
+		}
+		break;
+	      case binop::U:
 	      case binop::UConcat:
 	      case binop::EConcat:
 	      case binop::EConcatMarked:

src/ltlvisit/unabbrev.hh

@@ -40,11 +40,12 @@ namespace spot
       bool re_g_ = false;
       bool re_i_ = false;
       bool re_m_ = false;
+      bool re_r_ = false;
       bool re_w_ = false;
       bool re_xor_ = false;
       bool re_some_bool_ = false;	// rewrite xor, i, or e
       bool re_some_f_g_ = false;	// rewrite F or G
-      bool re_some_other_ = false;	// rewrite W or M
+      bool re_some_other_ = false;	// rewrite W, M, or R
       // Cache of rewritten subformulas
       std::unordered_map<const formula*, const formula*> cache_;
     public:

src/tests/unabbrevwm.test

@@ -25,8 +25,10 @@
 
 set -e
 
+ltlfilt=../../bin/ltlfilt
+
 # Removing W,M in this formula caused a segfault at some point.
-run 0 ../../bin/ltlfilt --remove-wm >out <<EOF
+run 0 $ltlfilt --remove-wm >out <<EOF
 (!((G(p0)) U ((F(p0)) M ((F(X(p1))) & ((p2) W (G(p2))))))) M (F(p0))
 (Fp0 U(Fp0&!(Gp0 U((FXp1 &(Gp2 R(p2|Gp2))) U(Fp0&FXp1&(Gp2 R(p2|Gp2)))))))
 EOF
@@ -34,3 +36,11 @@ EOF
 # The first formula will be simplified to the second, so after uniq
 # the output should have one line.
 test `uniq out | wc -l` = 1
+
+for i in 'GFa' 'a R b' 'a W b' 'a M b'; do
+    for fg in '' F G GF; do
+	for rwm in '' R W M RW RM WM RWM; do
+	    $ltlfilt -f "$i" --unabbrev=$fg$rwm --equivalent-to "$i"
+	done
+    done
+done