Commit 2697fcdd authored by Maximilien Colange's avatar Maximilien Colange
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 d6ae7af5
......@@ -70,6 +70,11 @@ New in spot 2.4.0.dev (not yet released)
will work either on f or its negation.
(see https://spot.lrde.epita.fr/hierarchy.html for details).
Bugs fixed:
- spot::scc_info::determine_unknown_acceptance() incorrectly
considered some rejecting SCC as accepting.
Deprecation notices:
(These functions still work but compilers emit warnings.)
......
......@@ -368,26 +368,32 @@ namespace spot
void scc_info::determine_unknown_acceptance()
{
std::vector<bool> k;
unsigned n = scc_count();
unsigned s = scc_count();
bool changed = false;
for (unsigned s = 0; s < n; ++s)
if (!is_rejecting_scc(s) && !is_accepting_scc(s))
{
if (!aut_->is_existential())
throw std::runtime_error("scc_info::determine_unknown_acceptance() "
"does not support alternating automata");
auto& node = node_[s];
if (k.empty())
k.resize(aut_->num_states());
for (auto i: node.states_)
k[i] = true;
if (mask_keep_accessible_states(aut_, k, node.states_.front())
->is_empty())
node.rejecting_ = true;
else
node.accepting_ = true;
changed = true;
}
// iterate over SCCs in topological order
do
{
--s;
if (!is_rejecting_scc(s) && !is_accepting_scc(s))
{
if (!aut_->is_existential())
throw std::runtime_error(
"scc_info::determine_unknown_acceptance() "
"does not support alternating automata");
auto& node = node_[s];
if (k.empty())
k.resize(aut_->num_states());
for (auto i: node.states_)
k[i] = true;
if (mask_keep_accessible_states(aut_, k, node.states_.front())
->is_empty())
node.rejecting_ = true;
else
node.accepting_ = true;
changed = true;
}
}
while (s);
if (changed)
determine_usefulness();
}
......
......@@ -246,19 +246,21 @@ namespace spot
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
/// false if an SCC interesects a mix of Fin and Inf sets.
/// Call determine_unknown_acceptance() to decide.
bool is_accepting() const
{
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
/// false if an SCC interesects a mix of Fin and Inf sets.
/// Call determine_unknown_acceptance() to decide.
bool is_rejecting() const
{
return rejecting_;
......@@ -295,9 +297,14 @@ namespace spot
///
/// This takes twa_graph as input and compute its SCCs. This
/// 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.
///
/// 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
/// in this case, universal transitions are handled like existential
/// transitions. It still make sense to check which states belong
......
......@@ -52,8 +52,6 @@ l3 = si.states_of(3)
l = sorted(list(l0) + list(l1) + list(l2) + list(l3))
assert l == [0, 1, 2, 3, 4]
i = si.initial()
todo = {i}
seen = {i}
......@@ -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)]
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