From 35b41331f7a49c6ab9c920526d46cd0bbef6e8aa Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 18 Apr 2012 01:00:49 +0200 Subject: [PATCH] Add more simplification rules for AndNLM. * src/ltlvisit/simplify.cc: Here. * src/ltltest/reduccmp.test: More tests. * doc/tl/tl.tex: Document them. --- doc/tl/tl.tex | 19 +++- src/ltltest/reduccmp.test | 19 +++- src/ltlvisit/simplify.cc | 211 ++++++++++++++++++++++++++++++++++++++ 3 files changed, 240 insertions(+), 9 deletions(-) diff --git a/doc/tl/tl.tex b/doc/tl/tl.tex index 41ffe2c4e..7cbb653ef 100644 --- a/doc/tl/tl.tex +++ b/doc/tl/tl.tex @@ -1367,7 +1367,12 @@ SERE. \begin{cases} b \ANDALT r &\text{if~} i\le 1\le j\\ \0 &\text{else}\\ - \end{cases}\\ + \end{cases} & + b \AND r &\equiV + \begin{cases} + b \OR \mathtt{\{}b\FUSION r\mathtt{\}}&\text{if~} \varepsilon\VDash r_i\\ + b\FUSION r&\text{if~} \varepsilon\not\VDash r_i\\ + \end{cases} \\ b \ANDALT \sere{r_1 \FUSION \ldots \FUSION r_n} &\equiv b \ANDALT r_1 \ANDALT \ldots \ANDALT r_n \\ b \ANDALT \sere{r_1 \CONCAT \ldots \CONCAT r_n} &\equiv \begin{cases} @@ -1375,10 +1380,14 @@ SERE. b \ANDALT (r_1 \OR \ldots \OR r_n) & \text{if~}\forall i,\, \varepsilon\VDash r_i\\ \0 &\text{else}\\ \end{cases}\\ - \sere{b_1\CONCAT r_1}\ANDALT\sere{b_2\CONCAT r_2} &\equiv \sere{b_1\ANDALT b_2}\CONCAT\sere{r_1\ANDALT r_2} \\ - \sere{b_1\FUSION r_1}\ANDALT\sere{b_2\FUSION r_2} &\equiv \sere{b_1\ANDALT b_2}\FUSION\sere{r_1\ANDALT r_2} \\ - \sere{r_1\CONCAT b_1}\ANDALT\sere{r_2\CONCAT b_2} &\equiv \sere{r_1\ANDALT r_2}\CONCAT\sere{b_1\ANDALT b_2} \\ - \sere{r_1\FUSION b_1}\ANDALT\sere{r_2\FUSION b_2} &\equiv \sere{r_1\ANDALT r_2}\FUSION\sere{b_1\ANDALT b_2} \\ + \sere{b_1\CONCAT r_1}\ANDALT\sere{b_2\CONCAT r_2} &\equiv \sere{b_1\ANDALT b_2}\CONCAT\sere{r_1\ANDALT r_2} & + \sere{b_1\CONCAT r_1}\AND \sere{b_2\CONCAT r_2} &\equiv \sere{b_1\ANDALT b_2}\CONCAT\sere{r_1\AND r_2} \\ + \sere{b_1\FUSION r_1}\ANDALT\sere{b_2\FUSION r_2} &\equiv \sere{b_1\ANDALT b_2}\FUSION\sere{r_1\ANDALT r_2} & + \sere{b_1\FUSION r_1}\AND \sere{b_2\FUSION r_2} &\equiv \sere{b_1\ANDALT b_2}\FUSION\sere{r_1\AND r_2} \\ + \sere{r_1\CONCAT b_1}\ANDALT\sere{r_2\CONCAT b_2} &\equiv \sere{r_1\ANDALT r_2}\CONCAT\sere{b_1\ANDALT b_2} & + \sere{r_1\CONCAT b_1}\AND \sere{r_2\CONCAT b_2} &\equiv \sere{r_1\ANDALT r_2}\CONCAT\sere{b_1\AND b_2} \\ + \sere{r_1\FUSION b_1}\ANDALT\sere{r_2\FUSION b_2} &\equiv \sere{r_1\ANDALT r_2}\FUSION\sere{b_1\ANDALT b_2} & + \sere{r_1\FUSION b_1}\AND \sere{r_2\FUSION b_2} &\equiv \sere{r_1\ANDALT r_2}\FUSION\sere{b_1\AND b_2} \\ \end{align*} \subsection{Simplifications for Eventual and Universal Formul\ae} diff --git a/src/ltltest/reduccmp.test b/src/ltltest/reduccmp.test index b8ccd14c6..15ecefb44 100755 --- a/src/ltltest/reduccmp.test +++ b/src/ltltest/reduccmp.test @@ -270,16 +270,27 @@ 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 '{{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 '{{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' '{(a&&b)|((a&&b):c*)}|-> X!b' ;; esac diff --git a/src/ltlvisit/simplify.cc b/src/ltlvisit/simplify.cc index e77060668..f7a309c85 100644 --- a/src/ltlvisit/simplify.cc +++ b/src/ltlvisit/simplify.cc @@ -2976,6 +2976,217 @@ namespace spot return; } case multop::AndNLM: + { + mospliter s(mospliter::Split_Bool, res, c_); + if (!s.res_Bool->empty()) + { + // b1 & b2 & b3 = b1 && b2 && b3 + formula* b = multop::instance(multop::And, s.res_Bool); + + // now we just consider b & rest + formula* rest = multop::instance(multop::AndNLM, + s.res_other); + + // We have b & rest = b : rest if rest does not + // accept [*0]. Otherwise b & rest = b | (b : rest) + // FIXME: It would be nice to remove [*0] from rest. + if (rest->accepts_eword()) + { + // The b & rest = b | (b : rest) rewriting + // augment the size, so do that only when + // explicitly requested. + if (!opt_.reduce_size_strictly) + { + formula* brest = + multop::instance(multop::Fusion, b->clone(), + rest); + result_ = + multop::instance(multop::Or, b, brest); + } + else + { + result_ = multop::instance(multop::AndNLM, + b, rest); + } + } + else + { + result_ = multop::instance(multop::Fusion, + b, rest); + } + // If we altered the formula in some way, process + // it another time. + if (result_ != mo) + result_ = recurse_destroy(result_); + return; + } + 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(*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::AndNLM, 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::AndNLM, 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(*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::AndNLM, 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::AndNLM, 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::AndNLM, s.res_other); + // If we altered the formula in some way, process + // it another time. + if (result_ != mo) + result_ = recurse_destroy(result_); + return; + } + break; + } case multop::Concat: case multop::Fusion: break;