From 691119c188db6d1c71ea0975807f771245dc730a Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 18 Apr 2012 19:20:43 +0200 Subject: [PATCH] Introduce AndRat and OrRat operator. It was a mistake to try to overload And/Or LTL operator for these when trivial simplification are performed. The reason is so simple it is embarassing: And(f,1)=f is a trivial identity that should not be applied with AndRat. E.g. AndRat(a;b, 1) is equal to 0, not a;b. * src/ltlast/multop.hh, src/ltlast/multop.cc: Add the AndRat and OrRat operators. * src/ltlparse/ltlparse.yy: Build them. * src/ltlvisit/mark.cc, src/ltlvisit/simplify.cc, src/ltlvisit/tostring.cc, src/tgba/formula2bdd.cc, src/tgbaalgos/eltl2tgba_lacim.cc, src/tgbaalgos/ltl2taa.cc, src/tgbaalgos/ltl2tgba_fm.cc, src/tgbaalgos/ltl2tgba_lacim.cc: Adjust all switches. --- src/ltlast/multop.cc | 104 ++- src/ltlast/multop.hh | 56 +- src/ltlparse/ltlparse.yy | 4 +- src/ltlvisit/mark.cc | 11 +- src/ltlvisit/simplify.cc | 1383 +++++++++++++++--------------- src/ltlvisit/tostring.cc | 13 +- src/tgba/formula2bdd.cc | 6 +- src/tgbaalgos/eltl2tgba_lacim.cc | 4 +- src/tgbaalgos/ltl2taa.cc | 6 +- src/tgbaalgos/ltl2tgba_fm.cc | 77 +- src/tgbaalgos/ltl2tgba_lacim.cc | 11 +- 11 files changed, 916 insertions(+), 759 deletions(-) diff --git a/src/ltlast/multop.cc b/src/ltlast/multop.cc index a1ac89d4c..17ec4ab52 100644 --- a/src/ltlast/multop.cc +++ b/src/ltlast/multop.cc @@ -47,11 +47,13 @@ namespace spot is.accepting_eword = false; case Concat: case AndNLM: - // Note: AndNLM(p1,p2) is a Boolean formula, but it is - // actually rewritten as And(p1,p2) by trivial identities - // before this constructor is called. So at this point, - // AndNLM is always used with at most one Boolean argument, - // and the result is therefore NOT Boolean. + case AndRat: + // Note: AndNLM(p1,p2) and AndRat(p1,p2) are Boolean + // formulae, but there are actually rewritten as And(p1,p2) + // by trivial identities before this constructor is called. + // So at this point, AndNLM/AndRat are always used with at + // most one Boolean argument, and the result is therefore + // NOT Boolean. is.boolean = false; is.ltl_formula = false; is.eltl_formula = false; @@ -62,6 +64,18 @@ namespace spot for (unsigned i = 1; i < s; ++i) props &= (*v)[i]->get_props(); break; + case OrRat: + // Note: OrRat(p1,p2) is a Boolean formula, but its is + // actually rewritten as Or(p1,p2) by trivial identities + // before this constructor is called. So at this point, + // AndNLM is always used with at most one Boolean argument, + // and the result is therefore NOT Boolean. + is.boolean = false; + is.ltl_formula = false; + is.eltl_formula = false; + is.psl_formula = false; + is.eventual = false; + is.universal = false; case Or: { bool ew = (*v)[0]->accepts_eword(); @@ -159,10 +173,14 @@ namespace spot { case And: return "And"; + case AndRat: + return "AndRat"; case AndNLM: return "AndNLM"; case Or: return "Or"; + case OrRat: + return "OrRat"; case Concat: return "Concat"; case Fusion: @@ -173,6 +191,37 @@ namespace spot return 0; } + + void + gather_bool(multop::vec* v, multop::type op) + { + // Gather all boolean terms. + multop::vec* b = new multop::vec; + multop::vec::iterator i = v->begin(); + while (i != v->end()) + { + if ((*i)->is_boolean()) + { + b->push_back(*i); + i = v->erase(i); + } + else + { + ++i; + } + } + // - AndNLM(Exps1...,Bool1,Exps2...,Bool2,Exps3...) = + // AndNLM(Exps1...,Exps2...,Exps3...,And(Bool1,Bool2)) + // - AndRat(Exps1...,Bool1,Exps2...,Bool2,Exps3...) = + // AndRat(Exps1...,Exps2...,Exps3...,And(Bool1,Bool2)) + // - OrRat(Exps1...,Bool1,Exps2...,Bool2,Exps3...) = + // AndRat(Exps1...,Exps2...,Exps3...,Or(Bool1,Bool2)) + if (!b->empty()) + v->push_back(multop::instance(op, b)); + else + delete b; + } + multop::map multop::instances; // We match equivalent formulae modulo "ACI rules" @@ -246,7 +295,15 @@ namespace spot neutral2 = 0; abs = constant::false_instance(); abs2 = 0; + weak_abs = 0; + break; + case AndRat: + neutral = 0; /* FIXME: we should use 1[*] as neutral */ + neutral2 = 0; + abs = constant::false_instance(); + abs2 = 0; weak_abs = constant::empty_word_instance(); + gather_bool(v, And); break; case AndNLM: neutral = constant::true_instance(); @@ -254,30 +311,7 @@ namespace spot abs = constant::false_instance(); abs2 = 0; weak_abs = 0; - - // Make a first pass to gather all boolean terms. - { - vec* b = new vec; - vec::iterator i = v->begin(); - while (i != v->end()) - { - if ((*i)->is_boolean()) - { - b->push_back(*i); - i = v->erase(i); - } - else - { - ++i; - } - } - // - AndNLM(Exps1...,Bool1,Exps2...,Bool2,Exps3...) = - // AndNLM(Exps1...,Exps2...,Exps3...,And(Bool1,Bool2)) - if (!b->empty()) - v->push_back(instance(And, b)); - else - delete b; - } + gather_bool(v, And); break; case Or: neutral = constant::false_instance(); @@ -286,6 +320,14 @@ namespace spot abs2 = 0; weak_abs = 0; break; + case OrRat: + neutral = constant::false_instance(); + neutral2 = 0; + abs = 0; // FIXME: should be 1[*]. + abs2 = 0; + weak_abs = 0; + gather_bool(v, Or); + break; case Concat: neutral = constant::empty_word_instance(); neutral2 = 0; @@ -377,8 +419,8 @@ namespace spot } } - // We have a* & [*0] & c = 0 - // and a* & [*0] & c* = [*0] + // We have a* && [*0] && c = 0 + // and a* && [*0] && c* = [*0] // So if [*0] has been seen, check if alls term recognize the // empty word. if (weak_abs_seen) diff --git a/src/ltlast/multop.hh b/src/ltlast/multop.hh index 9b229a97d..f0f7b886e 100644 --- a/src/ltlast/multop.hh +++ b/src/ltlast/multop.hh @@ -41,7 +41,7 @@ namespace spot class multop : public ref_formula { public: - enum type { Or, And, AndNLM, Concat, Fusion }; + enum type { Or, OrRat, And, AndRat, AndNLM, Concat, Fusion }; /// List of formulae. typedef std::vector vec; @@ -68,24 +68,27 @@ namespace spot /// has been passed to spot::ltl::multop. Inside the vector, /// null pointers are ignored. /// - /// All operators (Or, And, Concat) are associative, and are - /// automatically inlined. Or and And are commutative, so their - /// argument are also sorted, to ensure that "a & b" is equal to - /// "b & a". For Or and And, duplicate arguments are also - /// removed. + /// Most operators (Or, OrRat, And, AndRat, Concat) are + /// associative, and are automatically inlined. Or, OrRat, And, + /// and AndRat are commutative, so their arguments are also + /// sorted, to ensure that "a & b" is equal to "b & a", also + /// duplicate arguments are removed. /// /// Furthermore this function can perform slight optimizations /// and may not return an ltl::multop object. For instance if /// the vector contains only one unique element, this this /// formula will be returned as-is. Neutral and absorbent element - /// are also taken care of. The following rewriting are performed + /// are also taken care of. The following rewritings are performed /// (the left patterns are rewritten as shown on the right): /// /// - And(Exps1...,1,Exps2...) = And(Exps1...,Exps2...) /// - And(Exps1...,0,Exps2...) = 0 - /// - And(Exps1...,[*0],Exps2...) = [*0] if all Expi accept [*0] - /// - And(Exps1...,[*0],Exps2...) = 0 if some Expi reject [*0] /// - And(Exp) = Exp + /// - AndRat(Exps1...,0,Exps2...) = 0 + /// - AndRat(Exps1...,BoolExp1,Exps2...,BoolExps2...) = + /// AndRat(Exps1...,Exps2...,And(BoolExp1,BoolExps2...)) + /// - AndRat(Exps1...,[*0],Exps2...) = [*0] if all Expi accept [*0] + /// - AndRat(Exps1...,[*0],Exps2...) = 0 if some Expi reject [*0] /// - AndNLM(Exps1...,1,Exps2...) = AndNLM(Exps1...,Exps2...) /// - AndNLM(Exps1...,0,Exps2...) = 0 /// - AndNLM(Exps1...,[*0],Exps2...) = AndNLM(Exps1...,Exps2...) @@ -93,8 +96,11 @@ namespace spot /// - AndNLM(Exps1...,BoolExp1,Exps2...,BoolExp2,Exps3...) = /// AndNLM(Exps1...,Exps2...,Exps3...,And(BoolExp1,BoolExp2)) /// - Or(Exps1...,1,Exps2...) = 1 - /// - Or(Exps1...,0,Exps2...) = And(Exps1...,Exps2...) + /// - Or(Exps1...,0,Exps2...) = Or(Exps1...,Exps2...) /// - Or(Exp) = Exp + /// - OrRat(Exps1...,0,Exps2...) = OrRat(Exps1...,Exps2...) + /// - OrRat(Exps1...,BoolExp1,Exps2...,BoolExps2...) = + /// OrRat(Exps1...,Exps2...,Or(BoolExp1,BoolExps2...)) /// - Concat(Exps1...,0,Exps2...) = 0 /// - Concat(Exps1...,[*0],Exps2...) = Concat(Exps1...,Exps2...) /// - Concat(Exp) = Exp @@ -221,6 +227,26 @@ namespace spot return is_multop(f, multop::And); } + /// \brief Cast \a f into a multop if it is an AndRat. + /// + /// Return 0 otherwise. + inline + multop* + is_AndRat(const formula* f) + { + return is_multop(f, multop::AndRat); + } + + /// \brief Cast \a f into a multop if it is an AndNLM. + /// + /// Return 0 otherwise. + inline + multop* + is_AndNLM(const formula* f) + { + return is_multop(f, multop::AndNLM); + } + /// \brief Cast \a f into a multop if it is an Or. /// /// Return 0 otherwise. @@ -231,6 +257,16 @@ namespace spot return is_multop(f, multop::Or); } + /// \brief Cast \a f into a multop if it is an OrRat. + /// + /// Return 0 otherwise. + inline + multop* + is_OrRat(const formula* f) + { + return is_multop(f, multop::OrRat); + } + /// \brief Cast \a f into a multop if it is a Concat. /// /// Return 0 otherwise. diff --git a/src/ltlparse/ltlparse.yy b/src/ltlparse/ltlparse.yy index 4bd6aa64a..0f4b51e4c 100644 --- a/src/ltlparse/ltlparse.yy +++ b/src/ltlparse/ltlparse.yy @@ -354,7 +354,7 @@ sere: booleanatom $$ = constant::false_instance(); } | sere OP_AND sere - { $$ = multop::instance(multop::And, $1, $3); } + { $$ = multop::instance(multop::AndRat, $1, $3); } | sere OP_AND error { missing_right_binop($$, $1, @2, "length-matching and operator"); } @@ -364,7 +364,7 @@ sere: booleanatom { missing_right_binop($$, $1, @2, "non-length-matching and operator"); } | sere OP_OR sere - { $$ = multop::instance(multop::Or, $1, $3); } + { $$ = multop::instance(multop::OrRat, $1, $3); } | sere OP_OR error { missing_right_binop($$, $1, @2, "or operator"); } | sere OP_CONCAT sere diff --git a/src/ltlvisit/mark.cc b/src/ltlvisit/mark.cc index 05d834e0e..1f5479a95 100644 --- a/src/ltlvisit/mark.cc +++ b/src/ltlvisit/mark.cc @@ -1,4 +1,4 @@ -// Copyright (C) 2010 Laboratoire de Recherche et Développement +// Copyright (C) 2010, 2012 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -89,14 +89,17 @@ namespace spot multop::vec* res = new multop::vec; switch (mo->op()) { - case multop::Or: + case multop::OrRat: + case multop::AndNLM: + case multop::AndRat: case multop::Concat: case multop::Fusion: + assert(!"unexpected operator"); + case multop::Or: for (unsigned i = 0; i < mos; ++i) res->push_back(recurse(mo->nth(i))); break; case multop::And: - case multop::AndNLM: { typedef std::set > pset; pset Epairs, EMpairs; @@ -125,10 +128,12 @@ namespace spot res->push_back(recurse(f)); break; case binop::EConcat: + assert(mo->op() == multop::And); Epairs.insert(std::make_pair(bo->first(), bo->second())); break; case binop::EConcatMarked: + assert(mo->op() == multop::And); EMpairs.insert(std::make_pair(bo->first(), bo->second())); break; diff --git a/src/ltlvisit/simplify.cc b/src/ltlvisit/simplify.cc index f7a309c85..cd936cb22 100644 --- a/src/ltlvisit/simplify.cc +++ b/src/ltlvisit/simplify.cc @@ -184,6 +184,8 @@ namespace spot break; } case multop::AndNLM: + case multop::AndRat: + case multop::OrRat: case multop::Concat: case multop::Fusion: assert(!"Unsupported operator"); @@ -566,6 +568,8 @@ namespace spot case multop::Concat: case multop::Fusion: case multop::AndNLM: + case multop::OrRat: + case multop::AndRat: break; } multop::vec* res = new multop::vec; @@ -583,6 +587,8 @@ namespace spot case multop::Concat: case multop::Fusion: case multop::AndNLM: + case multop::AndRat: + case multop::OrRat: { for (unsigned i = 0; i < mos; ++i) res->push_back(recurse_(mo->nth(i), false)); @@ -1765,10 +1771,14 @@ namespace spot multop::type op = mo->op(); if ((opt_.synt_impl | opt_.containment_checks) + && (op != multop::AndRat) + && (op != multop::AndNLM) + && (op != multop::OrRat) + && (op != multop::Concat) && (op != multop::Concat) && (op != multop::Fusion)) { - bool is_and = op != multop::Or; // And or AndNLM + bool is_and = op == multop::And; constant* neutral = is_and ? constant::false_instance() : constant::true_instance(); @@ -1842,691 +1852,701 @@ namespace spot switch (op) { case multop::And: - if (!mo->is_sere_formula()) - { - // a & X(G(a&b...) & c...) = Ga & X(G(b...) & c...) - // a & (Xa W b) = b R a - // a & (Xa U b) = b M a - // a & (b | X(b R a)) = b R a - // a & (b | X(b M a)) = b M a - if (!mo->is_X_free()) - { - typedef Sgi::hash_set > fset_t; - typedef Sgi::hash_map, - ptr_hash > fmap_t; - fset_t xgset; // XG(...) - fset_t xset; // X(...) - fmap_t wuset; // (X...)W(...) or (X...)U(...) + assert(!mo->is_sere_formula()); + { + // a & X(G(a&b...) & c...) = Ga & X(G(b...) & c...) + // a & (Xa W b) = b R a + // a & (Xa U b) = b M a + // a & (b | X(b R a)) = b R a + // a & (b | X(b M a)) = b M a + if (!mo->is_X_free()) + { + typedef Sgi::hash_set > fset_t; + typedef Sgi::hash_map, + ptr_hash > fmap_t; + fset_t xgset; // XG(...) + fset_t xset; // X(...) + fmap_t wuset; // (X...)W(...) or (X...)U(...) - unsigned s = res->size(); - std::vector tokill(s); + unsigned s = res->size(); + std::vector tokill(s); - // Make a pass to search for subterms - // of the form XGa or X(... & G(...&a&...) & ...) - for (unsigned n = 0; n < s; ++n) - { - if (!(*res)[n]) + // Make a pass to search for subterms + // of the form XGa or X(... & G(...&a&...) & ...) + for (unsigned n = 0; n < s; ++n) + { + if (!(*res)[n]) + continue; + + formula* xarg = is_XWU((*res)[n]); + if (xarg) + { + wuset[xarg].insert(n); continue; + } - formula* xarg = is_XWU((*res)[n]); - if (xarg) - { - wuset[xarg].insert(n); - continue; - } + // Now we are looking for + // - X(...) + // - b | X(b R ...) + // - b | X(b M ...) + if ((*res)[n]->is_X_free()) + continue; - // Now we are looking for - // - X(...) - // - b | X(b R ...) - // - b | X(b M ...) - if ((*res)[n]->is_X_free()) + binop* barg = is_bXbRM((*res)[n]); + if (barg) + { + wuset[barg->second()].insert(n); continue; + } - binop* barg = is_bXbRM((*res)[n]); - if (barg) - { - wuset[barg->second()].insert(n); - continue; - } + unop* uo = is_X((*res)[n]); + if (!uo) + continue; - unop* uo = is_X((*res)[n]); - if (!uo) - continue; - - formula* c = uo->child(); - multop* a; - unop* g; - if ((g = is_G(c))) - { + formula* c = uo->child(); + multop* a; + unop* g; + if ((g = is_G(c))) + { #define HANDLE_G multop* a2; \ - if ((a2 = is_And(g->child()))) \ - { \ - unsigned y = a2->size(); \ - for (unsigned n = 0; n < y; ++n) \ - xgset. \ - insert(a2->nth(n)->clone()); \ - } \ - else \ - { \ - xgset.insert(g->child()->clone()); \ - } - HANDLE_G; - } - else if ((a = is_And(c))) - { - unsigned z = a->size(); - for (unsigned m = 0; m < z; ++m) + if ((a2 = is_And(g->child()))) \ + { \ + unsigned y = a2->size(); \ + for (unsigned n = 0; n < y; ++n) \ + xgset. \ + insert(a2->nth(n)->clone()); \ + } \ + else \ + { \ + xgset.insert(g->child()->clone()); \ + } + HANDLE_G; + } + else if ((a = is_And(c))) + { + unsigned z = a->size(); + for (unsigned m = 0; m < z; ++m) + { + formula* x = a->nth(m); + if ((g = is_G(x))) + { + HANDLE_G; + } + else + { + xset.insert(x->clone()); + } + } + } + else + { + xset.insert(c->clone()); + } + (*res)[n]->destroy(); + (*res)[n] = 0; + } + // Make a second pass to check if the "a" + // terms can be used to simplify "Xa W b", + // "Xa U b", "b | X(b R a)", or "b | X(b M a)". + for (unsigned n = 0; n < s; ++n) + { + if (!(*res)[n]) + continue; + fmap_t::const_iterator gs = + wuset.find((*res)[n]); + if (gs == wuset.end()) + continue; + + const std::set& s = gs->second; + std::set::const_iterator g; + for (g = s.begin(); g != s.end(); ++g) + { + unsigned pos = *g; + binop* wu = is_binop((*res)[pos]); + if (wu) + { + // a & (Xa W b) = b R a + // a & (Xa U b) = b M a + binop::type t = (wu->op() == binop::U) + ? binop::M : binop::R; + unop* xa = down_cast(wu->first()); + formula* a = xa->child()->clone(); + formula* b = wu->second()->clone(); + wu->destroy(); + (*res)[pos] = binop::instance(t, b, a); + } + else + { + // a & (b | X(b R a)) = b R a + // a & (b | X(b M a)) = b M a + wu = is_bXbRM((*res)[pos]); + assert(wu); + wu->clone(); + (*res)[pos]->destroy(); + (*res)[pos] = wu; + } + // Remember to kill "a". + tokill[n] = true; + } + } + // Make third pass to search for terms 'a' + // that also appears as 'XGa'. Replace them + // by 'Ga' and delete XGa. + for (unsigned n = 0; n < s; ++n) + { + formula* x = (*res)[n]; + if (!x) + continue; + fset_t::const_iterator g = xgset.find(x); + if (g != xgset.end()) + { + // x can appear only once. + formula* gf = *g; + xgset.erase(g); + gf->destroy(); + (*res)[n] = unop::instance(unop::G, x); + } + else if (tokill[n]) + { + (*res)[n]->destroy(); + (*res)[n] = 0; + } + } + + multop::vec* xv = new multop::vec; + size_t xgs = xgset.size(); + xv->reserve(xset.size() + 1); + if (xgs > 0) + { + multop::vec* xgv = new multop::vec; + xgv->reserve(xgs); + fset_t::iterator i; + for (i = xgset.begin(); i != xgset.end(); ++i) + xgv->push_back(*i); + formula* gv = multop::instance(multop::And, xgv); + xv->push_back(unop::instance(unop::G, gv)); + } + fset_t::iterator j; + for (j = xset.begin(); j != xset.end(); ++j) + xv->push_back(*j); + formula* av = multop::instance(multop::And, xv); + res->push_back(unop::instance(unop::X, av)); + } + + // 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. + + // 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()) + { + 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; + } + break; + case multop::AndRat: + { + 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 + switch (r->op()) + { + case bunop::Star: + if (r->min() > 1 || r->max() < 1) + goto returnfalse; + ares->push_back(r->child()->clone()); + r->destroy(); + *i = 0; + break; + } + break; + } + case formula::MultOp: + { + multop* r = down_cast(*i); + unsigned rs = r->size(); + switch (r->op()) + { + case multop::Fusion: + //b && {r1:..:rn} = b && r1 && .. && rn + for (unsigned j = 0; j < rs; ++j) + ares->push_back(r->nth(j)->clone()); + r->destroy(); + *i = 0; + break; + case multop::Concat: + // b && {r1;...;rn} = + // - b && ri if there is only one ri + // that does not accept [*0] + // - b && (r1|...|rn) if all ri + // do not accept [*0] + // - 0 if more than one ri accept [*0] { - formula* x = a->nth(m); - if ((g = is_G(x))) + formula* ri = 0; + unsigned nonempty = 0; + for (unsigned j = 0; j < rs; ++j) { - HANDLE_G; + formula* jf = r->nth(j); + if (!jf->accepts_eword()) + { + ri = jf; + ++nonempty; + } + } + if (nonempty == 1) + { + ares->push_back(ri->clone()); + } + else if (nonempty == 0) + { + multop::vec* sum = new multop::vec; + for (unsigned j = 0; j < rs; ++j) + sum->push_back(r->nth(j) + ->clone()); + formula* sumf = + multop::instance(multop::OrRat, + sum); + ares->push_back(sumf); } else { - xset.insert(x->clone()); + goto returnfalse; } - } - } - else - { - xset.insert(c->clone()); - } - (*res)[n]->destroy(); - (*res)[n] = 0; - } - // Make a second pass to check if the "a" - // terms can be used to simplify "Xa W b", - // "Xa U b", "b | X(b R a)", or "b | X(b M a)". - for (unsigned n = 0; n < s; ++n) - { - if (!(*res)[n]) - continue; - fmap_t::const_iterator gs = - wuset.find((*res)[n]); - if (gs == wuset.end()) - continue; - - const std::set& s = gs->second; - std::set::const_iterator g; - for (g = s.begin(); g != s.end(); ++g) - { - unsigned pos = *g; - binop* wu = is_binop((*res)[pos]); - if (wu) - { - // a & (Xa W b) = b R a - // a & (Xa U b) = b M a - binop::type t = (wu->op() == binop::U) - ? binop::M : binop::R; - unop* xa = down_cast(wu->first()); - formula* a = xa->child()->clone(); - formula* b = wu->second()->clone(); - wu->destroy(); - (*res)[pos] = binop::instance(t, b, a); - } - else - { - // a & (b | X(b R a)) = b R a - // a & (b | X(b M a)) = b M a - wu = is_bXbRM((*res)[pos]); - assert(wu); - wu->clone(); - (*res)[pos]->destroy(); - (*res)[pos] = wu; - } - // Remember to kill "a". - tokill[n] = true; - } - } - // Make third pass to search for terms 'a' - // that also appears as 'XGa'. Replace them - // by 'Ga' and delete XGa. - for (unsigned n = 0; n < s; ++n) - { - formula* x = (*res)[n]; - if (!x) - continue; - fset_t::const_iterator g = xgset.find(x); - if (g != xgset.end()) - { - // x can appear only once. - formula* gf = *g; - xgset.erase(g); - gf->destroy(); - (*res)[n] = unop::instance(unop::G, x); - } - else if (tokill[n]) - { - (*res)[n]->destroy(); - (*res)[n] = 0; - } - } - - multop::vec* xv = new multop::vec; - size_t xgs = xgset.size(); - xv->reserve(xset.size() + 1); - if (xgs > 0) - { - multop::vec* xgv = new multop::vec; - xgv->reserve(xgs); - fset_t::iterator i; - for (i = xgset.begin(); i != xgset.end(); ++i) - xgv->push_back(*i); - formula* gv = multop::instance(multop::And, xgv); - xv->push_back(unop::instance(unop::G, gv)); - } - fset_t::iterator j; - for (j = xset.begin(); j != xset.end(); ++j) - xv->push_back(*j); - formula* av = multop::instance(multop::And, xv); - res->push_back(unop::instance(unop::X, av)); - } - - // 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. - - // 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()) - { - 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 - switch (r->op()) - { - case bunop::Star: - if (r->min() > 1 || r->max() < 1) - goto returnfalse; - ares->push_back(r->child()->clone()); r->destroy(); *i = 0; break; } - break; - } - case formula::MultOp: - { - multop* r = down_cast(*i); - unsigned rs = r->size(); - switch (r->op()) - { - case multop::Fusion: - //b && {r1:..:rn} = b && r1 && .. && rn - for (unsigned j = 0; j < rs; ++j) - ares->push_back(r->nth(j)->clone()); - r->destroy(); - *i = 0; - break; - case multop::Concat: - // b && {r1;...;rn} = - // - b && ri if there is only one ri - // that does not accept [*0] - // - b && (r1|...|rn) if all ri - // do not accept [*0] - // - 0 if more than one ri accept [*0] - { - formula* ri = 0; - unsigned nonempty = 0; - for (unsigned j = 0; j < rs; ++j) - { - formula* jf = r->nth(j); - if (!jf->accepts_eword()) - { - ri = jf; - ++nonempty; - } - } - if (nonempty == 1) - { - ares->push_back(ri->clone()); - } - else if (nonempty == 0) - { - multop::vec* sum = new multop::vec; - for (unsigned j = 0; j < rs; ++j) - sum->push_back(r->nth(j) - ->clone()); - formula* sumf = - multop::instance(multop::Or, sum); - ares->push_back(sumf); - } - else - { - goto returnfalse; - } - r->destroy(); - *i = 0; - break; - } - default: - goto common; - } - break; - } - default: - common: - ares->push_back(*i); - *i = 0; + default: + goto common; + } 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(); - delete s.res_other; - for (multop::vec::iterator i = ares->begin(); - i != ares->end(); ++i) + default: + common: + ares->push_back(*i); + *i = 0; + break; + } + delete s.res_other; + ares->push_back(b); + result_ = multop::instance(multop::AndRat, 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(); - delete ares; - result_ = constant::false_instance(); - return; - } - else - { - // No Boolean as argument of &&. - delete s.res_Bool; + delete s.res_other; + for (multop::vec::iterator i = ares->begin(); + i != ares->end(); ++i) + (*i)->destroy(); + delete ares; + result_ = constant::false_instance(); + 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 + // 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) + 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 ((*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; - } + } + } + if (!head1->empty()) + { + formula* h = + multop::instance(multop::And, head1); + formula* t = + multop::instance(multop::AndRat, 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::AndRat, 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) + // {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 ((*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; - } + } + } + if (!head3->empty()) + { + formula* h = + multop::instance(multop::AndRat, 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::AndRat, 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; - } - } + result_ = + multop::instance(multop::AndRat, s.res_other); + // If we altered the formula in some way, process + // it another time. + if (result_ != mo) + result_ = recurse_destroy(result_); + return; + } + } case multop::Or: { // a | X(F(a) | c...) = Fa | X(c...) @@ -2975,12 +2995,15 @@ namespace spot result_ = recurse_destroy(result_); return; } + case multop::OrRat: + // FIXME: No simplifications yet. + break; case multop::AndNLM: { mospliter s(mospliter::Split_Bool, res, c_); if (!s.res_Bool->empty()) { - // b1 & b2 & b3 = b1 && b2 && b3 + // b1 & b2 & b3 = b1 ∧ b2 ∧ b3 formula* b = multop::instance(multop::And, s.res_Bool); // now we just consider b & rest @@ -3001,7 +3024,7 @@ namespace spot multop::instance(multop::Fusion, b->clone(), rest); result_ = - multop::instance(multop::Or, b, brest); + multop::instance(multop::OrRat, b, brest); } else { @@ -3026,9 +3049,9 @@ namespace spot delete s.res_Bool; // Look for occurrences of {b;r} or {b:r}. We have - // {b1;r1}&{b2;r2} = {b1&&b2};{r1&r2} + // {b1;r1}&{b2;r2} = {b1∧b2};{r1&r2} // head1 tail1 - // {b1:r1}&{b2:r2} = {b1&&b2}:{r1&r2} + // {b1:r1}&{b2:r2} = {b1∧b2}:{r1&r2} // head2 tail2 multop::vec* head1 = new multop::vec; @@ -3076,11 +3099,12 @@ namespace spot } if (!head1->empty()) { - formula* h = multop::instance(multop::And, head1); + formula* h = + multop::instance(multop::And, head1); formula* t = multop::instance(multop::AndNLM, tail1); - formula* f = multop::instance(multop::Concat, - h, t); + formula* f = + multop::instance(multop::Concat, h, t); s.res_other->push_back(f); } else @@ -3090,11 +3114,12 @@ namespace spot } if (!head2->empty()) { - formula* h = multop::instance(multop::And, head2); + formula* h = + multop::instance(multop::And, head2); formula* t = multop::instance(multop::AndNLM, tail2); - formula* f = multop::instance(multop::Fusion, - h, t); + formula* f = + multop::instance(multop::Fusion, h, t); s.res_other->push_back(f); } else @@ -3103,9 +3128,9 @@ namespace spot delete tail2; } - // {r1;b1}&{r2;b2} = {r1&r2};{b1&&b2} + // {r1;b1}&{r2;b2} = {r1&r2};{b1∧b2} // head3 tail3 - // {r1:b1}&{r2:b2} = {r1&r2}:{b1&&b2} + // {r1:b1}&{r2:b2} = {r1&r2}:{b1∧b2} // head4 tail4 multop::vec* head3 = new multop::vec; multop::vec* tail3 = new multop::vec; @@ -3153,9 +3178,10 @@ namespace spot { formula* h = multop::instance(multop::AndNLM, head3); - formula* t = multop::instance(multop::And, tail3); - formula* f = multop::instance(multop::Concat, - h, t); + formula* t = + multop::instance(multop::And, tail3); + formula* f = + multop::instance(multop::Concat, h, t); s.res_other->push_back(f); } else @@ -3167,9 +3193,10 @@ namespace spot { formula* h = multop::instance(multop::AndNLM, head4); - formula* t = multop::instance(multop::And, tail4); - formula* f = multop::instance(multop::Fusion, - h, t); + formula* t = + multop::instance(multop::And, tail4); + formula* f = + multop::instance(multop::Fusion, h, t); s.res_other->push_back(f); } else @@ -3441,6 +3468,8 @@ namespace spot case multop::Concat: case multop::Fusion: case multop::AndNLM: + case multop::AndRat: + case multop::OrRat: break; } break; @@ -3524,6 +3553,8 @@ namespace spot case multop::Concat: case multop::Fusion: case multop::AndNLM: + case multop::AndRat: + case multop::OrRat: break; } break; diff --git a/src/ltlvisit/tostring.cc b/src/ltlvisit/tostring.cc index 88ab06a33..ab6d3d076 100644 --- a/src/ltlvisit/tostring.cc +++ b/src/ltlvisit/tostring.cc @@ -60,8 +60,9 @@ namespace spot KF, KG, KOr, + KOrRat, KAnd, - KAndLM, + KAndRat, KAndNLM, KConcat, KFusion @@ -89,6 +90,7 @@ namespace spot "F", "G", " | ", + " | ", " & ", " && ", " & ", @@ -118,6 +120,7 @@ namespace spot "<>", "[]", " || ", + " || ", " && ", " && ", // not supported " & ", // not supported @@ -623,8 +626,14 @@ namespace spot case multop::Or: k = KOr; break; + case multop::OrRat: + k = KOrRat; + break; case multop::And: - k = in_ratexp_ ? KAndLM : KAnd; + k = in_ratexp_ ? KAndRat : KAnd; + break; + case multop::AndRat: + k = KAndRat; break; case multop::AndNLM: k = KAndNLM; diff --git a/src/tgba/formula2bdd.cc b/src/tgba/formula2bdd.cc index 202b9fad8..66e911ddf 100644 --- a/src/tgba/formula2bdd.cc +++ b/src/tgba/formula2bdd.cc @@ -1,5 +1,5 @@ -// Copyright (C) 2009, 2010 Laboratoire de Recherche et Développement -// de l'Epita (LRDE). +// Copyright (C) 2009, 2010, 2012 Laboratoire de Recherche et +// Développement de l'Epita (LRDE). // Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris // 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), // Université Pierre et Marie Curie. @@ -152,6 +152,8 @@ namespace spot case multop::Concat: case multop::Fusion: case multop::AndNLM: + case multop::OrRat: + case multop::AndRat: assert(!"unsupported operator"); } assert(op != -1); diff --git a/src/tgbaalgos/eltl2tgba_lacim.cc b/src/tgbaalgos/eltl2tgba_lacim.cc index 16c4ada42..6ce0fb967 100644 --- a/src/tgbaalgos/eltl2tgba_lacim.cc +++ b/src/tgbaalgos/eltl2tgba_lacim.cc @@ -1,4 +1,4 @@ -// Copyright (C) 2008, 2009, 2010 Laboratoire de Recherche et +// Copyright (C) 2008, 2009, 2010, 2012 Laboratoire de Recherche et // Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -168,6 +168,8 @@ namespace spot case multop::Concat: case multop::Fusion: case multop::AndNLM: + case multop::AndRat: + case multop::OrRat: assert(!"unsupported operator"); } assert(op != -1); diff --git a/src/tgbaalgos/ltl2taa.cc b/src/tgbaalgos/ltl2taa.cc index b6cea7d0c..4ad623479 100644 --- a/src/tgbaalgos/ltl2taa.cc +++ b/src/tgbaalgos/ltl2taa.cc @@ -1,5 +1,5 @@ -// Copyright (C) 2009, 2010 Laboratoire de Recherche et Développement -// de l'Epita (LRDE). +// Copyright (C) 2009, 2010, 2012 Laboratoire de Recherche et +// Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -332,6 +332,8 @@ namespace spot case multop::Concat: case multop::Fusion: case multop::AndNLM: + case multop::AndRat: + case multop::OrRat: assert(!"unsupported operator"); return; } diff --git a/src/tgbaalgos/ltl2tgba_fm.cc b/src/tgbaalgos/ltl2tgba_fm.cc index 4a44fb24e..8ddb13724 100644 --- a/src/tgbaalgos/ltl2tgba_fm.cc +++ b/src/tgbaalgos/ltl2tgba_fm.cc @@ -243,6 +243,12 @@ namespace spot return multop::instance(op, v); } + formula* + conj_bdd_to_sere(bdd b) const + { + return conj_bdd_to_formula(b, multop::AndRat); + } + formula* bdd_to_formula(bdd f) { @@ -259,6 +265,22 @@ namespace spot return multop::instance(multop::Or, v); } + formula* + bdd_to_sere(bdd f) + { + if (f == bddfalse) + return constant::false_instance(); + + multop::vec* v = new multop::vec; + + minato_isop isop(f); + bdd cube; + while ((cube = isop.next()) != bddfalse) + v->push_back(conj_bdd_to_sere(cube)); + + return multop::instance(multop::OrRat, v); + } + void conj_bdd_to_acc(tgba_explicit_formula* a, bdd b, state_explicit_formula::transition* t) @@ -429,7 +451,7 @@ namespace spot { bdd label = bdd_exist(cube, dict_.next_set); bdd dest_bdd = bdd_existcomp(cube, dict_.next_set); - formula* dest = dict_.conj_bdd_to_formula(dest_bdd); + formula* dest = dict_.conj_bdd_to_sere(dest_bdd); if (dest == constant::empty_word_instance()) { out |= label & next_to_concat(); @@ -537,12 +559,12 @@ namespace spot } else { - // if "f" accepts the empty words, doing the above would + // if "f" accepts the empty word, doing the above would // lead to an infinite loop: // f*;g -> f;f*;g | g // f;f*;g -> f*;g | ... // - // So we do in two steps: + // So we do it in three steps: // 1. translate f, // 2. append f*;g to all destinations // 3. add |g @@ -556,8 +578,7 @@ namespace spot { bdd label = bdd_exist(cube, dict_.next_set); bdd dest_bdd = bdd_existcomp(cube, dict_.next_set); - formula* dest = - dict_.conj_bdd_to_formula(dest_bdd); + formula* dest = dict_.conj_bdd_to_sere(dest_bdd); formula* dest2; int x; if (dest == constant::empty_word_instance()) @@ -623,7 +644,7 @@ namespace spot { delete non_final; // (a* & b*);c = (a*|b*);c - formula* f = multop::instance(multop::Or, final); + formula* f = multop::instance(multop::OrRat, final); res_ = recurse_and_concat(f); f->destroy(); break; @@ -635,7 +656,7 @@ namespace spot // (F_1 & ... & F_n & N_1 & ... & N_m) // = (F_1 | ... | F_n);[*] && (N_1 & ... & N_m) // | (F_1 | ... | F_n) && (N_1 & ... & N_m);[*] - formula* f = multop::instance(multop::Or, final); + formula* f = multop::instance(multop::OrRat, final); formula* n = multop::instance(multop::AndNLM, non_final); formula* t = bunop::instance(bunop::Star, constant::true_instance()); @@ -643,9 +664,9 @@ namespace spot f->clone(), t->clone()); formula* nt = multop::instance(multop::Concat, n->clone(), t); - formula* ftn = multop::instance(multop::And, ft, n); - formula* fnt = multop::instance(multop::And, f, nt); - formula* all = multop::instance(multop::Or, ftn, fnt); + formula* ftn = multop::instance(multop::AndRat, ft, n); + formula* fnt = multop::instance(multop::AndRat, f, nt); + formula* all = multop::instance(multop::OrRat, ftn, fnt); res_ = recurse_and_concat(all); all->destroy(); break; @@ -673,15 +694,15 @@ namespace spot f, star->clone()); conj->push_back(f); } - disj->push_back(multop::instance(multop::And, conj)); + disj->push_back(multop::instance(multop::AndRat, conj)); } star->destroy(); - formula* all = multop::instance(multop::Or, disj); + formula* all = multop::instance(multop::OrRat, disj); res_ = recurse_and_concat(all); all->destroy(); break; } - case multop::And: + case multop::AndRat: { unsigned s = node->size(); @@ -707,7 +728,7 @@ namespace spot node->destroy(); break; } - case multop::Or: + case multop::OrRat: { res_ = bddfalse; unsigned s = node->size(); @@ -749,7 +770,7 @@ namespace spot { bdd label = bdd_exist(cube, dict_.next_set); bdd dest_bdd = bdd_existcomp(cube, dict_.next_set); - formula* dest = dict_.conj_bdd_to_formula(dest_bdd); + formula* dest = dict_.conj_bdd_to_sere(dest_bdd); if (dest->accepts_eword()) { @@ -786,6 +807,9 @@ namespace spot tail->destroy(); break; } + case multop::And: + case multop::Or: + assert(!"not a rational operator"); } } @@ -814,10 +838,10 @@ namespace spot { // static unsigned indent = 0; // for (unsigned i = indent; i > 0; --i) - // std::cerr << "| "; + // std::cerr << "| "; // std::cerr << "translate_ratexp[" << to_string(f); // if (to_concat) - // std::cerr << ", " << to_string(to_concat); + // std::cerr << ", " << to_string(to_concat); // std::cerr << "]" << std::endl; // ++indent; bdd res; @@ -839,7 +863,7 @@ namespace spot } // --indent; // for (unsigned i = indent; i > 0; --i) - // std::cerr << "| "; + // std::cerr << "| "; // std::cerr << "\\ "; // bdd_print_set(std::cerr, dict.dict, res) << std::endl; return res; @@ -891,7 +915,7 @@ namespace spot all_props -= label; const formula* dest = - dict_.bdd_to_formula(bdd_exist(res & label, dict_.var_set)); + dict_.bdd_to_sere(bdd_exist(res & label, dict_.var_set)); f2a_t::const_iterator i = f2a_.find(dest); if (i != f2a_.end() && i->second == 0) @@ -1218,8 +1242,7 @@ namespace spot all_props -= label; formula* dest = - dict_.bdd_to_formula(bdd_exist(f1 & label, - dict_.var_set)); + dict_.bdd_to_sere(bdd_exist(f1 & label, dict_.var_set)); // !{ Exp } is false if Exp accepts the empty word. if (dest->accepts_eword()) @@ -1347,8 +1370,8 @@ namespace spot all_props -= label; formula* dest = - dict_.bdd_to_formula(bdd_exist(f1 & label, - dict_.var_set)); + dict_.bdd_to_sere(bdd_exist(f1 & label, + dict_.var_set)); const formula* dest2 = binop::instance(op, dest, node->second()->clone()); @@ -1371,7 +1394,7 @@ namespace spot { bdd label = bdd_exist(cube, dict_.next_set); bdd dest_bdd = bdd_existcomp(cube, dict_.next_set); - formula* dest = dict_.conj_bdd_to_formula(dest_bdd); + formula* dest = dict_.conj_bdd_to_sere(dest_bdd); if (dest == constant::empty_word_instance()) { @@ -1420,7 +1443,7 @@ namespace spot { bdd label = bdd_exist(cube, dict_.next_set); bdd dest_bdd = bdd_existcomp(cube, dict_.next_set); - formula* dest = dict_.conj_bdd_to_formula(dest_bdd); + formula* dest = dict_.conj_bdd_to_sere(dest_bdd); formula* dest2 = binop::instance(op, dest, node->second()->clone()); @@ -1478,6 +1501,8 @@ namespace spot case multop::Concat: case multop::Fusion: case multop::AndNLM: + case multop::AndRat: + case multop::OrRat: assert(!"Not an LTL operator"); break; } @@ -1699,7 +1724,7 @@ namespace spot // std::cerr << "Marked: " << t.has_marked << std::endl; // std::cerr << "Mark all: " << !f->is_marked() << std::endl; // std::cerr << "Transitions:" << std::endl; - // trace_ltl_bdd(v_.get_dict(), t.symbolic); + // trace_ltl_bdd(d_, t.symbolic); // std::cerr << "-----" << std::endl; if (t.has_rational) diff --git a/src/tgbaalgos/ltl2tgba_lacim.cc b/src/tgbaalgos/ltl2tgba_lacim.cc index 1bf4d4d15..dcd360885 100644 --- a/src/tgbaalgos/ltl2tgba_lacim.cc +++ b/src/tgbaalgos/ltl2tgba_lacim.cc @@ -1,7 +1,8 @@ -// Copyright (C) 2009, 2010 Laboratoire de Recherche et Développement -// de l'Epita (LRDE). +// -*- coding: utf-8 -*- +// Copyright (C) 2009, 2010, 2012 Laboratoire de Recherche et +// Développement de l'Epita (LRDE). // Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), -// département Systèmes Répartis Coopératifs (SRC), Université Pierre +// département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. // // This file is part of Spot, a model checking library. @@ -103,7 +104,7 @@ namespace spot /* `x | next', doesn't actually encode the fact that x should be fulfilled eventually. We ensure this by - creating a new generalized Büchi acceptance set, Acc[x], + creating a new generalized Büchi acceptance set, Acc[x], and leave out of this set any transition going off NOW without checking X. Such acceptance conditions are checked for during the emptiness check. @@ -266,6 +267,8 @@ namespace spot case multop::Concat: case multop::Fusion: case multop::AndNLM: + case multop::AndRat: + case multop::OrRat: assert(!"unsupported operator"); } assert(op != -1);