From 77084747b96748399c8199c116eeaa037d6b6459 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 1 Dec 2011 16:39:15 +0100 Subject: [PATCH] Simplify {b && r[*]} as {b && r}; likewise for [->] and [=]. * src/ltlvisit/simplify.cc (simplify_visitor): Do it. * src/ltltest/reduccmp.test: Add more tests. * doc/tl/tl.tex: Document it. --- doc/tl/tl.tex | 26 ++ src/ltltest/reduccmp.test | 8 + src/ltlvisit/simplify.cc | 499 +++++++++++++++++++++----------------- 3 files changed, 317 insertions(+), 216 deletions(-) diff --git a/doc/tl/tl.tex b/doc/tl/tl.tex index b204e39bc..39027cd2c 100644 --- a/doc/tl/tl.tex +++ b/doc/tl/tl.tex @@ -1192,6 +1192,7 @@ The goals in most of these simplification are to: These simplifications are enabled with \verb|ltl_simplifier_options::reduce_basics|'. +\subsubsection{Basic Simplifications for Temporal Operators} The following are simplification rules for unary operators (applied from left to right, as usual): @@ -1264,6 +1265,31 @@ in the OR arguments: &\equiv \F(f_1\OR \ldots \OR f_n \OR \G\F(g_1\OR \ldots \OR g_m)) \\ \end{align*} +\subsubsection{Basic Simplifications for SERE Operators} + +% Cite Symbolic computation of PSL. + +The following simplification rules are used for the $n$-ary operators +$\ANDALT$, $\AND$, and $\OR$, and are of course commutative. + +\begin{align*} + b \ANDALT r\STAR{\mvar{i}..\mvar{j}} &\equiv + \begin{cases} + b \ANDALT r &\text{if~} i\le 1\le j\\ + \0 &\text{else}\\ + \end{cases}\\ + b \ANDALT r\EQUAL{\mvar{i}..\mvar{j}} &\equiv + \begin{cases} + b \ANDALT r &\text{if~} i\le 1\le j\\ + \0 &\text{else}\\ + \end{cases}\\ + b \ANDALT r\GOTO{\mvar{i}..\mvar{j}} &\equiv + \begin{cases} + b \ANDALT r &\text{if~} i\le 1\le j\\ + \0 &\text{else}\\ + \end{cases}\\ +\end{align*} + \subsection{Simplifications for Eventual and Universal Formul\ae} \label{sec:eventunivrew} diff --git a/src/ltltest/reduccmp.test b/src/ltltest/reduccmp.test index a9583ca0e..f89180a36 100755 --- a/src/ltltest/reduccmp.test +++ b/src/ltltest/reduccmp.test @@ -202,6 +202,14 @@ for x in ../reduccmp ../reductaustr; do # without pruning the rational automaton. run 0 $x '{(c&!c)[=2]}' '0' + run 0 $x '{a && b && c*} <>-> d' 'a&b&c&d' + run 0 $x '{a && b && c[*1..3]} <>-> d' 'a&b&c&d' + run 0 $x '{a && b && c[->0..2]} <>-> d' 'a&b&c&d' + run 0 $x '{a && b && c[+]} <>-> d' 'a&b&c&d' + run 0 $x '{a && b && c[=1]} <>-> d' 'a&b&c&d' + run 0 $x '{a && b && d[=2]} <>-> d' '0' + run 0 $x '{a && b && d[->2..4]} <>-> d' '0' + run 0 $x '{a && b && d[*2..]} <>-> d' '0' ;; esac diff --git a/src/ltlvisit/simplify.cc b/src/ltlvisit/simplify.cc index f9cee65ca..2154bd0a8 100644 --- a/src/ltlvisit/simplify.cc +++ b/src/ltlvisit/simplify.cc @@ -1628,8 +1628,7 @@ namespace spot while (f1 != res->end()) { multop::vec::iterator f2 = f1; - ++f2 -; + ++f2; while (f2 != res->end()) { assert(f1 != f2); @@ -1687,229 +1686,297 @@ namespace spot assert(!res->empty()); - if (opt_.reduce_basics) + // basics reduction do not concern Boolean formulas, + // so don't waste time trying to apply them. + if (opt_.reduce_basics && !mo->is_boolean()) { switch (op) { case multop::And: - { - // Gather all operands by type. - mospliter s(mospliter::Strip_X | - mospliter::Strip_FG | - mospliter::Strip_G | - mospliter::Split_F | - mospliter::Split_U_or_W | - mospliter::Split_R_or_M | - mospliter::Split_EventUniv, - res, c_); - // FG(a) & FG(b) = FG(a & b) - formula* allFG = unop_unop_multop(unop::F, unop::G, - multop::And, s.res_FG); - // Xa & Xb = X(a & b) - // Xa & Xb & FG(c) = X(a & b & FG(c)) - // For Universal&Eventual formulae f1...fn we also have: - // Xa & Xb & f1...fn = X(a & b & f1...fn) - if (!s.res_X->empty()) - { - s.res_X->push_back(allFG); - allFG = 0; - s.res_X->insert(s.res_X->begin(), - s.res_EventUniv->begin(), - s.res_EventUniv->end()); - } - else - // We don't rewrite Ga & f1...fn = G(a & f1..fn) - // similarly to what we do in the unop::Or case - // as it is not clear what we'd gain by doing so. - { - s.res_other->insert(s.res_other->begin(), - s.res_EventUniv->begin(), - s.res_EventUniv->end()); - } - delete s.res_EventUniv; + if (!mo->is_sere_formula()) + { + // Gather all operands by type. + mospliter s(mospliter::Strip_X | + mospliter::Strip_FG | + mospliter::Strip_G | + mospliter::Split_F | + mospliter::Split_U_or_W | + mospliter::Split_R_or_M | + mospliter::Split_EventUniv, + res, c_); + // FG(a) & FG(b) = FG(a & b) + formula* allFG = unop_unop_multop(unop::F, unop::G, + multop::And, s.res_FG); + // Xa & Xb = X(a & b) + // Xa & Xb & FG(c) = X(a & b & FG(c)) + // For Universal&Eventual formulae f1...fn we also have: + // Xa & Xb & f1...fn = X(a & b & f1...fn) + if (!s.res_X->empty()) + { + s.res_X->push_back(allFG); + allFG = 0; + s.res_X->insert(s.res_X->begin(), + s.res_EventUniv->begin(), + s.res_EventUniv->end()); + } + else + // We don't rewrite Ga & f1...fn = G(a & f1..fn) + // similarly to what we do in the unop::Or case + // as it is not clear what we'd gain by doing so. + { + s.res_other->insert(s.res_other->begin(), + s.res_EventUniv->begin(), + s.res_EventUniv->end()); + } + delete s.res_EventUniv; - // Xa & Xb & f1...fn = X(a & b & f1...fn) - // is built at the end of this multop::And case. - // G(a) & G(b) = G(a & b) - // is built at the end of this multop::And case. + // Xa & Xb & f1...fn = X(a & b & f1...fn) + // is built at the end of this multop::And case. + // G(a) & G(b) = G(a & b) + // is built at the end of this multop::And case. - // The following three loops perform these rewritings: - // (a U b) & (c U b) = (a & c) U b - // (a U b) & (c W b) = (a & c) U b - // (a W b) & (c W b) = (a & c) W b - // (a R b) & (a R c) = a R (b & c) - // (a R b) & (a M c) = a M (b & c) - // (a M b) & (a M c) = a M (b & c) - // F(a) & (a R b) = a M b - // F(a) & (a M b) = a M b - // F(b) & (a W b) = a U b - // F(b) & (a U b) = a U b - typedef Sgi::hash_map > fmap_t; - fmap_t uwmap; // associates "b" to "a U b" or "a W b" - fmap_t rmmap; // associates "a" to "a R b" or "a M b" - // (a U b) & (c U b) = (a & c) U b - // (a U b) & (c W b) = (a & c) U b - // (a W b) & (c W b) = (a & c) W b - for (multop::vec::iterator i = s.res_U_or_W->begin(); - i != s.res_U_or_W->end(); ++i) - { - binop* bo = static_cast(*i); - formula* b = bo->second(); - fmap_t::iterator j = uwmap.find(b); - if (j == uwmap.end()) - { - // First occurrence. - uwmap[b] = i; - continue; - } - // We already have one occurrence. Merge them. - binop* old = static_cast(*j->second); - binop::type op = binop::W; - if (bo->op() == binop::U - || old->op() == binop::U) - op = binop::U; - formula* fst_arg = - multop::instance(multop::And, - old->first()->clone(), - bo->first()->clone()); - *j->second = binop::instance(op, fst_arg, b->clone()); - assert((*j->second)->kind() == formula::BinOp); - *i = 0; - old->destroy(); - bo->destroy(); - } - // (a R b) & (a R c) = a R (b & c) - // (a R b) & (a M c) = a M (b & c) - // (a M b) & (a M c) = a M (b & c) - for (multop::vec::iterator i = s.res_R_or_M->begin(); - i != s.res_R_or_M->end(); ++i) - { - binop* bo = static_cast(*i); - formula* a = bo->first(); - fmap_t::iterator j = rmmap.find(a); - if (j == rmmap.end()) - { - // First occurrence. - rmmap[a] = i; - continue; - } - // We already have one occurrence. Merge them. - binop* old = static_cast(*j->second); - binop::type op = binop::R; - if (bo->op() == binop::M - || old->op() == binop::M) - op = binop::M; - formula* snd_arg = - multop::instance(multop::And, - old->second()->clone(), - bo->second()->clone()); - *j->second = binop::instance(op, a->clone(), snd_arg); - assert((*j->second)->kind() == formula::BinOp); - *i = 0; - old->destroy(); - bo->destroy(); - } - // F(a) & (a R b) = a M b - // F(a) & (a M b) = a M b - // F(b) & (a W b) = a U b - // F(b) & (a U b) = a U b - for (multop::vec::iterator i = s.res_F->begin(); - i != s.res_F->end(); ++i) - { - bool superfluous = false; - unop* uo = static_cast(*i); - formula* c = uo->child(); - - fmap_t::iterator j = uwmap.find(c); - if (j != uwmap.end()) - { - superfluous = true; - binop* bo = static_cast(*j->second); - if (bo->op() == binop::W) - { - *j->second = - binop::instance(binop::U, - bo->first()->clone(), - bo->second()->clone()); - assert((*j->second)->kind() == formula::BinOp); - bo->destroy(); - } - } - j = rmmap.find(c); - if (j != rmmap.end()) - { - superfluous = true; - binop* bo = static_cast(*j->second); - if (bo->op() == binop::R) - { - *j->second = - binop::instance(binop::M, - bo->first()->clone(), - bo->second()->clone()); - assert((*j->second)->kind() == formula::BinOp); - bo->destroy(); - } - } - if (superfluous) - { - (*i)->destroy(); - *i = 0; - } - } - - s.res_other->reserve(s.res_other->size() - + s.res_F->size() - + s.res_U_or_W->size() - + s.res_R_or_M->size() - + 3); - s.res_other->insert(s.res_other->end(), - s.res_F->begin(), - s.res_F->end()); - delete s.res_F; - s.res_other->insert(s.res_other->end(), - s.res_U_or_W->begin(), - s.res_U_or_W->end()); - delete s.res_U_or_W; - s.res_other->insert(s.res_other->end(), - s.res_R_or_M->begin(), - s.res_R_or_M->end()); - delete s.res_R_or_M; - - // Those "G" formulae that are eventual can be - // postponed inside the X term if there is one. - // - // In effect we rewrite - // Xa&Xb&GFc&GFd&Ge as X(a&b&G(Fc&Fd))&Ge - if (!s.res_X->empty()) - { - multop::vec* event = new multop::vec; - for (multop::vec::iterator i = s.res_G->begin(); - i != s.res_G->end(); ++i) - if ((*i)->is_eventual()) + // The following three loops perform these rewritings: + // (a U b) & (c U b) = (a & c) U b + // (a U b) & (c W b) = (a & c) U b + // (a W b) & (c W b) = (a & c) W b + // (a R b) & (a R c) = a R (b & c) + // (a R b) & (a M c) = a M (b & c) + // (a M b) & (a M c) = a M (b & c) + // F(a) & (a R b) = a M b + // F(a) & (a M b) = a M b + // F(b) & (a W b) = a U b + // F(b) & (a U b) = a U b + typedef Sgi::hash_map > fmap_t; + fmap_t uwmap; // associates "b" to "a U b" or "a W b" + fmap_t rmmap; // associates "a" to "a R b" or "a M b" + // (a U b) & (c U b) = (a & c) U b + // (a U b) & (c W b) = (a & c) U b + // (a W b) & (c W b) = (a & c) W b + for (multop::vec::iterator i = s.res_U_or_W->begin(); + i != s.res_U_or_W->end(); ++i) + { + binop* bo = static_cast(*i); + formula* b = bo->second(); + fmap_t::iterator j = uwmap.find(b); + if (j == uwmap.end()) { - event->push_back(*i); - *i = 0; // Remove it from res_G. + // First occurrence. + uwmap[b] = i; + continue; } - s.res_X->push_back(unop_multop(unop::G, - multop::And, event)); - } + // We already have one occurrence. Merge them. + binop* old = static_cast(*j->second); + binop::type op = binop::W; + if (bo->op() == binop::U + || old->op() == binop::U) + op = binop::U; + formula* fst_arg = + multop::instance(multop::And, + old->first()->clone(), + bo->first()->clone()); + *j->second = binop::instance(op, fst_arg, b->clone()); + assert((*j->second)->kind() == formula::BinOp); + *i = 0; + old->destroy(); + bo->destroy(); + } + // (a R b) & (a R c) = a R (b & c) + // (a R b) & (a M c) = a M (b & c) + // (a M b) & (a M c) = a M (b & c) + for (multop::vec::iterator i = s.res_R_or_M->begin(); + i != s.res_R_or_M->end(); ++i) + { + binop* bo = static_cast(*i); + formula* a = bo->first(); + fmap_t::iterator j = rmmap.find(a); + if (j == rmmap.end()) + { + // First occurrence. + rmmap[a] = i; + continue; + } + // We already have one occurrence. Merge them. + binop* old = static_cast(*j->second); + binop::type op = binop::R; + if (bo->op() == binop::M + || old->op() == binop::M) + op = binop::M; + formula* snd_arg = + multop::instance(multop::And, + old->second()->clone(), + bo->second()->clone()); + *j->second = binop::instance(op, a->clone(), snd_arg); + assert((*j->second)->kind() == formula::BinOp); + *i = 0; + old->destroy(); + bo->destroy(); + } + // F(a) & (a R b) = a M b + // F(a) & (a M b) = a M b + // F(b) & (a W b) = a U b + // F(b) & (a U b) = a U b + for (multop::vec::iterator i = s.res_F->begin(); + i != s.res_F->end(); ++i) + { + bool superfluous = false; + unop* uo = static_cast(*i); + formula* c = uo->child(); - // G(a) & G(b) & ... = G(a & b & ...) - formula* allG = unop_multop(unop::G, multop::And, s.res_G); - // Xa & Xb & ... = X(a & b & ...) - formula* allX = unop_multop(unop::X, multop::And, s.res_X); + fmap_t::iterator j = uwmap.find(c); + if (j != uwmap.end()) + { + superfluous = true; + binop* bo = static_cast(*j->second); + if (bo->op() == binop::W) + { + *j->second = + binop::instance(binop::U, + bo->first()->clone(), + bo->second()->clone()); + assert((*j->second)->kind() + == formula::BinOp); + bo->destroy(); + } + } + j = rmmap.find(c); + if (j != rmmap.end()) + { + superfluous = true; + binop* bo = static_cast(*j->second); + if (bo->op() == binop::R) + { + *j->second = + binop::instance(binop::M, + bo->first()->clone(), + bo->second()->clone()); + assert((*j->second)->kind() + == formula::BinOp); + bo->destroy(); + } + } + if (superfluous) + { + (*i)->destroy(); + *i = 0; + } + } - s.res_other->push_back(allX); - s.res_other->push_back(allG); - s.res_other->push_back(allFG); - 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; - } + s.res_other->reserve(s.res_other->size() + + s.res_F->size() + + s.res_U_or_W->size() + + s.res_R_or_M->size() + + 3); + s.res_other->insert(s.res_other->end(), + s.res_F->begin(), + s.res_F->end()); + delete s.res_F; + s.res_other->insert(s.res_other->end(), + s.res_U_or_W->begin(), + s.res_U_or_W->end()); + delete s.res_U_or_W; + s.res_other->insert(s.res_other->end(), + s.res_R_or_M->begin(), + s.res_R_or_M->end()); + delete s.res_R_or_M; + + // Those "G" formulae that are eventual can be + // postponed inside the X term if there is one. + // + // In effect we rewrite + // Xa&Xb&GFc&GFd&Ge as X(a&b&G(Fc&Fd))&Ge + if (!s.res_X->empty()) + { + multop::vec* event = new multop::vec; + for (multop::vec::iterator i = s.res_G->begin(); + i != s.res_G->end(); ++i) + if ((*i)->is_eventual()) + { + event->push_back(*i); + *i = 0; // Remove it from res_G. + } + s.res_X->push_back(unop_multop(unop::G, + multop::And, event)); + } + + // G(a) & G(b) & ... = G(a & b & ...) + formula* allG = + unop_multop(unop::G, multop::And, s.res_G); + // Xa & Xb & ... = X(a & b & ...) + formula* allX = + unop_multop(unop::X, multop::And, s.res_X); + + s.res_other->push_back(allX); + s.res_other->push_back(allG); + s.res_other->push_back(allFG); + 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; + } + else // SERE + { + 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); + + multop::vec* ares = new multop::vec; + for (multop::vec::iterator i = s.res_other->begin(); + i != s.res_other->end(); ++i) + switch ((*i)->kind()) + { + case formula::BUnOp: + { + bunop* r = down_cast(*i); + // b && r[*i..j] = b & r if i<=1<=j + // = 0 otherwise + // likewise for b && r[=i..j] + // and b && r[->i..j] + if (r->min() > 1 || r->max() < 1) + goto returnfalse; + ares->push_back(r->child()->clone()); + r->destroy(); + *i = 0; + break; + } + default: + ares->push_back(*i); + *i = 0; + break; + } + delete s.res_other; + ares->push_back(b); + result_ = multop::instance(multop::And, ares); + // If we altered the formula in some way, process + // it another time. + if (result_ != mo) + result_ = recurse_destroy(result_); + return; + returnfalse: + b->destroy(); + for (multop::vec::iterator i = s.res_other->begin(); + i != s.res_other->end(); ++i) + if (*i) + (*i)->destroy(); + for (multop::vec::iterator i = res->begin(); + i != res->end(); ++i) + if (*i) + (*i)->destroy(); + result_ = constant::false_instance(); + return; + } + else + { + delete s.res_Bool; + result_ = multop::instance(multop::And, s.res_other); + return; + } + } case multop::Or: { // Gather all operand by type. @@ -2160,8 +2227,8 @@ namespace spot result_ = recurse_destroy(result_); return; } - case multop::Concat: case multop::AndNLM: + case multop::Concat: case multop::Fusion: break; }