diff --git a/src/ltltest/reduccmp.test b/src/ltltest/reduccmp.test index 526f15cd5..b7dc60912 100755 --- a/src/ltltest/reduccmp.test +++ b/src/ltltest/reduccmp.test @@ -101,8 +101,8 @@ for x in ../reduccmp ../reductaustr; do run 0 $x '(a R b) | (c R b)' '(a | c) R b' run 0 $x 'Xa & FGb' 'X(a & FGb)' - run 0 $x 'Xa | FGb' 'Xa | FGb' # We'd prefer 'X(a | FGb)' - run 0 $x 'Xa & GFb' 'Xa & GFb' # 'X(a & GFb)' + run 0 $x 'Xa | FGb' 'X(a | FGb)' + run 0 $x 'Xa & GFb' 'X(a & GFb)' run 0 $x 'Xa | GFb' 'X(a | GFb)' # The following is not reduced to F(a) & GFb. because # (1) is does not help the translate the formula into a @@ -111,8 +111,10 @@ for x in ../reduccmp ../reductaustr; do # (2) ... it would hinder this useful reduction (that helps to # produce a smaller automaton) run 0 $x 'F(f1 & GF(f2)) | F(a & GF(b))' 'F((f1&GFf2)|(a&GFb))' - # FIXME: Don't we want the opposite rewriting - run 0 $x 'Fa & GFb' 'Fa & GFb' # We'd prefer 'F(a & GFb)' + # FIXME: Don't we want the opposite rewriting? + # rewriting Fa & GFb as F(a & GFb) seems better, but + # it not clear how that scales to Fa & Fb & GFc... + run 0 $x 'Fa & GFb' 'Fa & GFb' run 0 $x 'G(a | GFb)' 'Ga | GFb' # The following is not reduced to F(a & c) & GF(b) for the same # reason as above. @@ -168,8 +170,16 @@ for x in ../reduccmp ../reductaustr; do run 0 $x 'Fa|GFc' 'F(a|GFc)' run 0 $x 'FGa|GFc' 'F(Ga|GFc)' run 0 $x 'Ga&Xb&FGc' 'Ga & X(b&FGc)' - run 0 $x 'Ga&Xb&GFc' 'G(a&Fc) & Xb' + run 0 $x 'Ga&Xb&GFc' 'Ga & X(b&GFc)' run 0 $x 'Ga&GFc' 'G(a&Fc)' + run 0 $x 'G(a|b|GFc|GFd|FGe|FGf)' 'G(a|b)|GF(c|d)|F(Ge|Gf)' + run 0 $x 'G(a|b)|GFc|GFd|FGe|FGf' 'G(a|b)|GF(c|d)|F(Ge|Gf)' + run 0 $x 'X(a|b)|GFc|GFd|FGe|FGf' 'X(a|b|GF(c|d)|F(Ge|Gf))' + run 0 $x 'Xa&Xb&GFc&GFd&Ge' 'X(a&b&G(Fc&Fd))&Ge' + + # F comes in front when possible... + run 0 $x 'GFc|GFd|FGe|FGf' 'F(GF(c|d)|Ge|Gf)' + run 0 $x 'G(GFc|GFd|FGe|FGf)' 'F(GF(c|d)|Ge|Gf)' ;; esac diff --git a/src/ltlvisit/simplify.cc b/src/ltlvisit/simplify.cc index 086204b28..421eb3da7 100644 --- a/src/ltlvisit/simplify.cc +++ b/src/ltlvisit/simplify.cc @@ -1005,22 +1005,25 @@ namespace spot } } - // G(f1|f2|GF(f3)|GF(f4)|FG(f5)|FG(f6)) = - // G(f1|f2) | GF(f3|f4) | FG(f5) | FG(f6) - // FIXME: can this be generalized to Universal formulae? + // G(f1|f2|GF(f3)|GF(f4)|f5|f6) = + // G(f1|f2) | GF(f3|f4) | f5 | f6 + // if f5 and f6 are both eventual and universal. if (result_->kind() == formula::MultOp) { multop* mo = static_cast(result_); if (mo->op() == multop::Or) { - mospliter s(mospliter::Strip_GF | mospliter::Split_FG, + mospliter s(mospliter::Strip_GF | + mospliter::Split_EventUniv, mo, c_); - s.res_FG->push_back(unop_multop(unop::G, multop::Or, - s.res_other)); - s.res_FG->push_back(unop_unop_multop(unop::G, unop::F, - multop::Or, - s.res_GF)); - result_ = multop::instance(multop::Or, s.res_FG); + s.res_EventUniv->push_back(unop_multop(unop::G, + multop::Or, + s.res_other)); + s.res_EventUniv->push_back(unop_unop_multop(unop::G, + unop::F, + multop::Or, + s.res_GF)); + result_ = multop::instance(multop::Or, s.res_EventUniv); if (result_ != uo) result_ = recurse_destroy(result_); return; @@ -1553,10 +1556,10 @@ namespace spot } delete s.res_EventUniv; - formula* allX = unop_multop(unop::X, multop::And, s.res_X); - - // G(a) & G(b) = G(a & b) - formula* allG = unop_multop(unop::G, multop::And, s.res_G); + // Xa & Xb & f1...fn = X(a & b & f1...fn) + // is built at the end of this multop::And case. + // G(a) & F(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 @@ -1700,9 +1703,34 @@ namespace spot 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(allFG); 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. @@ -1736,10 +1764,33 @@ namespace spot s.res_EventUniv->begin(), s.res_EventUniv->end()); } - else if (!s.res_F->empty()) + else if (!s.res_F->empty() + && s.res_G->empty() + && s.res_U_or_W->empty() + && s.res_R_or_M->empty() + && s.res_other->empty()) { - // If there is no X but some F, do - // Fa | Fb | f1...fn | GF(c) = F(a | b | f1...fn | GF(c)) + // If there is no X but some F and only + // eventual&universal formula, do: + // Fa|Fb|f1...fn|GF(c) = F(a|b|f1...fn|GF(c)) + // + // The reasoning here is that if we should + // move f1...fn|GF(c) inside the "F" only + // if it allows us to move all terms under F, + // allowing a nice initial self-loop. + // + // For instance: + // F(a|GFb) 3st.6tr. with initial self-loop + // Fa|GFb 4st.8tr. without initial self-loop + // + // However, if other term are presents they will + // prevent the formation of a self-loop, and the + // rewriting is unwelcome: + // F(a|GFb)|Gc 5st.11tr. without initial self-loop + // Fa|GFb|Gc 5st.10tr. without initial self-loop + // (counting the number of "subtransitions" + // or, degeneralizing the automaton amplify + // these differences) s.res_F->push_back(allGF); allGF = 0; s.res_F->insert(s.res_F->end(), @@ -1753,9 +1804,10 @@ namespace spot s.res_EventUniv->end()); } delete s.res_EventUniv; - formula* allX = unop_multop(unop::X, multop::Or, s.res_X); + // Xa | Xb | f1...fn = X(a | b | f1...fn) + // is built at the end of this multop::Or case. // F(a) | F(b) = F(a | b) - formula* allF = unop_multop(unop::F, multop::Or, s.res_F); + // is built at the end of this multop::Or case. // The following three loops perform these rewritings: // (a U b) | (a U c) = a U (b | c) @@ -1882,6 +1934,8 @@ namespace spot } } + + s.res_other->reserve(s.res_other->size() + s.res_G->size() + s.res_U_or_W->size() @@ -1899,9 +1953,34 @@ namespace spot s.res_R_or_M->begin(), s.res_R_or_M->end()); delete s.res_R_or_M; + + // Those "F" formulae that are universal can be + // postponed inside the X term if there is one. + // + // In effect we rewrite + // Xa|Xb|FGc|FGd|Fe as X(a|b|F(Gc|Gd))|Fe + if (!s.res_X->empty()) + { + multop::vec* univ = new multop::vec; + for (multop::vec::iterator i = s.res_F->begin(); + i != s.res_F->end(); ++i) + if ((*i)->is_universal()) + { + univ->push_back(*i); + *i = 0; // Remove it from res_F. + } + s.res_X->push_back(unop_multop(unop::F, + multop::Or, univ)); + } + + // F(a) | F(b) | ... = F(a | b | ...) + formula* allF = unop_multop(unop::F, multop::Or, s.res_F); + // Xa | Xb | ... = X(a | b | ...) + formula* allX = unop_multop(unop::X, multop::Or, s.res_X); + s.res_other->push_back(allX); - s.res_other->push_back(allGF); s.res_other->push_back(allF); + s.res_other->push_back(allGF); result_ = multop::instance(multop::Or, s.res_other); // If we altered the formula in some way, process // it another time.