Commit dad17b36 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz

honor ap() when counting transitions

Fixing this bug alone revealed another bug: parsing never claim or LBTT
automata did not register APs.  So this fixes both bugs.

This is the first part of #170.

* spot/twa/twa.hh (register_aps_from_dict): New method.
* spot/parseaut/parseaut.yy: Call it for never claim and LBTT files.
* spot/twaalgos/stats.cc: Simplify using ap_vars().
* tests/core/ltl2tgba.test: Add a test case.
* NEWS: Mention the bugs.
parent 4f913c7f
...@@ -17,6 +17,12 @@ New in spot 2.0.0a (not yet released) ...@@ -17,6 +17,12 @@ New in spot 2.0.0a (not yet released)
* Fix autfilt to apply --simplify-exclusive-ap only after * Fix autfilt to apply --simplify-exclusive-ap only after
the simplifications of (--small/--deterministic) have the simplifications of (--small/--deterministic) have
been performed. 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) New in spot 2.0 (2016-04-11)
......
...@@ -1529,6 +1529,7 @@ never: "never" ...@@ -1529,6 +1529,7 @@ never: "never"
// Pretend that we have declared all states. // Pretend that we have declared all states.
for (auto& p: res.info_states) for (auto& p: res.info_states)
p.declared = true; p.declared = true;
res.h->aut->register_aps_from_dict();
} }
nc-states: nc-states:
...@@ -1750,6 +1751,7 @@ lbtt: lbtt-header lbtt-body ENDAUT ...@@ -1750,6 +1751,7 @@ lbtt: lbtt-header lbtt-body ENDAUT
res.info_states.resize(res.h->aut->num_states()); res.info_states.resize(res.h->aut->num_states());
for (auto& s: res.info_states) for (auto& s: res.info_states)
s.declared = true; s.declared = true;
res.h->aut->register_aps_from_dict();
} }
| lbtt-header-states LBTT_EMPTY | lbtt-header-states LBTT_EMPTY
{ {
......
...@@ -738,6 +738,34 @@ namespace spot ...@@ -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 /// \brief The vector of atomic propositions registered by this
/// automaton. /// automaton.
const std::vector<formula>& ap() const const std::vector<formula>& ap() const
......
...@@ -62,7 +62,7 @@ namespace spot ...@@ -62,7 +62,7 @@ namespace spot
{ {
public: public:
sub_stats_bfs(const const_twa_ptr& a, twa_sub_statistics& s) 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 ...@@ -71,24 +71,7 @@ namespace spot
const twa_succ_iterator* it) override const twa_succ_iterator* it) override
{ {
++s_.edges; ++s_.edges;
bdd cond = it->cond(); 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) while (cond != bddfalse)
{ {
cond -= bdd_satoneset(cond, seen_, bddtrue); cond -= bdd_satoneset(cond, seen_, bddtrue);
......
...@@ -221,3 +221,6 @@ ltlfilt -q -r -f '{c && {b | [*0]}[:+]}' --equivalent-to 'c & b' ...@@ -221,3 +221,6 @@ ltlfilt -q -r -f '{c && {b | [*0]}[:+]}' --equivalent-to 'c & b'
# test unknown dot options # test unknown dot options
ltl2tgba --dot=@ a 2>stderr && exit 1 ltl2tgba --dot=@ a 2>stderr && exit 1
grep 'ltl2tgba: unknown option.*@' stderr 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
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment