Commit f45112a2 authored by Maximilien Colange's avatar Maximilien Colange Committed by Alexandre Duret-Lutz
Browse files

Fix a bug in scc_info, and clarify documentation

* spot/twaalgos/sccinfo.hh, spot/twaalgos/sccinfo.cc: Implement it
* tests/python/sccinfo.py: Test it
* NEWS: Document the fix
parent cdfe78f1
New in spot 2.4.0.dev (not yet released) New in spot 2.4.0.dev (not yet released)
Nothing yet.
Bugs fixed: Bugs fixed:
- spot::scc_info::determine_unknown_acceptance() incorrectly
considered some rejecting SCC as accepting.
- The twa_graph::mege_edges() function relied on BDD IDs to sort - The twa_graph::mege_edges() function relied on BDD IDs to sort
edges. This in turn caused some algorithm (like the edges. This in turn caused some algorithm (like the
degeneralization) to produce slighltly different outputs (but degeneralization) to produce slighltly different outputs (but
......
...@@ -368,13 +368,17 @@ namespace spot ...@@ -368,13 +368,17 @@ namespace spot
void scc_info::determine_unknown_acceptance() void scc_info::determine_unknown_acceptance()
{ {
std::vector<bool> k; std::vector<bool> k;
unsigned n = scc_count(); unsigned s = scc_count();
bool changed = false; bool changed = false;
for (unsigned s = 0; s < n; ++s) // iterate over SCCs in topological order
do
{
--s;
if (!is_rejecting_scc(s) && !is_accepting_scc(s)) if (!is_rejecting_scc(s) && !is_accepting_scc(s))
{ {
if (!aut_->is_existential()) if (!aut_->is_existential())
throw std::runtime_error("scc_info::determine_unknown_acceptance() " throw std::runtime_error(
"scc_info::determine_unknown_acceptance() "
"does not support alternating automata"); "does not support alternating automata");
auto& node = node_[s]; auto& node = node_[s];
if (k.empty()) if (k.empty())
...@@ -388,6 +392,8 @@ namespace spot ...@@ -388,6 +392,8 @@ namespace spot
node.accepting_ = true; node.accepting_ = true;
changed = true; changed = true;
} }
}
while (s);
if (changed) if (changed)
determine_usefulness(); determine_usefulness();
} }
......
...@@ -246,19 +246,21 @@ namespace spot ...@@ -246,19 +246,21 @@ namespace spot
return trivial_; return trivial_;
} }
/// \brief True if we are sure that the SCC is accepting /// \brief True if we know that the SCC has an accepting cycle
/// ///
/// Note that both is_accepting() and is_rejecting() may return /// Note that both is_accepting() and is_rejecting() may return
/// false if an SCC interesects a mix of Fin and Inf sets. /// false if an SCC interesects a mix of Fin and Inf sets.
/// Call determine_unknown_acceptance() to decide.
bool is_accepting() const bool is_accepting() const
{ {
return accepting_; return accepting_;
} }
// True if we are sure that the SCC is rejecting /// \brief True if we know that all cycles in the SCC are rejecting
/// ///
/// Note that both is_accepting() and is_rejecting() may return /// Note that both is_accepting() and is_rejecting() may return
/// false if an SCC interesects a mix of Fin and Inf sets. /// false if an SCC interesects a mix of Fin and Inf sets.
/// Call determine_unknown_acceptance() to decide.
bool is_rejecting() const bool is_rejecting() const
{ {
return rejecting_; return rejecting_;
...@@ -295,9 +297,14 @@ namespace spot ...@@ -295,9 +297,14 @@ namespace spot
/// ///
/// This takes twa_graph as input and compute its SCCs. This /// This takes twa_graph as input and compute its SCCs. This
/// class maps all input states to their SCCs, and vice-versa. /// class maps all input states to their SCCs, and vice-versa.
/// It allows iterating over all SCCs of the automaton, and check /// It allows iterating over all SCCs of the automaton, and checks
/// their acceptance or non-acceptance. /// their acceptance or non-acceptance.
/// ///
/// SCC are numbered in reverse topological order, i.e. the SCC of the
/// initial state has the highest number, and if s1 is reachable from
/// s2, then s1 < s2. Many algorithms depend on this property to
/// determine in what order to iterate the SCCs.
///
/// Additionally this class can be used on alternating automata, but /// Additionally this class can be used on alternating automata, but
/// in this case, universal transitions are handled like existential /// in this case, universal transitions are handled like existential
/// transitions. It still make sense to check which states belong /// transitions. It still make sense to check which states belong
......
...@@ -52,8 +52,6 @@ l3 = si.states_of(3) ...@@ -52,8 +52,6 @@ l3 = si.states_of(3)
l = sorted(list(l0) + list(l1) + list(l2) + list(l3)) l = sorted(list(l0) + list(l1) + list(l2) + list(l3))
assert l == [0, 1, 2, 3, 4] assert l == [0, 1, 2, 3, 4]
i = si.initial() i = si.initial()
todo = {i} todo = {i}
seen = {i} seen = {i}
...@@ -77,3 +75,34 @@ assert transi == [(0, 0, 1), (0, 3, 4), (3, 0, 7), ...@@ -77,3 +75,34 @@ assert transi == [(0, 0, 1), (0, 3, 4), (3, 0, 7),
(3, 3, 9), (1, 1, 5), (2, 2, 6), (4, 4, 12)] (3, 3, 9), (1, 1, 5), (2, 2, 6), (4, 4, 12)]
assert not spot.is_weak_automaton(a, si) assert not spot.is_weak_automaton(a, si)
a = spot.automaton("""
HOA: v1
States: 4
Start: 0
AP: 1 "a"
Acceptance: 2 Inf(0)&Fin(1)
--BODY--
State: 0
[t] 0 {1}
[t] 1 {0}
State: 1
[t] 1 {1}
[t] 0 {1}
[t] 2
State: 2
[t] 2 {1}
[t] 3 {0}
State: 3
[t] 3 {1}
[t] 2
--END--
""")
si = spot.scc_info(a)
si.determine_unknown_acceptance()
assert si.scc_count() == 2
assert si.is_accepting_scc(0)
assert not si.is_rejecting_scc(0)
assert si.is_rejecting_scc(1)
assert not si.is_accepting_scc(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