diff --git a/src/bin/ltl2tgba.cc b/src/bin/ltl2tgba.cc index 0d59b79f0..bd13d062a 100644 --- a/src/bin/ltl2tgba.cc +++ b/src/bin/ltl2tgba.cc @@ -34,6 +34,7 @@ #include "common_post.hh" #include "ltlast/formula.hh" +#include "ltlvisit/tostring.hh" #include "tgba/tgbaexplicit.hh" #include "tgbaalgos/dotty.hh" #include "tgbaalgos/lbtt.hh" @@ -231,17 +232,6 @@ namespace s.c_str()); } - if (utf8) - { - spot::tgba* a = const_cast(aut); - if (spot::tgba_explicit_formula* tef = - dynamic_cast(a)) - tef->enable_utf8(); - else if (spot::sba_explicit_formula* sef = - dynamic_cast(a)) - sef->enable_utf8(); - } - switch (format) { case Dot: diff --git a/src/bin/ltl2tgta.cc b/src/bin/ltl2tgta.cc index 8b471770e..3a0f12166 100644 --- a/src/bin/ltl2tgta.cc +++ b/src/bin/ltl2tgta.cc @@ -33,6 +33,7 @@ #include "common_post.hh" #include "ltlparse/public.hh" +#include "ltlvisit/tostring.hh" #include "ltlvisit/simplify.hh" #include "tgbaalgos/dotty.hh" #include "tgbaalgos/ltl2tgba_fm.hh" @@ -184,17 +185,6 @@ namespace s.c_str()); } - if (utf8) - { - spot::tgba* a = const_cast(aut); - if (spot::tgba_explicit_formula* tef = - dynamic_cast(a)) - tef->enable_utf8(); - else if (spot::sba_explicit_formula* sef = - dynamic_cast(a)) - sef->enable_utf8(); - } - bdd ap_set = atomic_prop_collect_as_bdd(f, aut); if (ta_type != TGTA) diff --git a/src/graph/ngraph.hh b/src/graph/ngraph.hh index 5d1b66b9e..42a97816e 100644 --- a/src/graph/ngraph.hh +++ b/src/graph/ngraph.hh @@ -94,6 +94,16 @@ namespace spot return state_to_name.at(s); } + bool has_state(name n) const + { + return name_to_state.find(n) != name_to_state.end(); + } + + state_to_name_t& names() + { + return state_to_name; + } + template transition new_transition(name src, name dst, Args&&... args) diff --git a/src/priv/acccompl.cc b/src/priv/acccompl.cc index 3212f5718..17c01e1fa 100644 --- a/src/priv/acccompl.cc +++ b/src/priv/acccompl.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012 Laboratoire de Recherche et Developpement de -// l'Epita (LRDE) +// Copyright (C) 2012, 2014 Laboratoire de Recherche et Developpement +// de l'Epita (LRDE) // // This file is part of Spot, a model checking library. // @@ -18,6 +18,7 @@ // along with this program. If not, see . #include "acccompl.hh" +#include namespace spot { @@ -60,6 +61,8 @@ namespace spot if (acc == bddtrue) return all_; + assert(acc != bddfalse); + // Since we never cache a unique positive bdd, we can reuse the // same cache. In fact the only kind of acc we will receive in // this method, are a conjunction of positive acceptance @@ -70,12 +73,13 @@ namespace spot bdd res = all_; bdd cond = acc; + bdd neg = bddtrue; while (cond != bddtrue) { - res &= bdd_nithvar(bdd_var(cond)); + neg &= bdd_nithvar(bdd_var(cond)); cond = bdd_high(cond); } - + res &= neg; cache_[acc] = res; return res; diff --git a/src/tgba/tgbagraph.hh b/src/tgba/tgbagraph.hh index e5cce86c4..79681ea59 100644 --- a/src/tgba/tgbagraph.hh +++ b/src/tgba/tgbagraph.hh @@ -360,9 +360,12 @@ namespace spot return neg_acceptance_conditions_; } - virtual bdd compute_support_conditions(const state*) const + virtual bdd compute_support_conditions(const state* s) const { - return bddtrue; + bdd sum = bddfalse; + for (auto& t: out(state_number(s))) + sum |= t.cond; + return sum; } /// Iterate over all transitions, and merge those with compatible diff --git a/src/tgbaalgos/ltl2tgba_fm.cc b/src/tgbaalgos/ltl2tgba_fm.cc index d30463b5a..20e651e82 100644 --- a/src/tgbaalgos/ltl2tgba_fm.cc +++ b/src/tgbaalgos/ltl2tgba_fm.cc @@ -36,7 +36,9 @@ #include "ltl2tgba_fm.hh" #include "tgba/bddprint.hh" #include "tgbaalgos/scc.hh" +#include "tgba/tgbaexplicit.hh" //#include "tgbaalgos/dotty.hh" +#include "priv/acccompl.hh" namespace spot { @@ -403,33 +405,6 @@ namespace spot return multop::instance(multop::OrRat, v); } - void - conj_bdd_to_acc(tgba_explicit_formula* a, bdd b, - state_explicit_formula::transition* t) - { - assert(b != bddfalse); - while (b != bddtrue) - { - int var = bdd_var(b); - bdd high = bdd_high(b); - if (high == bddfalse) - { - // Simply ignore negated acceptance variables. - b = bdd_low(b); - } - else - { - const formula* ac = var_to_formula(var); - - if (!a->has_acceptance_condition(ac)) - a->declare_acceptance_condition(ac->clone()); - a->add_acceptance_condition(t, ac); - b = high; - } - assert(b != bddfalse); - } - } - const translated& ltl_to_bdd(const formula* f, bool mark_all, bool recurring = false); @@ -2048,7 +2023,7 @@ namespace spot } - tgba_explicit_formula* + tgba_digraph* ltl_to_tgba_fm(const formula* f, bdd_dict* dict, bool exprop, bool symb_merge, bool branching_postponement, bool fair_loop_approx, const atomic_prop_set* unobs, @@ -2128,14 +2103,15 @@ namespace spot bdd all_events = observable_events | unobservable_events; - tgba_explicit_formula* a = new tgba_explicit_formula(dict); + tgba_digraph* a = new tgba_digraph(dict); + auto namer = a->create_namer(); // This is in case the initial state is equivalent to true... if (symb_merge) f2 = fc.canonize(f2); formulae_to_translate.insert(f2); - a->set_init_state(f2); + a->set_init_state(namer->new_state(f2)); while (!formulae_to_translate.empty()) { @@ -2273,7 +2249,8 @@ namespace spot // Check for an arc going to 1 (True). Register it first, that // way it will be explored before others during model checking. - dest_map::const_iterator i = dests.find(constant::true_instance()); + 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 @@ -2296,7 +2273,7 @@ namespace spot // When translating LTL for an event-based logic with // unobservable events, the 1 state should accept all events, // even unobservable events. - if (unobs && now == constant::true_instance()) + if (unobs && now == truef) cond_for_true = all_events; else { @@ -2308,44 +2285,38 @@ namespace spot assert(fair_loop_approx || j->first == bddtrue); cond_for_true = j->second; } - if (!a->has_state(constant::true_instance())) - formulae_to_translate.insert(constant::true_instance()); - state_explicit_formula::transition* t = - a->create_transition(now, constant::true_instance()); - t->condition = cond_for_true; + if (!namer->has_state(truef)) + { + formulae_to_translate.insert(truef); + namer->new_state(truef); + } + namer->new_transition(now, truef, cond_for_true, bddtrue); } // 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 = a->has_state(dest); + bool seen = namer->has_state(dest); - if (dest != constant::true_instance()) + for (auto& j: i->second) { - for (prom_map::const_iterator j = i->second.begin(); - j != i->second.end(); ++j) - { - bdd cond = j->second - cond_for_true; - if (cond == bddfalse) // Skip false transitions. - continue; - state_explicit_formula::transition* t = - a->create_transition(now, dest); - t->condition = cond; - d.conj_bdd_to_acc(a, j->first, t); - reachable = true; - } - } - else - { - // "1" is reachable. + 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, j.first); } + if (reachable && !seen) formulae_to_translate.insert(dest); else @@ -2353,9 +2324,21 @@ namespace spot } } + for (auto n: namer->names()) + n->destroy(); + delete namer; + dict->register_propositions(fc.used_vars(), a); + a->set_acceptance_conditions(d.a_set); // Turn all promises into real acceptance conditions. - a->complement_all_acceptance_conditions(); + acc_compl ac(a->all_acceptance_conditions(), + a->neg_acceptance_conditions()); + + unsigned ns = a->num_states(); + for (unsigned s = 0; s < ns; ++s) + for (auto& t: a->out(s)) + t.acc = ac.reverse_complement(t.acc); + if (!simplifier) // This should not be deleted before we have registered all propositions. diff --git a/src/tgbaalgos/ltl2tgba_fm.hh b/src/tgbaalgos/ltl2tgba_fm.hh index a9af771a6..a3d09d195 100644 --- a/src/tgbaalgos/ltl2tgba_fm.hh +++ b/src/tgbaalgos/ltl2tgba_fm.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2010, 2011, 2012, 2013 Laboratoire de Recherche et +// Copyright (C) 2010, 2011, 2012, 2013, 2014 Laboratoire de Recherche et // Développement de l'Epita (LRDE). // Copyright (C) 2003, 2004, 2005, 2006 Laboratoire d'Informatique de // Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), @@ -24,14 +24,14 @@ # define SPOT_TGBAALGOS_LTL2TGBA_FM_HH #include "ltlast/formula.hh" -#include "tgba/tgbaexplicit.hh" +#include "tgba/tgbagraph.hh" #include "ltlvisit/apcollect.hh" #include "ltlvisit/simplify.hh" namespace spot { /// \ingroup tgba_ltl - /// \brief Build a spot::tgba_explicit* from an LTL formula. + /// \brief Build a spot::tgba_digraph* from an LTL formula. /// /// This is based on the following paper. /** \verbatim @@ -122,7 +122,7 @@ namespace spot \endverbatim */ /// /// \return A spot::tgba_explicit that recognizes the language of \a f. - SPOT_API tgba_explicit_formula* + SPOT_API tgba_digraph* ltl_to_tgba_fm(const ltl::formula* f, bdd_dict* dict, bool exprop = false, bool symb_merge = true, bool branching_postponement = false, diff --git a/src/tgbatest/wdba.test b/src/tgbatest/wdba.test index 36eb034e6..35012f5aa 100755 --- a/src/tgbatest/wdba.test +++ b/src/tgbatest/wdba.test @@ -120,14 +120,14 @@ while read f; do # If the labels of the state have only digits, assume the minimization # worked. - x=`../ltl2tgba -f -Rm "!($f)" | - grep -v -- '->' | - sed -n 's/.*label="\(..*\)".*/\1/p' | - tr -d '0-9\n'` - case $x in - "") echo "wrongly minimized !($f)"; success=false;; - *) echo "OK !($f)";; - esac + ../ltl2tgba -kt -Rm "!($f)" > out1 + ../ltl2tgba -kt -R3 "!($f)" > out2 + if cmp out1 out2; then + echo "OK !($f)"; + else + echo "wrongly minimized !($f)"; + success=false; + fi done < non-obligations.txt $success