Commit 6623af67 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz

twa_graph: fix purge_unreachable_states on alternating automata

The algorithm had two problems: it was removing only useless
destination from universal destination (instead of removing the entire
edge), and it was not properly iterating over the entire reachable
automaton.

* spot/twa/twagraph.cc: Fix it.
* spot/twa/twagraph.hh: Adjust documentation.
* tests/core/alternating.test: Add more tests.
* tests/python/twagraph.py: Adjust.
* NEWS: Mention the bug.
parent 73bb562b
...@@ -12,6 +12,9 @@ New in spot 2.3.2.dev (not yet released) ...@@ -12,6 +12,9 @@ New in spot 2.3.2.dev (not yet released)
the output is "terminal" because dtwa_complement() failed to reset the output is "terminal" because dtwa_complement() failed to reset
that property. that property.
- spot::twa_graph::purge_unreachable_states() was misbehaving on
alternating automata.
New in spot 2.3.2 (2017-03-15) New in spot 2.3.2 (2017-03-15)
Tools: Tools:
......
...@@ -245,6 +245,8 @@ namespace spot ...@@ -245,6 +245,8 @@ namespace spot
std::vector<unsigned> order; std::vector<unsigned> order;
order.reserve(num_states); order.reserve(num_states);
bool purge_unreachable_needed = false;
if (is_existential()) if (is_existential())
{ {
std::vector<std::pair<unsigned, unsigned>> todo; // state, edge std::vector<std::pair<unsigned, unsigned>> todo; // state, edge
...@@ -307,13 +309,16 @@ namespace spot ...@@ -307,13 +309,16 @@ namespace spot
const unsigned*& end = std::get<3>(todo.back()); const unsigned*& end = std::get<3>(todo.back());
if (tid == 0U && begin == end) if (tid == 0U && begin == end)
{ {
unsigned src = std::get<0>(todo.back());
todo.pop_back(); todo.pop_back();
// Last transition from a state?
if ((int)src >= 0 && (todo.empty()
|| src != std::get<0>(todo.back())))
order.emplace_back(src);
if (todo.empty()) if (todo.empty())
break; break;
unsigned src = std::get<0>(todo.back()); else
if ((int)src >= 0) continue;
order.emplace_back(src);
continue;
} }
unsigned dst = *begin++; unsigned dst = *begin++;
if (begin == end) if (begin == end)
...@@ -338,53 +343,76 @@ namespace spot ...@@ -338,53 +343,76 @@ namespace spot
} }
} }
// Process states in topological order // At this point, all reachable states with successors are marked
for (auto s: order) // as useful.
for (;;)
{ {
auto t = g_.out_iteraser(s); bool univ_edge_erased = false;
bool useless = true; // Process states in topological order to mark those without
while (t) // successors as useless.
for (auto s: order)
{ {
bool usefuldst = false; auto t = g_.out_iteraser(s);
for (unsigned d: univ_dests(t->dst)) bool useless = true;
if (useful[d]) while (t)
{
usefuldst = true;
break;
}
// Erase any edge to a useless state.
if (!usefuldst)
{ {
t.erase(); // An edge is useful if all its
continue; // destinations are useful.
bool usefuledge = true;
for (unsigned d: univ_dests(t->dst))
if (!useful[d])
{
usefuledge = false;
break;
}
// Erase any useless edge
if (!usefuledge)
{
if (is_univ_dest(t->dst))
univ_edge_erased = true;
t.erase();
continue;
}
// if we have a edge to a useful state, then the
// state is useful.
useless = false;
++t;
} }
// if we have a edge to a useful state, then the if (useless)
// state is useful. useful[s] = 0;
useless = false;
++t;
} }
if (useless) // If we have erased any universal destination, it is possible
useful[s] = 0; // that we have have created some new dead states, so we
// actually need to redo the whole thing again until there is
// no more universal edge to remove. Also we might have
// created some unreachable states, so we will simply call
// purge_unreachable_states() later to clean this.
if (!univ_edge_erased)
break;
else
purge_unreachable_needed = true;
} }
// Make sure at least one initial destination is useful (even if // Is the initial state actually useful? If not, make this an
// it has been marked as useless by the previous loop because it // empty automaton by resetting the graph.
// has no successor). bool usefulinit = true;
bool usefulinit = false;
for (unsigned d: univ_dests(init_number_)) for (unsigned d: univ_dests(init_number_))
if (useful[d]) if (!useful[d])
{ {
usefulinit = true; usefulinit = false;
break; break;
} }
if (!usefulinit) if (!usefulinit)
for (unsigned d: univ_dests(init_number_)) {
{ g_ = graph_t();
useful[d] = true; init_number_ = new_state();
break; prop_deterministic(true);
} prop_stutter_invariant(true);
prop_weak(true);
return;
}
// Now renumber each used state. // Renumber each used state.
unsigned current = 0; unsigned current = 0;
for (unsigned s = 0; s < num_states; ++s) for (unsigned s = 0; s < num_states; ++s)
if (useful[s]) if (useful[s])
...@@ -394,6 +422,9 @@ namespace spot ...@@ -394,6 +422,9 @@ namespace spot
if (current == num_states) if (current == num_states)
return; // No useless state. return; // No useless state.
defrag_states(std::move(useful), current); defrag_states(std::move(useful), current);
if (purge_unreachable_needed)
purge_unreachable_states();
} }
void twa_graph::defrag_states(std::vector<unsigned>&& newst, void twa_graph::defrag_states(std::vector<unsigned>&& newst,
...@@ -401,14 +432,46 @@ namespace spot ...@@ -401,14 +432,46 @@ namespace spot
{ {
if (!is_existential()) if (!is_existential())
{ {
// Running defrag_states() on alternating automata is tricky,
// because we want to
// #1 rename the regular states
// #2 rename the states in universal destinations
// #3 get rid of the unused universal destinations
// #4 merge identical universal destinations
//
// graph::degrag_states() actually does only #1. It it could
// do #2, but that would prevent use from doing #3 and #4. It
// cannot do #3 and #4 because the graph object does not know
// what an initial state is, and our initial state might be
// universal.
//
// As a consequence this code preforms #2, #3, and #4 before
// calling graph::degrag_states() to finish with #1. We clear
// the "dests vector" of the current automaton, recreate all
// the new destination groups using a univ_dest_mapper to
// simplify an unify them, and extend newst with some new
// entries that will point the those new universal destination
// so that graph::defrag_states() does not have to deal with
// universal destination in any way.
auto& g = get_graph(); auto& g = get_graph();
auto& dests = g.dests_vector(); auto& dests = g.dests_vector();
// Clear the destination vector, saving the old one.
std::vector<unsigned> old_dests; std::vector<unsigned> old_dests;
std::swap(dests, old_dests); std::swap(dests, old_dests);
std::vector<unsigned> seen(old_dests.size(), -1U); // dests will be updated as a side effect of declaring new
// destination groups to uniq.
internal::univ_dest_mapper<twa_graph::graph_t> uniq(g); internal::univ_dest_mapper<twa_graph::graph_t> uniq(g);
// The newst entry associated to each of the old destination
// group.
std::vector<unsigned> seen(old_dests.size(), -1U);
// Rename a state if it denotes a universal destination. This
// function has to be applied to the destination of each edge,
// as well as to the initial state. The need to work on the
// initial state is the reason it cannot be implemented in
// graph::defrag_states().
auto fixup = [&](unsigned& in_dst) auto fixup = [&](unsigned& in_dst)
{ {
unsigned dst = in_dst; unsigned dst = in_dst;
...@@ -416,8 +479,9 @@ namespace spot ...@@ -416,8 +479,9 @@ namespace spot
return; return;
dst = ~dst; dst = ~dst;
unsigned& nd = seen[dst]; unsigned& nd = seen[dst];
if (nd == -1U) if (nd == -1U) // An unprocessed destination group
{ {
// store all renamed destination states in tmp
std::vector<unsigned> tmp; std::vector<unsigned> tmp;
auto begin = old_dests.data() + dst + 1; auto begin = old_dests.data() + dst + 1;
auto end = begin + old_dests[dst]; auto end = begin + old_dests[dst];
...@@ -430,10 +494,17 @@ namespace spot ...@@ -430,10 +494,17 @@ namespace spot
} }
if (tmp.empty()) if (tmp.empty())
{ {
// All destinations of this group were marked for
// removal. Mark this universal transition for
// removal as well. Is this really what we expect?
nd = -1U; nd = -1U;
} }
else else
{ {
// register this new destination group, add et two
// newst, and use the index in newst to relabel
// the state so that graph::degrag_states() will
// eventually update it to the correct value.
nd = newst.size(); nd = newst.size();
newst.emplace_back(uniq.new_univ_dests(tmp.begin(), newst.emplace_back(uniq.new_univ_dests(tmp.begin(),
tmp.end())); tmp.end()));
......
...@@ -541,18 +541,26 @@ namespace spot ...@@ -541,18 +541,26 @@ namespace spot
/// states without successors, unreachable states, and states /// states without successors, unreachable states, and states
/// that only have dead successors. /// that only have dead successors.
/// ///
/// This function runs in linear time on non-alternating automata,
/// but its current implementation can be quadratic when removing
/// dead states from alternating automata. (In the latter case, a
/// universal edge has to be remove when any of its destination is
/// dead, but this might cause the other destinations to become
/// dead or unreachable themselves.)
///
/// \see purge_unreachable_states /// \see purge_unreachable_states
void purge_dead_states(); void purge_dead_states();
/// \brief Remove all unreachable states. /// \brief Remove all unreachable states.
/// ///
/// A state is unreachable if it cannot be reached from the initial state. /// A state is unreachable if it cannot be reached from the
/// initial state.
/// ///
/// Use this function if you have declared more states than you /// Use this function if you have declared more states than you
/// actually need in the automaton. /// actually need in the automaton. It runs in linear time.
/// ///
/// purge_dead_states() will remove more states than /// purge_dead_states() will remove more states than
/// purge_unreachable_states(). /// purge_unreachable_states(), but it is more costly.
/// ///
/// \see purge_dead_states /// \see purge_dead_states
void purge_unreachable_states(); void purge_unreachable_states();
......
...@@ -276,6 +276,27 @@ autfilt -q --intersect=ex1 ex3 ...@@ -276,6 +276,27 @@ autfilt -q --intersect=ex1 ex3
cat >ex4<<EOF cat >ex4<<EOF
HOA: v1 HOA: v1
States: 5 States: 5
Start: 0&2
AP: 1 "a"
acc-name: co-Buchi
Acceptance: 1 Fin(0)
properties: univ-branch trans-labels explicit-labels trans-acc
properties: deterministic
--BODY--
State: 0
[0] 0
[!0] 0&2
State: 1
[t] 1&4
State: 2
[!0] 2 {0}
[0] 3
State: 3
[t] 3
State: 4
--END--
HOA: v1
States: 5
Start: 0&2&4 Start: 0&2&4
AP: 1 "a" AP: 1 "a"
acc-name: co-Buchi acc-name: co-Buchi
...@@ -299,6 +320,24 @@ EOF ...@@ -299,6 +320,24 @@ EOF
cat >expect4<<EOF cat >expect4<<EOF
HOA: v1 HOA: v1
States: 3
Start: 0&1
AP: 1 "a"
acc-name: co-Buchi
Acceptance: 1 Fin(0)
properties: univ-branch trans-labels explicit-labels trans-acc complete
properties: deterministic
--BODY--
State: 0
[0] 0
[!0] 0&1
State: 1
[!0] 1 {0}
[0] 2
State: 2
[t] 2
--END--
HOA: v1
States: 4 States: 4
Start: 0&1&3 Start: 0&1&3
AP: 1 "a" AP: 1 "a"
...@@ -319,10 +358,42 @@ State: 3 ...@@ -319,10 +358,42 @@ State: 3
--END-- --END--
EOF EOF
cat >expect4d<<EOF
HOA: v1
States: 3
Start: 0&1
AP: 1 "a"
acc-name: co-Buchi
Acceptance: 1 Fin(0)
properties: univ-branch trans-labels explicit-labels trans-acc complete
properties: deterministic
--BODY--
State: 0
[0] 0
[!0] 0&1
State: 1
[!0] 1 {0}
[0] 2
State: 2
[t] 2
--END--
HOA: v1
States: 1
Start: 0
AP: 1 "a"
acc-name: co-Buchi
Acceptance: 1 Fin(0)
properties: trans-labels explicit-labels state-acc deterministic
properties: stutter-invariant weak
--BODY--
State: 0
--END--
EOF
run 0 autfilt --remove-unreachable-states ex4 > out4 run 0 autfilt --remove-unreachable-states ex4 > out4
diff expect4 out4 diff expect4 out4
run 0 autfilt --remove-dead-states ex4 > out4 run 0 autfilt --remove-dead-states ex4 > out4
diff ex2 out4 diff expect4d out4
cat >ex5<<EOF cat >ex5<<EOF
...@@ -336,6 +407,33 @@ Acceptance: 1 Fin(0) ...@@ -336,6 +407,33 @@ Acceptance: 1 Fin(0)
State: 0 State: 0
State: 1 State: 1
--END-- --END--
HOA: v1
States: 3
Start: 0
AP: 1 "a"
Acceptance: 0 t
--BODY--
State: 0
[0] 1&2
[!0] 1
State: 1
[!0] 1
State: 2
--END--
HOA: v1
States: 4
Start: 0&1
AP: 1 "a"
Acceptance: 0 t
--BODY--
State: 0
[0] 1&2
State: 1
[!0] 1&0&3
State: 2
State: 3
[t] 3
--END--
EOF EOF
run 0 autfilt --remove-dead-states ex5 > out5 run 0 autfilt --remove-dead-states ex5 > out5
...@@ -347,6 +445,31 @@ AP: 1 "a" ...@@ -347,6 +445,31 @@ AP: 1 "a"
acc-name: co-Buchi acc-name: co-Buchi
Acceptance: 1 Fin(0) Acceptance: 1 Fin(0)
properties: trans-labels explicit-labels state-acc deterministic properties: trans-labels explicit-labels state-acc deterministic
properties: stutter-invariant weak
--BODY--
State: 0
--END--
HOA: v1
States: 2
Start: 0
AP: 1 "a"
acc-name: all
Acceptance: 0 t
properties: trans-labels explicit-labels state-acc deterministic
--BODY--
State: 0
[!0] 1
State: 1
[!0] 1
--END--
HOA: v1
States: 1
Start: 0
AP: 1 "a"
acc-name: all
Acceptance: 0 t
properties: trans-labels explicit-labels state-acc deterministic
properties: stutter-invariant weak
--BODY-- --BODY--
State: 0 State: 0
--END-- --END--
......
...@@ -87,4 +87,5 @@ assert aut.edge_data(1).cond == bddtrue ...@@ -87,4 +87,5 @@ assert aut.edge_data(1).cond == bddtrue
aut.release_iter(it) aut.release_iter(it)
aut.purge_dead_states() aut.purge_dead_states()
i = aut.get_init_state()
assert aut.state_is_accepting(i) == False assert aut.state_is_accepting(i) == False
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