From d6587cf531d0275cba830376ecea062c5e464480 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 26 Apr 2012 18:12:01 +0200 Subject: [PATCH] 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. --- doc/tl/tl.tex | 17 +- src/ltltest/reduccmp.test | 49 ++-- src/ltlvisit/simplify.cc | 489 ++++++++++++++++++++------------------ 3 files changed, 307 insertions(+), 248 deletions(-) diff --git a/doc/tl/tl.tex b/doc/tl/tl.tex index fb8ab6192..ec63a3948 100644 --- a/doc/tl/tl.tex +++ b/doc/tl/tl.tex @@ -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{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\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*} \subsection{Simplifications for Eventual and Universal Formul\ae} diff --git a/src/ltltest/reduccmp.test b/src/ltltest/reduccmp.test index e97409aa7..cc6afc54f 100755 --- a/src/ltltest/reduccmp.test +++ b/src/ltltest/reduccmp.test @@ -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*}} <>-> 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' - 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' - run 0 $x '{a&b&c*}|->!Xb' '(X!b | !(a & b)) & (!(a & b) | !c | X(!c R !b))' + run 0 $x '{{b1;r1*}&&{b2;r2*}}' '{{b1&&b2};{r1*&&r2*}}' + run 0 $x '{{b1:r1*}&&{b2:r2*}}' '{{b1&&b2}:{r1*&&r2*}}' + run 0 $x '{{r1*;b1}&&{r2*;b2}}' '{{r1*&&r2*};{b1&&b2}}' + run 0 $x '{{r1*:b1}&&{r2*:b2}}' '{{r1*&&r2*}:{b1&&b2}}' + run 0 $x '{{a;b*;c}&&{d;e*}&&{f*;g}&&{h*}}' \ + '{{f*;g}&&{h*}&&{{a&&d};{e* && {b*;c}}}}' + run 0 $x '{{b1;r1*}&{b2;r2*}}' '{{b1&&b2};{r1*&r2*}}' + run 0 $x '{{b1:r1*}&{b2:r2*}}' '{{b1&&b2}:{r1*&r2*}}' + run 0 $x '{{r1*;b1}&{r2*;b2}}' '{{r1*&r2*};{b1&&b2}}' + run 0 $x '{{r1*:b1}&{r2*:b2}}' '{{r1*&r2*}:{b1&&b2}}' + run 0 $x '{{a;b*;c}&{d;e*}&{f*;g}&{h*}}' \ + '{{f*;g}&{h*}&{{a&&d};{e* & {b*;c}}}}' 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 '{a;[*]}[]->b' 'Gb | !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' \ '{{[*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 run 0 $x '{a;(b[*2..4];c*;([*0]+{d;e}))*}!' \ '{a;(b[*2..4];c*;([*0]+{d;e}))*}!' diff --git a/src/ltlvisit/simplify.cc b/src/ltlvisit/simplify.cc index 3d1e961f2..3af94e874 100644 --- a/src/ltlvisit/simplify.cc +++ b/src/ltlvisit/simplify.cc @@ -1265,6 +1265,264 @@ namespace spot 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 visit(binop* bo) { @@ -1773,236 +2031,15 @@ namespace spot } } case binop::UConcat: - if (!opt_.reduce_basics) + case binop::EConcat: + case binop::EConcatMarked: + if (reduce_sere_ltl(op, a, b)) + return; + else 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::Equiv: case binop::Implies: - case binop::EConcat: - case binop::EConcatMarked: // No simplification... Yet? break; }