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

Implement rewritings for {f|g} and !{f|g}.

Browse source 
* src/ltlvisit/simplify.cc: Here.
* src/ltltest/reduccmp.test: Test them.
* doc/tl/tl.tex: Document them.
This commit is contained in:
Alexandre Duret-Lutz 2012-04-29 23:36:12 +02:00
parent 496c449fa4
commit 0821599db8
3 changed files with 21 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

4
doc/tl/tl.tex
View file

@ -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}

2
src/ltltest/reduccmp.test
View file

@ -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}))*}!' \

16
src/ltlvisit/simplify.cc
View file

@ -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;