alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

Simplify {r1;b1}&&{r2;b2} or {b1:r1}&&{b2:r2}, or similar.

Browse source 
* src/ltlvisit/simplify.cc: Add four rules.
* doc/tl/tl.tex: Document these rules.
* src/ltltest/reduccmp.test: Add tests.
This commit is contained in:
Alexandre Duret-Lutz 2011-12-05 15:41:45 +01:00
parent 2f9f274a5f
commit b03935a4cf
3 changed files with 172 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

9
doc/tl/tl.tex
View file

@ -1272,8 +1272,9 @@ 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. $b$
denots a Boolean formula while $r$ or $r_i$ denote any SERE.
$\ANDALT$, $\AND$, and $\OR$. The patterns are of course commutative.
$b$ or $b_i$ denote any Boolean formula while $r$ or $r_i$ denote any
SERE.
\begin{align*}
b \ANDALT r\STAR{\mvar{i}..\mvar{j}} &\equiv
@ -1298,6 +1299,10 @@ denots a Boolean formula while $r$ or $r_i$ denote any SERE.
b \ANDALT (r_1 \OR \ldots \OR r_n) & \text{if~}\forall i,\, \varepsilon\VDash r_i\\
\0 &\text{else}\\
\end{cases}\\
\ratgroup{b_1\CONCAT r_1}\ANDALT\ratgroup{b_2\CONCAT r_2} &\equiv \ratgroup{b_1\ANDALT b_2}\CONCAT\ratgroup{r_1\ANDALT r_2} \\
\ratgroup{b_1\FUSION r_1}\ANDALT\ratgroup{b_2\FUSION r_2} &\equiv \ratgroup{b_1\ANDALT b_2}\FUSION\ratgroup{r_1\ANDALT r_2} \\
\ratgroup{r_1\CONCAT b_1}\ANDALT\ratgroup{r_2\CONCAT b_2} &\equiv \ratgroup{r_1\ANDALT r_2}\CONCAT\ratgroup{b_1\ANDALT b_2} \\
\ratgroup{r_1\FUSION b_1}\ANDALT\ratgroup{r_2\FUSION b_2} &\equiv \ratgroup{r_1\ANDALT r_2}\FUSION\ratgroup{b_1\ANDALT b_2} \\
\end{align*}
\subsection{Simplifications for Eventual and Universal Formul\ae}

10
src/ltltest/reduccmp.test
View file

@ -219,6 +219,16 @@ for x in ../reduccmp ../reductaustr; do
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'
run 0 $x '{{b1;r1*} && {b2 ; r2*}} <>-> x' \
'{{b1&&b2};{r1*&&r2*}} <>-> x'
run 0 $x '{{b1;r1*}&&{b2;r2*}} <>-> x' \
'{{b1&&b2};{r1*&&r2*}} <>-> x'
run 0 $x '{{r1*;b1}&&{r2*;b2}} <>-> x' \
'{{r1*&&r2*};{b1&&b2}} <>-> x'
run 0 $x '{{r1*;b1}&&{r2*;b2}} <>-> x' \
'{{r1*&&r2*};{b1&&b2}} <>-> x'
run 0 $x '{{a;b*;c}&&{d;e*}&&{f*;g}&&{h*}} <>-> x' \
'{{f*;g}&&{h*}&&{{a&&d};{e* && {b*;c}}}} <>-> x'
;;
esac

155
src/ltlvisit/simplify.cc
View file

@ -2033,8 +2033,163 @@ namespace spot
}
else
{
// No Boolean as argument of &&.
delete s.res_Bool;
// Look for occurrences of {b;r} or {b:r}. We have
// {b1;r1}&&{b2;r2} = {b1&&b2};{r1&&r2}
// head1 tail1
// {b1:r1}&&{b2:r2} = {b1&&b2}:{r1&&r2}
// head2 tail2
multop::vec* head1 = new multop::vec;
multop::vec* tail1 = new multop::vec;
multop::vec* head2 = new multop::vec;
multop::vec* tail2 = new multop::vec;
for (multop::vec::iterator i = s.res_other->begin();
i != s.res_other->end(); ++i)
{
if (!*i)
continue;
if ((*i)->kind() != formula::MultOp)
continue;
multop* f = down_cast<multop*>(*i);
formula* h = f->nth(0);
if (!h->is_boolean())
continue;
multop::type op = f->op();
if (op == multop::Concat)
{
head1->push_back(h->clone());
multop::vec* tail = new multop::vec;
unsigned s = f->size();
for (unsigned j = 1; j < s; ++j)
tail->push_back(f->nth(j)->clone());
tail1->push_back(multop::instance(op, tail));
(*i)->destroy();
*i = 0;
}
else if (op == multop::Fusion)
{
head2->push_back(h->clone());
multop::vec* tail = new multop::vec;
unsigned s = f->size();
for (unsigned j = 1; j < s; ++j)
tail->push_back(f->nth(j)->clone());
tail2->push_back(multop::instance(op, tail));
(*i)->destroy();
*i = 0;
}
else
{
continue;
}
}
if (!head1->empty())
{
formula* h = multop::instance(multop::And, head1);
formula* t = multop::instance(multop::And, tail1);
formula* f = multop::instance(multop::Concat,
h, t);
s.res_other->push_back(f);
}
else
{
delete head1;
delete tail1;
}
if (!head2->empty())
{
formula* h = multop::instance(multop::And, head2);
formula* t = multop::instance(multop::And, tail2);
formula* f = multop::instance(multop::Fusion,
h, t);
s.res_other->push_back(f);
}
else
{
delete head2;
delete tail2;
}
// {r1;b1}&&{r2;b2} = {r1&&r2};{b1&&b2}
// head3 tail3
// {r1:b1}&&{r2:b2} = {r1&&r2}:{b1&&b2}
// head4 tail4
multop::vec* head3 = new multop::vec;
multop::vec* tail3 = new multop::vec;
multop::vec* head4 = new multop::vec;
multop::vec* tail4 = new multop::vec;
for (multop::vec::iterator i = s.res_other->begin();
i != s.res_other->end(); ++i)
{
if (!*i)
continue;
if ((*i)->kind() != formula::MultOp)
continue;
multop* f = down_cast<multop*>(*i);
unsigned s = f->size() - 1;
formula* t = f->nth(s);
if (!t->is_boolean())
continue;
multop::type op = f->op();
if (op == multop::Concat)
{
tail3->push_back(t->clone());
multop::vec* head = new multop::vec;
for (unsigned j = 0; j < s; ++j)
head->push_back(f->nth(j)->clone());
head3->push_back(multop::instance(op, head));
(*i)->destroy();
*i = 0;
}
else if (op == multop::Fusion)
{
tail4->push_back(t->clone());
multop::vec* head = new multop::vec;
for (unsigned j = 0; j < s; ++j)
head->push_back(f->nth(j)->clone());
head4->push_back(multop::instance(op, head));
(*i)->destroy();
*i = 0;
}
else
{
continue;
}
}
if (!head3->empty())
{
formula* h = multop::instance(multop::And, head3);
formula* t = multop::instance(multop::And, tail3);
formula* f = multop::instance(multop::Concat,
h, t);
s.res_other->push_back(f);
}
else
{
delete head3;
delete tail3;
}
if (!head4->empty())
{
formula* h = multop::instance(multop::And, head4);
formula* t = multop::instance(multop::And, tail4);
formula* f = multop::instance(multop::Fusion,
h, t);
s.res_other->push_back(f);
}
else
{
delete head4;
delete tail4;
}
result_ = multop::instance(multop::And, s.res_other);
// If we altered the formula in some way, process
// it another time.
if (result_ != mo)
result_ = recurse_destroy(result_);
return;
}
}