Implement dual rewritings rules for <>->.
* src/ltlvisit/simplify.cc (reduce_sere_ltl): New function, to factor the code of the []-> and <>-> rewrittings. * src/ltltest/reduccmp.test: Add more tests. * doc/tl/tl.tex: Document these rewritings.
This commit is contained in:
Alexandre Duret-Lutz
parent
6f46345c3a
commit
d6587cf531
3 changed files with 307 additions and 248 deletions
|
|
@ -1456,7 +1456,22 @@ denoted with $\equiV$ can be disabled by setting the
|
||||||
\sere{b\STAR{}\CONCAT r}\Asuffix f &\equiV (\NOT b)\R(\sere{r}\Asuffix f) \text{~if~}\varepsilon\not\VDash r\\
|
\sere{b\STAR{}\CONCAT r}\Asuffix f &\equiV (\NOT b)\R(\sere{r}\Asuffix f) \text{~if~}\varepsilon\not\VDash r\\
|
||||||
\sere{r_1\CONCAT r_2}\Asuffix f &\equiV \sere{r_1}\Asuffix\X(\sere{r_2}\Asuffix f)\text{~if~}\varepsilon\not\VDash r_1\text{~and~}\varepsilon\not\VDash r_2\\
|
\sere{r_1\CONCAT r_2}\Asuffix f &\equiV \sere{r_1}\Asuffix\X(\sere{r_2}\Asuffix f)\text{~if~}\varepsilon\not\VDash r_1\text{~and~}\varepsilon\not\VDash r_2\\
|
||||||
\sere{r_1\FUSION r_2}\Asuffix f &\equiV \sere{r_1}\Asuffix(\sere{r_2}\Asuffix f)\\
|
\sere{r_1\FUSION r_2}\Asuffix f &\equiV \sere{r_1}\Asuffix(\sere{r_2}\Asuffix f)\\
|
||||||
\sere{r_1\OR r_2}\Asuffix f &\equiV (\sere{r_1}\Asuffix f)\AND(\sere{r_2}\Asuffix f)
|
\sere{r_1\OR r_2}\Asuffix f &\equiV (\sere{r_1}\Asuffix f)\AND(\sere{r_2}\Asuffix f)\\
|
||||||
|
\sere{\STAR{}}\Esuffix f &\equiv \F f\\
|
||||||
|
\sere{b\STAR{}}\Esuffix f &\equiv f \M b\\
|
||||||
|
\sere{b\PLUS{}}\Esuffix f &\equiv f \M b\\
|
||||||
|
\sere{r\STAR{\mvar{i}..\mvar{j}}}\Esuffix f &\equiV
|
||||||
|
\sere{r}\Esuffix \X(
|
||||||
|
\sere{r}\Esuffix \X(\ldots
|
||||||
|
\Esuffix\X(r\STAR{\mvar{1}..\mvar{j-i+1}})))
|
||||||
|
\text{~if~}i\ge 1\text{~and~}\varepsilon\not\VDash r\\
|
||||||
|
\sere{r\CONCAT \STAR{}}\Esuffix f &\equiv \sere{r}\Esuffix \F f\\
|
||||||
|
\sere{r\CONCAT b\STAR{}}\Esuffix f &\equiV \sere{r}\Esuffix (f\OR \X(f \M b)) \text{~if~}\varepsilon\not\VDash r\\
|
||||||
|
\sere{\STAR{}\CONCAT r}\Esuffix f &\equiV \F(\sere{r}\Esuffix f)\\
|
||||||
|
\sere{b\STAR{}\CONCAT r}\Esuffix f &\equiV b\U(\sere{r}\Esuffix f) \text{~if~}\varepsilon\not\VDash r\\
|
||||||
|
\sere{r_1\CONCAT r_2}\Esuffix f &\equiV \sere{r_1}\Esuffix\X(\sere{r_2}\Esuffix f)\text{~if~}\varepsilon\not\VDash r_1\text{~and~}\varepsilon\not\VDash r_2\\
|
||||||
|
\sere{r_1\FUSION r_2}\Esuffix f &\equiV \sere{r_1}\Esuffix(\sere{r_2}\Esuffix f)\\
|
||||||
|
\sere{r_1\OR r_2}\Esuffix f &\equiV (\sere{r_1}\Esuffix f)\OR(\sere{r_2}\Esuffix f)
|
||||||
\end{align*}
|
\end{align*}
|
||||||
|
|
||||||
\subsection{Simplifications for Eventual and Universal Formul\ae}
|
\subsection{Simplifications for Eventual and Universal Formul\ae}
|
||||||
|
|
|
||||||
|
|
@ -270,28 +270,20 @@ for x in ../reduccmp ../reductaustr; do
|
||||||
run 0 $x '{a && {b*;c:e}} <>-> d' 'a & c & d & e'
|
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*}} <>-> d' 'a & b & d'
|
||||||
run 0 $x '{a && {b;c*:e}} <>-> d' 'a & b & d & e'
|
run 0 $x '{a && {b;c*:e}} <>-> d' 'a & b & d & e'
|
||||||
run 0 $x '{{b1;r1*}&&{b2;r2*}} <>-> x' \
|
run 0 $x '{{b1;r1*}&&{b2;r2*}}' '{{b1&&b2};{r1*&&r2*}}'
|
||||||
'{{b1&&b2};{r1*&&r2*}} <>-> x'
|
run 0 $x '{{b1:r1*}&&{b2:r2*}}' '{{b1&&b2}:{r1*&&r2*}}'
|
||||||
run 0 $x '{{b1:r1*}&&{b2:r2*}} <>-> x' \
|
run 0 $x '{{r1*;b1}&&{r2*;b2}}' '{{r1*&&r2*};{b1&&b2}}'
|
||||||
'{{b1&&b2}:{r1*&&r2*}} <>-> x'
|
run 0 $x '{{r1*:b1}&&{r2*:b2}}' '{{r1*&&r2*}:{b1&&b2}}'
|
||||||
run 0 $x '{{r1*;b1}&&{r2*;b2}} <>-> x' \
|
run 0 $x '{{a;b*;c}&&{d;e*}&&{f*;g}&&{h*}}' \
|
||||||
'{{r1*&&r2*};{b1&&b2}} <>-> x'
|
'{{f*;g}&&{h*}&&{{a&&d};{e* && {b*;c}}}}'
|
||||||
run 0 $x '{{r1*:b1}&&{r2*:b2}} <>-> x' \
|
run 0 $x '{{b1;r1*}&{b2;r2*}}' '{{b1&&b2};{r1*&r2*}}'
|
||||||
'{{r1*&&r2*}:{b1&&b2}} <>-> x'
|
run 0 $x '{{b1:r1*}&{b2:r2*}}' '{{b1&&b2}:{r1*&r2*}}'
|
||||||
run 0 $x '{{a;b*;c}&&{d;e*}&&{f*;g}&&{h*}} <>-> x' \
|
run 0 $x '{{r1*;b1}&{r2*;b2}}' '{{r1*&r2*};{b1&&b2}}'
|
||||||
'{{f*;g}&&{h*}&&{{a&&d};{e* && {b*;c}}}} <>-> x'
|
run 0 $x '{{r1*:b1}&{r2*:b2}}' '{{r1*&r2*}:{b1&&b2}}'
|
||||||
run 0 $x '{{b1;r1*}&{b2;r2*}} <>-> x' \
|
run 0 $x '{{a;b*;c}&{d;e*}&{f*;g}&{h*}}' \
|
||||||
'{{b1&&b2};{r1*&r2*}} <>-> x'
|
'{{f*;g}&{h*}&{{a&&d};{e* & {b*;c}}}}'
|
||||||
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'
|
|
||||||
run 0 $x '{a&b&c*}|->!Xb' '(X!b | !(a & b)) & (!(a & b) | !c | X(!c R !b))'
|
|
||||||
run 0 $x '{a;(b*;c*;([*0]+{d;e}))*}!' '{a;{b|c|{d;e}}*}!'
|
run 0 $x '{a;(b*;c*;([*0]+{d;e}))*}!' '{a;{b|c|{d;e}}*}!'
|
||||||
|
run 0 $x '{a&b&c*}|->!Xb' '(X!b | !(a & b)) & (!(a & b) | !c | X(!c R !b))'
|
||||||
run 0 $x '{[*]}[]->b' 'Gb'
|
run 0 $x '{[*]}[]->b' 'Gb'
|
||||||
run 0 $x '{a;[*]}[]->b' 'Gb | !a'
|
run 0 $x '{a;[*]}[]->b' 'Gb | !a'
|
||||||
run 0 $x '{[*];a}[]->b' 'G(b | !a)'
|
run 0 $x '{[*];a}[]->b' 'G(b | !a)'
|
||||||
|
|
@ -306,6 +298,21 @@ for x in ../reduccmp ../reductaustr; do
|
||||||
run 0 $x '{{[*0] | a};b;{[*0] | a};c;e[*]} []-> f' \
|
run 0 $x '{{[*0] | a};b;{[*0] | a};c;e[*]} []-> f' \
|
||||||
'{{[*0] | a};b;{[*0] | a}} []-> X((f & X(f W !e)) | !c)'
|
'{{[*0] | a};b;{[*0] | a}} []-> X((f & X(f W !e)) | !c)'
|
||||||
|
|
||||||
|
run 0 $x '{a&b&c*}<>->!Xb' '(a & b & X!b) | (a & b & c & X(c U !b))'
|
||||||
|
run 0 $x '{[*]}<>->b' 'Fb'
|
||||||
|
run 0 $x '{a;[*]}<>->b' 'Fb & a'
|
||||||
|
run 0 $x '{[*];a}<>->b' 'F(a & b)'
|
||||||
|
run 0 $x '{a;b;[*]}<>->c' 'a & X(b & Fc)'
|
||||||
|
run 0 $x '{a;a;[*]}<>->c' 'a & X(a & Fc)'
|
||||||
|
run 0 $x '{s[*]}<>->b' 'b M s'
|
||||||
|
run 0 $x '{s[+]}<>->b' 'b M s'
|
||||||
|
run 0 $x '{s[*2..]}<>->b' 's & X(b M s)'
|
||||||
|
run 0 $x '{a;b*;c;d*}<>->e' 'a & X(b U (c & (e | X(e M d))))'
|
||||||
|
run 0 $x '{a:b*:c:d*}<>->e' 'a & ((c & (e M d)) M b)'
|
||||||
|
run 0 $x '{a|b*|c|d*}<>->e' '((a | c) & e) | (e M b) | (e M d)'
|
||||||
|
run 0 $x '{{[*0] | a};b;{[*0] | a};c;e[*]} <>-> f' \
|
||||||
|
'{{[*0] | a};b;{[*0] | a}} <>-> X(c & (f | X(f M e)))'
|
||||||
|
|
||||||
# not reduced
|
# not reduced
|
||||||
run 0 $x '{a;(b[*2..4];c*;([*0]+{d;e}))*}!' \
|
run 0 $x '{a;(b[*2..4];c*;([*0]+{d;e}))*}!' \
|
||||||
'{a;(b[*2..4];c*;([*0]+{d;e}))*}!'
|
'{a;(b[*2..4];c*;([*0]+{d;e}))*}!'
|
||||||
|
|
|
||||||
|
|
@ -1265,6 +1265,264 @@ namespace spot
|
||||||
result_ = unop::instance(op, result_);
|
result_ = unop::instance(op, result_);
|
||||||
}
|
}
|
||||||
|
|
||||||
|
// Return true iff reduction occurred.
|
||||||
|
bool
|
||||||
|
reduce_sere_ltl(binop::type bindop, formula* a, formula* b)
|
||||||
|
{
|
||||||
|
// All this function is documented assuming bindop ==
|
||||||
|
// UConcat, but by changing the following variable it can
|
||||||
|
// perform the rules for EConcat as well.
|
||||||
|
unop::type op_g;
|
||||||
|
binop::type op_w;
|
||||||
|
binop::type op_r;
|
||||||
|
multop::type op_and;
|
||||||
|
bool doneg;
|
||||||
|
if (bindop == binop::UConcat)
|
||||||
|
{
|
||||||
|
op_g = unop::G;
|
||||||
|
op_w = binop::W;
|
||||||
|
op_r = binop::R;
|
||||||
|
op_and = multop::And;
|
||||||
|
doneg = true;
|
||||||
|
}
|
||||||
|
else // EConcat & EConcatMarked
|
||||||
|
{
|
||||||
|
op_g = unop::F;
|
||||||
|
op_w = binop::M;
|
||||||
|
op_r = binop::U;
|
||||||
|
op_and = multop::Or;
|
||||||
|
doneg = false;
|
||||||
|
}
|
||||||
|
|
||||||
|
if (!opt_.reduce_basics)
|
||||||
|
return false;
|
||||||
|
if (bunop* bu = is_Star(a))
|
||||||
|
{
|
||||||
|
// {[*]}[]->b = Gb
|
||||||
|
if (a == bunop::one_star())
|
||||||
|
{
|
||||||
|
a->destroy();
|
||||||
|
result_ = recurse_destroy(unop::instance(op_g, b));
|
||||||
|
return true;
|
||||||
|
}
|
||||||
|
formula* s = bu->child();
|
||||||
|
unsigned min = bu->min();
|
||||||
|
unsigned max = bu->max();
|
||||||
|
// {s[*]}[]->b = b W !s if s is Boolean.
|
||||||
|
// {s[+]}[]->b = b W !s if s is Boolean.
|
||||||
|
if (s->is_boolean() && max == bunop::unbounded && min <= 1)
|
||||||
|
{
|
||||||
|
formula* ns = // !s
|
||||||
|
doneg ? unop::instance(unop::Not, s->clone()) : s->clone();
|
||||||
|
result_ = // b W !s
|
||||||
|
binop::instance(op_w, b, ns);
|
||||||
|
bu->destroy();
|
||||||
|
result_ = recurse_destroy(result_);
|
||||||
|
return true;
|
||||||
|
}
|
||||||
|
if (opt_.reduce_size_strictly)
|
||||||
|
return false;
|
||||||
|
// {s[*i..j]}[]->b = {s;s;...;s[*1..j-i+1]}[]->b
|
||||||
|
// = {s}[]->X({s}[]->X(...[]->X({s[*1..j-i+1]}[]->b)))
|
||||||
|
// if i>0 and s does not accept the empty word
|
||||||
|
if (min == 0 || s->accepts_eword())
|
||||||
|
return false;
|
||||||
|
--min;
|
||||||
|
if (max != bunop::unbounded)
|
||||||
|
max -= min; // j-i+1
|
||||||
|
// Don't rewrite s[1..].
|
||||||
|
if (min == 0)
|
||||||
|
return false;
|
||||||
|
formula* tail = // {s[*1..j-i]}[]->b
|
||||||
|
binop::instance(bindop,
|
||||||
|
bunop::instance(bunop::Star,
|
||||||
|
s->clone(), 1, max),
|
||||||
|
b);
|
||||||
|
for (unsigned n = 0; n < min; ++n)
|
||||||
|
tail = // {s}[]->X(tail)
|
||||||
|
binop::instance(bindop,
|
||||||
|
s->clone(),
|
||||||
|
unop::instance(unop::X, tail));
|
||||||
|
result_ = tail;
|
||||||
|
bu->destroy();
|
||||||
|
result_ = recurse_destroy(result_);
|
||||||
|
return true;
|
||||||
|
}
|
||||||
|
else if (multop* mo = is_Concat(a))
|
||||||
|
{
|
||||||
|
unsigned s = mo->size() - 1;
|
||||||
|
formula* last = mo->nth(s);
|
||||||
|
// {r;[*]}[]->b = {r}[]->Gb
|
||||||
|
if (last == bunop::one_star())
|
||||||
|
{
|
||||||
|
result_ =
|
||||||
|
binop::instance(bindop,
|
||||||
|
mo->all_but(s), unop::instance(op_g, b));
|
||||||
|
mo->destroy();
|
||||||
|
result_ = recurse_destroy(result_);
|
||||||
|
return true;
|
||||||
|
}
|
||||||
|
|
||||||
|
formula* first = mo->nth(0);
|
||||||
|
// {[*];r}[]->b = G({r}[]->b)
|
||||||
|
if (first == bunop::one_star())
|
||||||
|
{
|
||||||
|
result_ =
|
||||||
|
unop::instance(op_g,
|
||||||
|
binop::instance(bindop, mo->all_but(0), b));
|
||||||
|
mo->destroy();
|
||||||
|
result_ = recurse_destroy(result_);
|
||||||
|
return true;
|
||||||
|
}
|
||||||
|
|
||||||
|
if (opt_.reduce_size_strictly)
|
||||||
|
return false;
|
||||||
|
|
||||||
|
// {r;s[*]}[]->b = {r}[]->(b & X(b W !s))
|
||||||
|
// if s is Boolean and r does not accept [*0];
|
||||||
|
if (bunop* l = is_KleenStar(last)) // l = s[*]
|
||||||
|
if (l->child()->is_boolean())
|
||||||
|
{
|
||||||
|
formula* r = mo->all_but(s);
|
||||||
|
if (!r->accepts_eword())
|
||||||
|
{
|
||||||
|
formula* ns = // !s
|
||||||
|
doneg
|
||||||
|
? unop::instance(unop::Not, l->child()->clone())
|
||||||
|
: l->child()->clone();
|
||||||
|
formula* w = // b W !s
|
||||||
|
binop::instance(op_w, b->clone(), ns);
|
||||||
|
formula* x = // X(b W !s)
|
||||||
|
unop::instance(unop::X, w);
|
||||||
|
formula* d = // b & X(b W !s)
|
||||||
|
multop::instance(op_and, b, x);
|
||||||
|
result_ = // {r}[]->(b & X(b W !s))
|
||||||
|
binop::instance(bindop, r, d);
|
||||||
|
mo->destroy();
|
||||||
|
result_ = recurse_destroy(result_);
|
||||||
|
return true;
|
||||||
|
}
|
||||||
|
}
|
||||||
|
// {s[*];r}[]->b = !s R ({r}[]->b)
|
||||||
|
// if s is Boolean and r does not accept [*0];
|
||||||
|
if (bunop* l = is_KleenStar(first))
|
||||||
|
if (l->child()->is_boolean())
|
||||||
|
{
|
||||||
|
formula* r = mo->all_but(0);
|
||||||
|
if (!r->accepts_eword())
|
||||||
|
{
|
||||||
|
formula* ns = // !s
|
||||||
|
doneg
|
||||||
|
? unop::instance(unop::Not, l->child()->clone())
|
||||||
|
: l->child()->clone();
|
||||||
|
formula* u = // {r}[]->b
|
||||||
|
binop::instance(bindop, r, b);
|
||||||
|
result_ = // !s R ({r}[]->b)
|
||||||
|
binop::instance(op_r, ns, u);
|
||||||
|
mo->destroy();
|
||||||
|
result_ = recurse_destroy(result_);
|
||||||
|
return true;
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
// {r₁;r₂;r₃}[]->b = {r₁}[]->X({r₂}[]->X({r₃}[]->b))
|
||||||
|
// if r₁, r₂, r₃ do not accept [*0].
|
||||||
|
if (!mo->accepts_eword())
|
||||||
|
{
|
||||||
|
unsigned count = 0;
|
||||||
|
for (unsigned n = 0; n <= s; ++n)
|
||||||
|
count += !mo->nth(n)->accepts_eword();
|
||||||
|
assert(count > 0);
|
||||||
|
if (count == 1)
|
||||||
|
return false;
|
||||||
|
// Let e denote a term that accepts [*0]
|
||||||
|
// and let f denote a term that do not.
|
||||||
|
// A formula such as {e₁;f₁;e₂;e₃;f₂;e₄}[]->b
|
||||||
|
// in which count==2 will be grouped
|
||||||
|
// as follows: r₁ = e₁;f₁;e₂;e₃
|
||||||
|
// r₂ = f₂;e₄
|
||||||
|
// this way we have
|
||||||
|
// {e₁;f₁;e₂;e₃;f₂;e₄}[]->b = {r₁;r₂;r₃}[]->b
|
||||||
|
// where r₁ and r₂ do not accept [*0].
|
||||||
|
unsigned pos = s + 1;
|
||||||
|
|
||||||
|
// We compute the r formulas from the right
|
||||||
|
// (i.e., r₂ before r₁.)
|
||||||
|
multop::vec* r = new multop::vec;
|
||||||
|
do
|
||||||
|
r->insert(r->begin(), mo->nth(--pos)->clone());
|
||||||
|
while (r->front()->accepts_eword());
|
||||||
|
formula* tail = // {r₂}[]->b
|
||||||
|
binop::instance(bindop,
|
||||||
|
multop::instance(multop::Concat, r),
|
||||||
|
b);
|
||||||
|
while (--count)
|
||||||
|
{
|
||||||
|
multop::vec* r = new multop::vec;
|
||||||
|
do
|
||||||
|
r->insert(r->begin(), mo->nth(--pos)->clone());
|
||||||
|
while (r->front()->accepts_eword());
|
||||||
|
// If it's the last block, take all leading
|
||||||
|
// formulae as well.
|
||||||
|
if (count == 1)
|
||||||
|
while (pos > 0)
|
||||||
|
{
|
||||||
|
r->insert(r->begin(), mo->nth(--pos)->clone());
|
||||||
|
assert(r->front()->accepts_eword());
|
||||||
|
}
|
||||||
|
|
||||||
|
tail = // X({r₂}[]->b)
|
||||||
|
unop::instance(unop::X, tail);
|
||||||
|
tail = // {r₁}[]->X({r₂}[]->b)
|
||||||
|
binop::instance(bindop,
|
||||||
|
multop::instance(multop::Concat, r),
|
||||||
|
tail);
|
||||||
|
}
|
||||||
|
mo->destroy();
|
||||||
|
result_ = recurse_destroy(tail);
|
||||||
|
return true;
|
||||||
|
}
|
||||||
|
}
|
||||||
|
else if (opt_.reduce_size_strictly)
|
||||||
|
{
|
||||||
|
return false;
|
||||||
|
}
|
||||||
|
else if (multop* mo = is_Fusion(a))
|
||||||
|
{
|
||||||
|
// {r₁:r₂:r₃}[]->b = {r₁}[]->({r₂}[]->({r₃}[]->b))
|
||||||
|
unsigned s = mo->size();
|
||||||
|
formula* tail = b;
|
||||||
|
do
|
||||||
|
{
|
||||||
|
--s;
|
||||||
|
tail = binop::instance(bindop,
|
||||||
|
mo->nth(s)->clone(), tail);
|
||||||
|
}
|
||||||
|
while (s != 0);
|
||||||
|
mo->destroy();
|
||||||
|
result_ = recurse_destroy(tail);
|
||||||
|
return true;
|
||||||
|
}
|
||||||
|
else if (multop* mo = is_OrRat(a))
|
||||||
|
{
|
||||||
|
// {r₁|r₂|r₃}[]->b = ({r₁}[]->b)&({r₂}[]->b)&({r₃}[]->b)
|
||||||
|
unsigned s = mo->size();
|
||||||
|
multop::vec* v = new multop::vec;
|
||||||
|
for (unsigned n = 0; n < s; ++n)
|
||||||
|
{
|
||||||
|
formula* x = // {r₁}[]->b
|
||||||
|
binop::instance(bindop,
|
||||||
|
mo->nth(n)->clone(), b->clone());
|
||||||
|
v->push_back(x);
|
||||||
|
}
|
||||||
|
mo->destroy();
|
||||||
|
b->destroy();
|
||||||
|
result_ = recurse_destroy(multop::instance(op_and, v));
|
||||||
|
return true;
|
||||||
|
}
|
||||||
|
return false;
|
||||||
|
}
|
||||||
|
|
||||||
void
|
void
|
||||||
visit(binop* bo)
|
visit(binop* bo)
|
||||||
{
|
{
|
||||||
|
|
@ -1773,236 +2031,15 @@ namespace spot
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
case binop::UConcat:
|
case binop::UConcat:
|
||||||
if (!opt_.reduce_basics)
|
case binop::EConcat:
|
||||||
|
case binop::EConcatMarked:
|
||||||
|
if (reduce_sere_ltl(op, a, b))
|
||||||
|
return;
|
||||||
|
else
|
||||||
break;
|
break;
|
||||||
if (bunop* bu = is_Star(a))
|
|
||||||
{
|
|
||||||
// {[*]}[]->b = Gb
|
|
||||||
if (a == bunop::one_star())
|
|
||||||
{
|
|
||||||
a->destroy();
|
|
||||||
result_ = recurse_destroy(unop::instance(unop::G, b));
|
|
||||||
return;
|
|
||||||
}
|
|
||||||
formula* s = bu->child();
|
|
||||||
unsigned min = bu->min();
|
|
||||||
unsigned max = bu->max();
|
|
||||||
// {s[*]}[]->b = b W !s if s is Boolean.
|
|
||||||
// {s[+]}[]->b = b W !s if s is Boolean.
|
|
||||||
if (s->is_boolean() && max == bunop::unbounded && min <= 1)
|
|
||||||
{
|
|
||||||
formula* ns = // !s
|
|
||||||
unop::instance(unop::Not, s->clone());
|
|
||||||
result_ = // b W !s
|
|
||||||
binop::instance(binop::W, b, ns);
|
|
||||||
bu->destroy();
|
|
||||||
result_ = recurse_destroy(result_);
|
|
||||||
return;
|
|
||||||
}
|
|
||||||
if (opt_.reduce_size_strictly)
|
|
||||||
break;
|
|
||||||
// {s[*i..j]}[]->b = {s;s;...;s[*1..j-i+1]}[]->b
|
|
||||||
// = {s}[]->X({s}[]->X(...[]->X({s[*1..j-i+1]}[]->b)))
|
|
||||||
// if i>0 and s does not accept the empty word
|
|
||||||
if (min == 0 || s->accepts_eword())
|
|
||||||
break;
|
|
||||||
--min;
|
|
||||||
if (max != bunop::unbounded)
|
|
||||||
max -= min; // j-i+1
|
|
||||||
// Don't rewrite s[1..].
|
|
||||||
if (min == 0)
|
|
||||||
break;
|
|
||||||
formula* tail = // {s[*1..j-i]}[]->b
|
|
||||||
binop::instance(binop::UConcat,
|
|
||||||
bunop::instance(bunop::Star,
|
|
||||||
s->clone(), 1, max),
|
|
||||||
b);
|
|
||||||
for (unsigned n = 0; n < min; ++n)
|
|
||||||
tail = // {s}[]->X(tail)
|
|
||||||
binop::instance(binop::UConcat,
|
|
||||||
s->clone(),
|
|
||||||
unop::instance(unop::X, tail));
|
|
||||||
result_ = tail;
|
|
||||||
bu->destroy();
|
|
||||||
result_ = recurse_destroy(result_);
|
|
||||||
return;
|
|
||||||
}
|
|
||||||
else if (multop* mo = is_Concat(a))
|
|
||||||
{
|
|
||||||
unsigned s = mo->size() - 1;
|
|
||||||
formula* last = mo->nth(s);
|
|
||||||
// {r;[*]}[]->b = {r}[]->Gb
|
|
||||||
if (last == bunop::one_star())
|
|
||||||
{
|
|
||||||
result_ = binop::instance(binop::UConcat,
|
|
||||||
mo->all_but(s),
|
|
||||||
unop::instance(unop::G, b));
|
|
||||||
mo->destroy();
|
|
||||||
result_ = recurse_destroy(result_);
|
|
||||||
return;
|
|
||||||
}
|
|
||||||
|
|
||||||
formula* first = mo->nth(0);
|
|
||||||
// {[*];r}[]->b = G({r}[]->b)
|
|
||||||
if (first == bunop::one_star())
|
|
||||||
{
|
|
||||||
result_ =
|
|
||||||
unop::instance(unop::G,
|
|
||||||
binop::instance(binop::UConcat,
|
|
||||||
mo->all_but(0),
|
|
||||||
b));
|
|
||||||
mo->destroy();
|
|
||||||
result_ = recurse_destroy(result_);
|
|
||||||
return;
|
|
||||||
}
|
|
||||||
|
|
||||||
if (opt_.reduce_size_strictly)
|
|
||||||
break;
|
|
||||||
|
|
||||||
// {r;s[*]}[]->b = {r}[]->(b & X(b W !s))
|
|
||||||
// if s is Boolean and r does not accept [*0];
|
|
||||||
if (bunop* l = is_KleenStar(last)) // l = s[*]
|
|
||||||
if (l->child()->is_boolean())
|
|
||||||
{
|
|
||||||
formula* r = mo->all_but(s);
|
|
||||||
if (!r->accepts_eword())
|
|
||||||
{
|
|
||||||
formula* ns = // !s
|
|
||||||
unop::instance(unop::Not, l->child()->clone());
|
|
||||||
formula* w = // b W !s
|
|
||||||
binop::instance(binop::W, b->clone(), ns);
|
|
||||||
formula* x = // X(b W !s)
|
|
||||||
unop::instance(unop::X, w);
|
|
||||||
formula* d = // b & X(b W !s)
|
|
||||||
multop::instance(multop::And, b, x);
|
|
||||||
result_ = // {r}[]->(b & X(b W !s))
|
|
||||||
binop::instance(binop::UConcat, r, d);
|
|
||||||
mo->destroy();
|
|
||||||
result_ = recurse_destroy(result_);
|
|
||||||
return;
|
|
||||||
}
|
|
||||||
}
|
|
||||||
// {s[*];r}[]->b = !s R ({r}[]->b)
|
|
||||||
// if s is Boolean and r does not accept [*0];
|
|
||||||
if (bunop* l = is_KleenStar(first))
|
|
||||||
if (l->child()->is_boolean())
|
|
||||||
{
|
|
||||||
formula* r = mo->all_but(0);
|
|
||||||
if (!r->accepts_eword())
|
|
||||||
{
|
|
||||||
formula* ns = // !s
|
|
||||||
unop::instance(unop::Not, l->child()->clone());
|
|
||||||
formula* u = // {r}[]->b
|
|
||||||
binop::instance(binop::UConcat, r, b);
|
|
||||||
result_ = // !s R ({r}[]->b)
|
|
||||||
binop::instance(binop::R, ns, u);
|
|
||||||
mo->destroy();
|
|
||||||
result_ = recurse_destroy(result_);
|
|
||||||
return;
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
// {r₁;r₂;r₃}[]->b = {r₁}[]->X({r₂}[]->X({r₃}[]->b))
|
|
||||||
// if r₁, r₂, r₃ do not accept [*0].
|
|
||||||
if (!mo->accepts_eword())
|
|
||||||
{
|
|
||||||
unsigned count = 0;
|
|
||||||
for (unsigned n = 0; n <= s; ++n)
|
|
||||||
count += !mo->nth(n)->accepts_eword();
|
|
||||||
assert(count > 0);
|
|
||||||
if (count == 1)
|
|
||||||
break;
|
|
||||||
// Let e denote a term that accepts [*0]
|
|
||||||
// and let f denote a term that do not.
|
|
||||||
// A formula such as {e₁;f₁;e₂;e₃;f₂;e₄}[]->b
|
|
||||||
// in which count==2 will be grouped
|
|
||||||
// as follows: r₁ = e₁;f₁;e₂;e₃
|
|
||||||
// r₂ = f₂;e₄
|
|
||||||
// this way we have
|
|
||||||
// {e₁;f₁;e₂;e₃;f₂;e₄}[]->b = {r₁;r₂;r₃}[]->b
|
|
||||||
// where r₁ and r₂ do not accept [*0].
|
|
||||||
unsigned pos = s + 1;
|
|
||||||
|
|
||||||
// We compute the r formulas from the right
|
|
||||||
// (i.e., r₂ before r₁.)
|
|
||||||
multop::vec* r = new multop::vec;
|
|
||||||
do
|
|
||||||
r->insert(r->begin(), mo->nth(--pos)->clone());
|
|
||||||
while (r->front()->accepts_eword());
|
|
||||||
formula* tail = // {r₂}[]->b
|
|
||||||
binop::instance(binop::UConcat,
|
|
||||||
multop::instance(multop::Concat, r),
|
|
||||||
b);
|
|
||||||
while (--count)
|
|
||||||
{
|
|
||||||
multop::vec* r = new multop::vec;
|
|
||||||
do
|
|
||||||
r->insert(r->begin(), mo->nth(--pos)->clone());
|
|
||||||
while (r->front()->accepts_eword());
|
|
||||||
// If it's the last block, take all leading
|
|
||||||
// formulae as well.
|
|
||||||
if (count == 1)
|
|
||||||
while (pos > 0)
|
|
||||||
{
|
|
||||||
r->insert(r->begin(), mo->nth(--pos)->clone());
|
|
||||||
assert(r->front()->accepts_eword());
|
|
||||||
}
|
|
||||||
|
|
||||||
tail = // X({r₂}[]->b)
|
|
||||||
unop::instance(unop::X, tail);
|
|
||||||
tail = // {r₁}[]->X({r₂}[]->b)
|
|
||||||
binop::instance(binop::UConcat,
|
|
||||||
multop::instance(multop::Concat, r),
|
|
||||||
tail);
|
|
||||||
}
|
|
||||||
mo->destroy();
|
|
||||||
result_ = recurse_destroy(tail);
|
|
||||||
return;
|
|
||||||
}
|
|
||||||
}
|
|
||||||
else if (opt_.reduce_size_strictly)
|
|
||||||
{
|
|
||||||
break;
|
|
||||||
}
|
|
||||||
else if (multop* mo = is_Fusion(a))
|
|
||||||
{
|
|
||||||
// {r₁:r₂:r₃}[]->b = {r₁}[]->({r₂}[]->({r₃}[]->b))
|
|
||||||
unsigned s = mo->size();
|
|
||||||
formula* tail = b;
|
|
||||||
do
|
|
||||||
{
|
|
||||||
--s;
|
|
||||||
tail = binop::instance(binop::UConcat,
|
|
||||||
mo->nth(s)->clone(), tail);
|
|
||||||
}
|
|
||||||
while (s != 0);
|
|
||||||
mo->destroy();
|
|
||||||
result_ = recurse_destroy(tail);
|
|
||||||
return;
|
|
||||||
}
|
|
||||||
else if (multop* mo = is_OrRat(a))
|
|
||||||
{
|
|
||||||
// {r₁|r₂|r₃}[]->b = ({r₁}[]->b)&({r₂}[]->b)&({r₃}[]->b)
|
|
||||||
unsigned s = mo->size();
|
|
||||||
multop::vec* v = new multop::vec;
|
|
||||||
for (unsigned n = 0; n < s; ++n)
|
|
||||||
{
|
|
||||||
formula* x = // {r₁}[]->b
|
|
||||||
binop::instance(binop::UConcat,
|
|
||||||
mo->nth(n)->clone(), b->clone());
|
|
||||||
v->push_back(x);
|
|
||||||
}
|
|
||||||
mo->destroy();
|
|
||||||
b->destroy();
|
|
||||||
result_ = recurse_destroy(multop::instance(multop::And, v));
|
|
||||||
return;
|
|
||||||
}
|
|
||||||
break;
|
|
||||||
case binop::Xor:
|
case binop::Xor:
|
||||||
case binop::Equiv:
|
case binop::Equiv:
|
||||||
case binop::Implies:
|
case binop::Implies:
|
||||||
case binop::EConcat:
|
|
||||||
case binop::EConcatMarked:
|
|
||||||
// No simplification... Yet?
|
// No simplification... Yet?
|
||||||
break;
|
break;
|
||||||
}
|
}
|
||||||
|
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue