From 614810c0db66c5c4ce776c10b46374918c1204b4 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Thu, 1 Dec 2011 18:41:00 +0100
Subject: [PATCH] Simplify {b && {r1;...;rn}}.

* doc/tl/tl.tex: Document the rules.
* src/ltlvisit/simplify.cc (simplify_visitor): Implement them.
* src/ltltest/reduccmp.test: Test them.
---
 doc/tl/tl.tex             | 11 ++++++--
 src/ltltest/reduccmp.test | 10 +++++++-
 src/ltlvisit/simplify.cc  | 54 ++++++++++++++++++++++++++++++++++-----
 3 files changed, 65 insertions(+), 10 deletions(-)

diff --git a/doc/tl/tl.tex b/doc/tl/tl.tex
index 680e25edc..53cc1eab0 100644
--- a/doc/tl/tl.tex
+++ b/doc/tl/tl.tex
@@ -1272,7 +1272,8 @@ in the OR arguments:
   yet.}
 
 The following simplification rules are used for the $n$-ary operators
-$\ANDALT$, $\AND$, and $\OR$, and are of course commutative.
+$\ANDALT$, $\AND$, and $\OR$, and are of course commutative.  $b$
+denots a Boolean formula while $r$ or $r_i$ denote any SERE.
 
 \begin{align*}
   b \ANDALT r\STAR{\mvar{i}..\mvar{j}} &\equiv
@@ -1290,7 +1291,13 @@ $\ANDALT$, $\AND$, and $\OR$, and are of course commutative.
     b \ANDALT r &\text{if~} i\le 1\le j\\
     \0 &\text{else}\\
   \end{cases}\\
-  b \ANDALT \ratgroup{r_1 \FUSION \ldots \FUSION r_n}& \equiv b \ANDALT r_1 \ANDALT \ldots \ANDALT r_n \\
+  b \ANDALT \ratgroup{r_1 \FUSION \ldots \FUSION r_n} &\equiv b \ANDALT r_1 \ANDALT \ldots \ANDALT r_n \\
+  b \ANDALT \ratgroup{r_1 \CONCAT \ldots \CONCAT r_n} &\equiv
+  \begin{cases}
+    b \ANDALT r_i & \text{if~}\exists!i,\,\varepsilon\not\VDash r_i\\
+    b \ANDALT (r_1 \OR \ldots \OR r_n) & \text{if~}\forall i,\, \varepsilon\VDash r_i\\
+    \0 &\text{else}\\
+  \end{cases}\\
 \end{align*}
 
 \subsection{Simplifications for Eventual and Universal Formul\ae}
diff --git a/src/ltltest/reduccmp.test b/src/ltltest/reduccmp.test
index e4d8657fa..b9ab6978f 100755
--- a/src/ltltest/reduccmp.test
+++ b/src/ltltest/reduccmp.test
@@ -208,9 +208,17 @@ for x in ../reduccmp ../reductaustr; do
      run 0 $x '{a && b && c[+]} <>-> d' 'a&b&c&d'
      run 0 $x '{a && b && c[=1]} <>-> d' 'a&b&c&d'
      run 0 $x '{a && b && d[=2]} <>-> d' '0'
-     run 0 $x '{a && b && d[->2..4]} <>-> d' '0'
      run 0 $x '{a && b && d[*2..]} <>-> d' '0'
+     run 0 $x '{a && b && d[->2..4]} <>-> d' '0'
      run 0 $x '{a && { c* : b* : (g|h)*}} <>-> d' 'a & c & b & (g | h) & d'
+     run 0 $x '{a && {b;c}} <>-> d' '0'
+     run 0 $x '{a && {b;c:e}} <>-> d' '0'
+     run 0 $x '{a && {b*;c*}} <>-> d' '{a && {b*|c*}} <>-> d' # until better
+     run 0 $x '{a && {b*;c*:e}} <>-> d' '{a && {b*|c*} && e} <>-> d' #	idem
+     run 0 $x '{a && {b*;c}} <>-> d' 'a & c & d'
+     run 0 $x '{a && {b*;c:e}} <>-> d' 'a & c & d & e'
+     run 0 $x '{a && {b;c*}} <>-> d' 'a & b & d'
+     run 0 $x '{a && {b;c*:e}} <>-> d' 'a & b & d & e'
      ;;
   esac
 
diff --git a/src/ltlvisit/simplify.cc b/src/ltlvisit/simplify.cc
index 9d780471d..434c6e0f6 100644
--- a/src/ltlvisit/simplify.cc
+++ b/src/ltlvisit/simplify.cc
@@ -1947,14 +1947,53 @@ namespace spot
 			      case formula::MultOp:
 				{
 				  multop* r = down_cast<multop*>(*i);
+				  unsigned rs = r->size();
 				  switch (r->op())
 				    {
 				    case multop::Fusion:
+				      //b && {r1:..:rn} = b && r1 && .. && rn
+				      for (unsigned j = 0; j < rs; ++j)
+					ares->push_back(r->nth(j)->clone());
+				      r->destroy();
+				      *i = 0;
+				      break;
+				    case multop::Concat:
+				      // b && {r1;...;rn} =
+				      // - b && ri if there is only one ri
+				      //           that does not accept [*0]
+				      // - b && (r1|...|rn) if all ri
+				      //           do not accept [*0]
+				      // - 0 if more than one ri accept [*0]
 				      {
-					//b && {r1:..:rn} = b && r1 && .. && rn
-					unsigned rs = r->size();
+					formula* ri;
+					unsigned nonempty = 0;
 					for (unsigned j = 0; j < rs; ++j)
-					  ares->push_back(r->nth(j)->clone());
+					  {
+					    formula* jf = r->nth(j);
+					    if (!jf->accepts_eword())
+					      {
+						ri = jf;
+						++nonempty;
+					      }
+					  }
+					if (nonempty == 1)
+					  {
+					    ares->push_back(ri->clone());
+					  }
+					else if (nonempty == 0)
+					  {
+					    multop::vec* sum = new multop::vec;
+					    for (unsigned j = 0; j < rs; ++j)
+					      sum->push_back(r->nth(j)
+							     ->clone());
+					    formula* sumf =
+					      multop::instance(multop::Or, sum);
+					    ares->push_back(sumf);
+					  }
+					else
+					  {
+					    goto returnfalse;
+					  }
 					r->destroy();
 					*i = 0;
 					break;
@@ -1984,10 +2023,11 @@ namespace spot
 			       i != s.res_other->end(); ++i)
 			    if (*i)
 			      (*i)->destroy();
-			  for (multop::vec::iterator i = res->begin();
-			       i != res->end(); ++i)
-			    if (*i)
-			      (*i)->destroy();
+			  delete s.res_other;
+			  for (multop::vec::iterator i = ares->begin();
+			       i != ares->end(); ++i)
+			    (*i)->destroy();
+			  delete ares;
 			  result_ = constant::false_instance();
 			  return;
 			}