diff --git a/NEWS b/NEWS index 212bd4dad..865aa8c6a 100644 --- a/NEWS +++ b/NEWS @@ -17,6 +17,12 @@ New in spot 2.0.0a (not yet released) * Fix autfilt to apply --simplify-exclusive-ap only after the simplifications of (--small/--deterministic) have been performed. + * The automaton parser did not fully register atomic propositions + for automata read from never claim or as LBTT. + * The sub_stats_reachable() function used to count the number + of transitions based on the number of atomic propositions + actually *used* by the automaton instead of using the number + of AP declared. New in spot 2.0 (2016-04-11) diff --git a/spot/parseaut/parseaut.yy b/spot/parseaut/parseaut.yy index 3f35edb44..46be5e95d 100644 --- a/spot/parseaut/parseaut.yy +++ b/spot/parseaut/parseaut.yy @@ -1529,6 +1529,7 @@ never: "never" // Pretend that we have declared all states. for (auto& p: res.info_states) p.declared = true; + res.h->aut->register_aps_from_dict(); } nc-states: @@ -1750,6 +1751,7 @@ lbtt: lbtt-header lbtt-body ENDAUT res.info_states.resize(res.h->aut->num_states()); for (auto& s: res.info_states) s.declared = true; + res.h->aut->register_aps_from_dict(); } | lbtt-header-states LBTT_EMPTY { diff --git a/spot/twa/twa.hh b/spot/twa/twa.hh index 8d7ec3d7a..c213b9266 100644 --- a/spot/twa/twa.hh +++ b/spot/twa/twa.hh @@ -738,6 +738,34 @@ namespace spot } ///@} + + /// \brief Register all atomic propositions that have + /// already be register by the bdd_dict for this automaton. + /// + /// This method may only be called on an automaton with an empty + /// list of AP. It will fetch all atomic proposition that have + /// been set in the bdd_dict for this particular automaton. + /// + /// The typical use-case for this function is when the labels of + /// an automaton are created by functions such as + /// formula_to_bdd(). This is for instance done in the parser + /// for never claims or LBTT. + void register_aps_from_dict() + { + if (!aps_.empty()) + throw std::runtime_error("register_ap_from_dict() may not be" + " called on an automaton that has already" + " registered some AP"); + auto& m = get_dict()->bdd_map; + unsigned s = m.size(); + for (unsigned n = 0; n < s; ++n) + if (m[n].refs.find(this) != m[n].refs.end()) + { + aps_.push_back(m[n].f); + bddaps_ &= bdd_ithvar(n); + } + } + /// \brief The vector of atomic propositions registered by this /// automaton. const std::vector& ap() const diff --git a/spot/twaalgos/stats.cc b/spot/twaalgos/stats.cc index c3a8f14ec..e661e9252 100644 --- a/spot/twaalgos/stats.cc +++ b/spot/twaalgos/stats.cc @@ -62,7 +62,7 @@ namespace spot { public: sub_stats_bfs(const const_twa_ptr& a, twa_sub_statistics& s) - : stats_bfs(a, s), s_(s), seen_(bddtrue) + : stats_bfs(a, s), s_(s), seen_(a->ap_vars()) { } @@ -71,24 +71,7 @@ namespace spot const twa_succ_iterator* it) override { ++s_.edges; - bdd cond = it->cond(); - bdd newvars = bdd_exist(bdd_support(cond), seen_); - if (newvars != bddtrue) - { - seen_ &= newvars; - int count = 0; - while (newvars != bddtrue) - { - ++count; - newvars = bdd_high(newvars); - } - // If we discover one new variable, that means that all - // transitions we counted so far are actually double - // subtransitions. If we have two new variables, they where - // quadruple transitions, etc. - s_.transitions <<= count; - } while (cond != bddfalse) { cond -= bdd_satoneset(cond, seen_, bddtrue); diff --git a/tests/core/ltl2tgba.test b/tests/core/ltl2tgba.test index ec556f23c..c907c15d8 100755 --- a/tests/core/ltl2tgba.test +++ b/tests/core/ltl2tgba.test @@ -221,3 +221,6 @@ ltlfilt -q -r -f '{c && {b | [*0]}[:+]}' --equivalent-to 'c & b' # test unknown dot options ltl2tgba --dot=@ a 2>stderr && exit 1 grep 'ltl2tgba: unknown option.*@' stderr + +# Make sure the count of AP is correct through never claims or LBTT +ltl2tgba -f a -s | autfilt -q --ap=1 --lbtt | autfilt -q --ap=1