Commit d0cfd44b authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

Simplify {b && {r1:...:rn}} as {b && r1 && ... && rn}.

* src/ltlvisit/simplify.cc (simplify_visitor): Do it.
* src/ltltest/reduccmp.test: Add a test.
* doc/tl/tl.tex: Document it.
* src/ltlast/multop.cc: Fix the computation of is.accepting_eword
for Fusion.  The Fusion operator never accepts [*0].
parent 77084747
......@@ -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}
......
......@@ -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
......
......@@ -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
......
......@@ -1944,7 +1944,28 @@ namespace spot
*i = 0;
break;
}
case formula::MultOp:
{
multop* r = down_cast<multop*>(*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;
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment