From b03935a4cf2182fc82671686e7f6832827cb5086 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Mon, 5 Dec 2011 15:41:45 +0100 Subject: [PATCH] Simplify {r1;b1}&&{r2;b2} or {b1:r1}&&{b2:r2}, or similar. * src/ltlvisit/simplify.cc: Add four rules. * doc/tl/tl.tex: Document these rules. * src/ltltest/reduccmp.test: Add tests. --- doc/tl/tl.tex | 9 ++- src/ltltest/reduccmp.test | 10 +++ src/ltlvisit/simplify.cc | 155 ++++++++++++++++++++++++++++++++++++++ 3 files changed, 172 insertions(+), 2 deletions(-) diff --git a/doc/tl/tl.tex b/doc/tl/tl.tex index 6922b3698..c046eead1 100644 --- a/doc/tl/tl.tex +++ b/doc/tl/tl.tex @@ -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} diff --git a/src/ltltest/reduccmp.test b/src/ltltest/reduccmp.test index b9ab6978f..8fc77f230 100755 --- a/src/ltltest/reduccmp.test +++ b/src/ltltest/reduccmp.test @@ -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 diff --git a/src/ltlvisit/simplify.cc b/src/ltlvisit/simplify.cc index 434c6e0f6..96d8c829f 100644 --- a/src/ltlvisit/simplify.cc +++ b/src/ltlvisit/simplify.cc @@ -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(*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(*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; } }