diff --git a/doc/tl/tl.tex b/doc/tl/tl.tex index 39027cd2c..680e25edc 100644 --- a/doc/tl/tl.tex +++ b/doc/tl/tl.tex @@ -1267,7 +1267,9 @@ in the OR arguments: \subsubsection{Basic Simplifications for SERE Operators} -% Cite Symbolic computation of PSL. +\spottodo[inline]{These rules, mostly taken from ``Symbolic + computation of PSL'' (Cimatti, Roveri, and Tonetta) are not complete + yet.} The following simplification rules are used for the $n$-ary operators $\ANDALT$, $\AND$, and $\OR$, and are of course commutative. @@ -1288,6 +1290,7 @@ $\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 \\ \end{align*} \subsection{Simplifications for Eventual and Universal Formul\ae} diff --git a/src/ltlast/multop.cc b/src/ltlast/multop.cc index 413a9a77d..d375b6e4c 100644 --- a/src/ltlast/multop.cc +++ b/src/ltlast/multop.cc @@ -43,8 +43,9 @@ namespace spot switch (op) { - case Concat: case Fusion: + is.accepting_eword = false; + case Concat: case AndNLM: // Note: AndNLM(p1,p2) is a Boolean formula, but it is // actually rewritten as And(p1,p2) by trivial identities diff --git a/src/ltltest/reduccmp.test b/src/ltltest/reduccmp.test index f89180a36..e4d8657fa 100755 --- a/src/ltltest/reduccmp.test +++ b/src/ltltest/reduccmp.test @@ -210,6 +210,7 @@ for x in ../reduccmp ../reductaustr; do 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 && { c* : b* : (g|h)*}} <>-> d' 'a & c & b & (g | h) & d' ;; esac diff --git a/src/ltlvisit/simplify.cc b/src/ltlvisit/simplify.cc index 2154bd0a8..9d780471d 100644 --- a/src/ltlvisit/simplify.cc +++ b/src/ltlvisit/simplify.cc @@ -1944,7 +1944,28 @@ namespace spot *i = 0; break; } + case formula::MultOp: + { + multop* r = down_cast(*i); + switch (r->op()) + { + case multop::Fusion: + { + //b && {r1:..:rn} = b && r1 && .. && rn + unsigned rs = r->size(); + for (unsigned j = 0; j < rs; ++j) + ares->push_back(r->nth(j)->clone()); + r->destroy(); + *i = 0; + break; + } + default: + goto common; + } + break; + } default: + common: ares->push_back(*i); *i = 0; break;