From 0821599db82f27b81ca19aa86b6ca724afdd2d3e Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Sun, 29 Apr 2012 23:36:12 +0200
Subject: [PATCH] Implement rewritings for {f|g} and !{f|g}.

* src/ltlvisit/simplify.cc: Here.
* src/ltltest/reduccmp.test: Test them.
* doc/tl/tl.tex: Document them.
---
 doc/tl/tl.tex             |  4 +++-
 src/ltltest/reduccmp.test |  2 ++
 src/ltlvisit/simplify.cc  | 16 ++++++++++++++++
 3 files changed, 21 insertions(+), 1 deletion(-)

diff --git a/doc/tl/tl.tex b/doc/tl/tl.tex
index 7a3739337..98ea090a9 100644
--- a/doc/tl/tl.tex
+++ b/doc/tl/tl.tex
@@ -1502,7 +1502,9 @@ Here are basic the rewritings for the weak closure and its negation:
   \sere{b\STAR{\mvar{i}..\mvar{j}};r}&\equiV \underbrace{b\AND \X(b\ldots}_{\mathclap{i\text{~occurences of~}b}}\AND\X\sere{b\STAR{\mvar{0}..\mvar{j-i}}\CONCAT r})&
   \nsere{b\STAR{\mvar{i}..\mvar{j}};r}&\equiV \underbrace{(\NOT b)\OR \X((\NOT b)\ldots}_{\mathclap{i\text{~occurences of~}\NOT b}}\OR\X\nsere{b\STAR{\mvar{0}..\mvar{j-i}}\CONCAT r}) \\
   \sere{b\STAR{\mvar{i}..\mvar{j}}}&\equiV \underbrace{b\AND \X(b\AND \X(\ldots b))}_{i\text{~occurences of~}b}&
-  \nsere{b\STAR{\mvar{i}..\mvar{j}}}&\equiV \underbrace{(\NOT b)\OR \X((\NOT b)\OR \X(\ldots(\NOT b)))}_{i\text{~occurences of~}\NOT b}
+  \nsere{b\STAR{\mvar{i}..\mvar{j}}}&\equiV \underbrace{(\NOT b)\OR \X((\NOT b)\OR \X(\ldots(\NOT b)))}_{i\text{~occurences of~}\NOT b}\\
+  \sere{r_1\OR r_2}&\equiV\sere{r_1}\OR\sere{r_2} &
+  \nsere{r_1\OR r_2}&\equiV\nsere{r_1}\AND\nsere{r_2}
 \end{align*}
 
 \subsection{Simplifications for Eventual and Universal Formul\ae}
diff --git a/src/ltltest/reduccmp.test b/src/ltltest/reduccmp.test
index 10104a82a..a6c4b47de 100755
--- a/src/ltltest/reduccmp.test
+++ b/src/ltltest/reduccmp.test
@@ -322,6 +322,8 @@ for x in ../reduccmp ../reductaustr; do
      run 0 $x '!{a;a;b[*2..];b}' '!a | X(!a | X(!b | X(!b | X!b)))'
      run 0 $x '!{a;b[*];c[*];e;f*}' '!a | X(!b M (!c M !e))'
      run 0 $x '!{a;b*;(a* && (b;c));c*}' '!a | X(!b M !{a[*] && {b;c}})'
+     run 0 $x '{(a;c*;d)|(b;c)}' '(a & X(c W d)) | (b & Xc)'
+     run 0 $x '!{(a;c*;d)|(b;c)}' '(X(!c M !d) | !a) & (X!c | !b)'
 
      # not reduced
      run 0 $x '{a;(b[*2..4];c*;([*0]+{d;e}))*}!' \
diff --git a/src/ltlvisit/simplify.cc b/src/ltlvisit/simplify.cc
index 6d68fb682..2ea90679c 100644
--- a/src/ltlvisit/simplify.cc
+++ b/src/ltlvisit/simplify.cc
@@ -1294,6 +1294,22 @@ namespace spot
 			     : constant::false_instance());
 		  return;
 		}
+	      if (!opt_.reduce_size_strictly)
+		if (multop* mo = is_OrRat(result_))
+		  {
+		    //  {a₁|a₂} =  {a₁}| {a₂}
+		    // !{a₁|a₂} = !{a₁}&!{a₂}
+		    unsigned s = mo->size();
+		    multop::vec* v = new multop::vec;
+		    for (unsigned n = 0; n < s; ++n)
+		      v->push_back(unop::instance(op, mo->nth(n)->clone()));
+		    mo->destroy();
+		    result_ =
+		      recurse_destroy(multop::instance(op == unop::Closure
+						       ? multop::Or
+						       : multop::And, v));
+		    return;
+		  }
 	      if (multop* mo = is_Concat(result_))
 		{
 		  unsigned end = mo->size() - 1;