diff --git a/NEWS b/NEWS index 10cfd3c5a..f2190c1e0 100644 --- a/NEWS +++ b/NEWS @@ -157,6 +157,10 @@ New in spot 1.2.5a (not yet released) version 8.0 of Org-mode. (This was only a problem if you build from the git repository, or if you want to edit the documentation.) + - recent to changes to libstd++ (as shipped by g++ 4.9.2) have + demonstrated that the order of transitions output by the + LTL->TGBA translation used to be dependent on the implementation + of the STL. This is now fixed. New in spot 1.2.5 (2014-08-21) diff --git a/src/tgbaalgos/ltl2tgba_fm.cc b/src/tgbaalgos/ltl2tgba_fm.cc index cb3497dd2..3e71b7d80 100644 --- a/src/tgbaalgos/ltl2tgba_fm.cc +++ b/src/tgbaalgos/ltl2tgba_fm.cc @@ -34,6 +34,7 @@ #include #include #include +#include #include "ltl2tgba_fm.hh" #include "tgba/bddprint.hh" #include "tgbaalgos/sccinfo.hh" @@ -2093,28 +2094,56 @@ namespace spot } - typedef std::map prom_map; - typedef std::unordered_map dest_map; - - static void - fill_dests(translate_dict& d, dest_map& dests, bdd label, const formula* dest) + namespace { - bdd conds = bdd_existcomp(label, d.var_set); - bdd promises = bdd_existcomp(label, d.a_set); + struct transition + { + const formula* dest; + bdd prom; + bdd cond; - dest_map::iterator i = dests.find(dest); - if (i == dests.end()) + transition(const formula* dest, bdd cond, bdd prom) + : dest(dest), prom(prom), cond(cond) { - dests[dest][promises] = conds; } - else + + transition(const transition& other) + : dest(other.dest), prom(other.prom), cond(other.cond) { - i->second[promises] |= conds; - dest->destroy(); } + + bool operator<(const transition& other) const + { + ltl::formula_ptr_less_than lt; + if (lt(dest, other.dest)) + return true; + if (lt(other.dest, dest)) + return false; + if (prom.id() < other.prom.id()) + return true; + if (prom.id() > other.prom.id()) + return false; + return cond.id() < other.cond.id(); + } + }; + + bool postponement_cmp(const transition& lhs, const transition& rhs) + { + if (lhs.prom.id() < rhs.prom.id()) + return true; + if (lhs.prom.id() > rhs.prom.id()) + return false; + if (lhs.cond.id() < rhs.cond.id()) + return true; + if (lhs.cond.id() > rhs.cond.id()) + return false; + ltl::formula_ptr_less_than lt; + return lt(lhs.dest, rhs.dest); + } + + typedef std::vector dest_map; } - tgba_digraph_ptr ltl_to_tgba_fm(const formula* f, const bdd_dict_ptr& dict, bool exprop, bool symb_merge, bool branching_postponement, @@ -2206,6 +2235,7 @@ namespace spot formulae_to_translate.insert(f2); a->set_init_state(namer->new_state(f2)); + dest_map dests; while (!formulae_to_translate.empty()) { // Pick one formula. @@ -2216,6 +2246,9 @@ namespace spot const translate_dict::translated& t = fc.translate(now); bdd res = t.symbolic; + if (res == bddfalse) + continue; + // Handle exclusive events. if (unobs) { @@ -2253,7 +2286,7 @@ namespace spot // // In `exprop' mode, considering all possible combinations of // outgoing propositions generalizes the above trick. - dest_map dests; + dests.clear(); // Compute all outgoing arcs. @@ -2274,9 +2307,6 @@ namespace spot one_prop_set = bdd_satoneset(all_props, var_set, bddtrue); all_props -= one_prop_set; - typedef std::map succ_map; - succ_map succs; - // Compute prime implicants. // The reason we use prime implicants and not bdd_satone() // is that we do not want to get any negation in front of Next @@ -2315,39 +2345,36 @@ namespace spot if (symb_merge) dest = fc.canonize(dest); - // If we are not postponing the branching, we can - // declare the outgoing transitions immediately. - // Otherwise, we merge transitions with identical - // label, and declare the outgoing transitions in a - // second loop. - if (!branching_postponement) - { - fill_dests(d, dests, label, dest); - } - else - { - succ_map::iterator si = succs.find(label); - if (si == succs.end()) - succs[label] = dest; - else - si->second = - multop::instance(multop::Or, si->second, dest); - } + bdd conds = bdd_existcomp(label, d.var_set); + bdd promises = bdd_existcomp(label, d.a_set); + dests.push_back(transition(dest, conds, promises)); } - if (branching_postponement) - for (succ_map::const_iterator si = succs.begin(); - si != succs.end(); ++si) - fill_dests(d, dests, si->first, si->second); } - // Check for an arc going to 1 (True). Register it first, that - // way it will be explored before others during model checking. - auto truef = constant::true_instance(); - dest_map::const_iterator i = dests.find(truef); - // COND_FOR_TRUE is the conditions of the True arc, so we - // can remove them from all other arcs. It might sounds that - // this is not needed when exprop is used, but in fact it is - // complementary. + assert(dests.size() > 0); + if (branching_postponement && dests.size() > 1) + { + std::sort(dests.begin(), dests.end(), postponement_cmp); + // Iterate over all dests, and merge the destination of + // transitions with identical labels. + dest_map::iterator out = dests.begin(); + dest_map::const_iterator in = out; + do + { + transition t = *in; + while (++in != dests.end() + && t.cond == in->cond && t.prom == in->prom) + t.dest = multop::instance(multop::Or, t.dest, in->dest); + *out++ = t; + } + while (in != dests.end()); + dests.erase(out, dests.end()); + } + std::sort(dests.begin(), dests.end()); + // If we have some transitions to true, they are the first + // ones. Remove the sum of their conditions from other + // transitions. It might sounds that this is not needed when + // exprop is used, but in fact it is complementary. // // Consider // f = r(X(1) R p) = p.(1 + r(X(1) R p)) @@ -2360,61 +2387,60 @@ namespace spot // f ----> 1 // // because there is no point in looping on f if we can go to 1. - bdd cond_for_true = bddfalse; - if (i != dests.end()) + if (dests.front().dest == constant::true_instance()) { - // When translating LTL for an event-based logic with - // unobservable events, the 1 state should accept all events, - // even unobservable events. - if (unobs && now == truef) - cond_for_true = all_events; - else - { - // There should be only one transition going to 1 (true) ... - assert(i->second.size() == 1); - prom_map::const_iterator j = i->second.begin(); - // ... and it is not expected to make any promises (unless - // fair loop approximations are used). - assert(fair_loop_approx || j->first == bddtrue); - cond_for_true = j->second; - } - if (!namer->has_state(truef)) - { - formulae_to_translate.insert(truef); - namer->new_state(truef); - } - namer->new_transition(now, truef, cond_for_true, 0U); + dest_map::iterator i = dests.begin(); + bdd c = bddfalse; + while (i != dests.end() && i->dest == constant::true_instance()) + c |= i++->cond; + for (; i != dests.end(); ++i) + i->cond -= c; } - // Register other transitions. - for (i = dests.begin(); i != dests.end(); ++i) - { - const formula* dest = i->first; - if (dest == truef) - continue; - // The cond_for_true optimization can cause some - // transitions to be removed. So we have to remember - // whether a formula is actually reachable. - bool reachable = false; - // Will this be a new state? - bool seen = namer->has_state(dest); + // Create transitions in the automaton + { + dest_map::const_iterator in = dests.begin(); + do + { + // Merge transitions with same destination and + // acceptance. + transition t = *in; + while (++in != dests.end() + && t.prom == in->prom && t.dest == in->dest) + { + t.cond |= in->cond; + in->dest->destroy(); + } + // Actually create the transition + if (t.cond != bddfalse) + { + // When translating LTL for an event-based logic + // with unobservable events, the 1 state should + // accept all events, even unobservable events. + if (unobs + && t.dest == constant::true_instance() + && now == constant::true_instance()) + t.cond = all_events; - for (auto& j: i->second) - { - bdd cond = j.second - cond_for_true; - if (cond == bddfalse) // Skip false transitions. - continue; - if (!reachable && !seen) - namer->new_state(dest); - reachable = true; - namer->new_transition(now, dest, cond, d.bdd_to_mark(j.first)); - } + // Will this be a new state? + bool seen = namer->has_state(t.dest); - if (reachable && !seen) - formulae_to_translate.insert(dest); - else - dest->destroy(); - } + if (!seen) + { + formulae_to_translate.insert(t.dest); + namer->new_state(t.dest); + } + + namer->new_transition(now, t.dest, t.cond, + d.bdd_to_mark(t.prom)); + if (seen) + t.dest->destroy(); + } + else + t.dest->destroy(); + } + while (in != dests.end()); + } } for (auto n: namer->names()) diff --git a/src/tgbatest/ltl2ta.test b/src/tgbatest/ltl2ta.test index 412bb5a41..3a97bde17 100755 --- a/src/tgbatest/ltl2ta.test +++ b/src/tgbatest/ltl2ta.test @@ -169,12 +169,12 @@ in: Fa & b & GFc & Gd -TA -DS -RT | 12 | 126 | 8 -TA -DS -lv | 29 | 315 | 17 -TA -DS -lv -RT | 13 | 140 | 8 --TA -DS -sp | 28 | 306 | 16 --TA -DS -sp -RT | 12 | 134 | 7 +-TA -DS -sp | 28 | 309 | 16 +-TA -DS -sp -RT | 12 | 137 | 7 -TA -DS -lv -sp | 29 | 315 | 17 -TA -DS -lv -sp -RT | 13 | 140 | 8 --x -TA -DS -in | 29 | 240 | 13 --x -TA -DS -in -RT | 12 | 93 | 7 +-x -TA -DS -in | 29 | 254 | 13 +-x -TA -DS -in -RT | 12 | 96 | 7 in: Fa & a & GFc & Gc -TGTA | 4 | 8 | XXX -TGTA -RT | 3 | 6 | XXX @@ -326,13 +326,13 @@ in: # Make sure '(G (p -> F q)) && ((X (p) U q) || ! X (p U (p && q)))' in: # has 21 states and 96 transitions before minimization, and in: # has 20 states and 89 transitions, after minimization. in: (G (p -> F q)) && ((X (p) U q) || ! X (p U (p && q))) --TGTA | 21 | 129 | XXX +-TGTA | 21 | 127 | XXX -TGTA -RT | 17 | 93 | XXX -TA | 20 | 92 | 12 -TA -RT | 15 | 57 | 9 -TA -lv | 21 | 104 | 6 -TA -lv -RT | 17 | 75 | 4 --TA -sp | 20 | 102 | 5 +-TA -sp | 20 | 100 | 5 -TA -sp -RT | 16 | 70 | 3 -TA -lv -sp | 21 | 104 | 6 -TA -lv -sp -RT | 17 | 75 | 4 @@ -340,8 +340,8 @@ in: (G (p -> F q)) && ((X (p) U q) || ! X (p U (p && q))) -TA -DS -RT | 18 | 81 | 13 -TA -DS -lv | 21 | 104 | 11 -TA -DS -lv -RT | 20 | 99 | 11 --TA -DS -sp | 20 | 102 | 10 --TA -DS -sp -RT | 19 | 97 | 10 +-TA -DS -sp | 20 | 100 | 10 +-TA -DS -sp -RT | 19 | 95 | 10 -TA -DS -lv -sp | 21 | 104 | 11 -TA -DS -lv -sp -RT | 20 | 99 | 11 -x -TA -DS -in | 19 | 66 | 9 @@ -389,26 +389,26 @@ in: Gq|Gr|(G(q|FGp)&G(r|FG!p)) -x -TA -DS -in | 33 | 152 | 25 -x -TA -DS -in -RT | 21 | 112 | 17 in: FG((WaitRight4 M (HasRight1 W GWaitLeft0)) M HasLeft4) --TGTA | 45 | 717 | XXX +-TGTA | 45 | 730 | XXX -TGTA -RT | 35 | 598 | XXX -TA | 44 | 602 | 16 -TA -RT | 33 | 482 | 9 -TA -lv | 45 | 676 | 9 -TA -lv -RT | 35 | 566 | 4 --TA -sp | 44 | 654 | 8 +-TA -sp | 44 | 667 | 8 -TA -sp -RT | 34 | 545 | 3 -TA -lv -sp | 45 | 676 | 9 -TA -lv -sp -RT | 35 | 566 | 4 -TA -DS | 54 | 722 | 26 --TA -DS -RT | 38 | 534 | 17 +-TA -DS -RT | 42 | 600 | 19 -TA -DS -lv | 55 | 800 | 19 --TA -DS -lv -RT | 39 | 608 | 11 --TA -DS -sp | 54 | 776 | 18 --TA -DS -sp -RT | 38 | 586 | 10 +-TA -DS -lv -RT | 44 | 694 | 13 +-TA -DS -sp | 54 | 797 | 18 +-TA -DS -sp -RT | 43 | 683 | 12 -TA -DS -lv -sp | 55 | 800 | 19 --TA -DS -lv -sp -RT | 39 | 608 | 11 --x -TA -DS -in | 55 | 696 | 11 --x -TA -DS -in -RT | 42 | 603 | 8 +-TA -DS -lv -sp -RT | 44 | 694 | 13 +-x -TA -DS -in | 55 | 700 | 11 +-x -TA -DS -in -RT | 39 | 566 | 8 in: G(F(GWaitLeft7 U Idle4) U (WaitLeft2 M IsEating2)) -TGTA | 69 | 1539 | XXX -TGTA -RT | 49 | 935 | XXX @@ -421,15 +421,15 @@ in: G(F(GWaitLeft7 U Idle4) U (WaitLeft2 M IsEating2)) -TA -lv -sp | 68 | 1443 | 16 -TA -lv -sp -RT | 56 | 1179 | 15 -TA -DS | 124 | 2964 | 44 --TA -DS -RT | 96 | 2099 | 42 +-TA -DS -RT | 100 | 2285 | 42 -TA -DS -lv | 125 | 3028 | 42 --TA -DS -lv -RT | 97 | 2149 | 40 --TA -DS -sp | 124 | 3008 | 41 --TA -DS -sp -RT | 96 | 2129 | 39 +-TA -DS -lv -RT | 101 | 2339 | 40 +-TA -DS -sp | 124 | 3012 | 41 +-TA -DS -sp -RT | 100 | 2324 | 39 -TA -DS -lv -sp | 125 | 3028 | 42 --TA -DS -lv -sp -RT | 97 | 2149 | 40 +-TA -DS -lv -sp -RT | 101 | 2339 | 40 -x -TA -DS -in | 125 | 1838 | 25 --x -TA -DS -in -RT | 90 | 1368 | 25 +-x -TA -DS -in -RT | 89 | 1344 | 25 EOF sed -n 's/in: \(.*\)/\1/p' checkta.txt > input.txt