Commit 965ae855 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

is_unambiguous: fix false negatives again

Reported by Simon Jantsch and David Müller.

* spot/twaalgos/isunamb.cc (is_unambiguous): Rewrite wihtout assuming
that the product of two accepting SCCs is accepting,  Also use
the result of is_accepting_scc()/is_rejectng_scc() when available.
* spot/twaalgos/sccinfo.cc, spot/twaalgos/sccinfo.hh: Make it
possible to check the acceptance of a unique SCC.
* tests/core/unambig.test: Add more test cases.
parent 978cebe6
Pipeline #1348 passed with stage
in 198 minutes and 28 seconds
......@@ -79,36 +79,48 @@ namespace spot
assert(sprod);
// What follow is a way to compute whether an SCC is useless in
// prod, without having to call
// scc_map::determine_unknown_acceptance() on scc_map(prod),
// because prod has potentially a large acceptance condition.
//
// We know that an SCC of the product is accepting iff it is the
// combination of two accepting SCCs of the original automaton.
//
// So we can just compute the acceptance of each SCC this way, and
// derive the usefulness from that.
// prod, avoiding scc_info::determine_unknown_acceptance() on the
// product, because prod may have a large acceptance condition.
scc_info sccmap_prod(prod);
unsigned psc = sccmap_prod.scc_count();
std::vector<bool> useful(psc);
for (unsigned n = 0; n < psc; ++n)
{
unsigned one_state = sccmap_prod.states_of(n).front();
bool accepting =
v[(*sprod)[one_state].first] && v[(*sprod)[one_state].second];
if (accepting && !sccmap_prod.is_trivial(n))
// If scc_info could determinate acceptance easily, use it.
// An accepting SCC is useful.
bool uf = sccmap_prod.is_accepting_scc(n);
// If any of the successor is useful, this SCC is useful as
// well regardless of its acceptance.
if (!uf)
for (unsigned j: sccmap_prod.succ(n))
if (useful[j])
{
uf = true;
break;
}
if (uf)
{
useful[n] = true;
continue;
}
bool uf = false;
for (unsigned j: sccmap_prod.succ(n))
if (useful[j])
{
uf = true;
break;
}
useful[n] = uf;
if (!sccmap_prod.is_rejecting_scc(n))
{
// This SCC has no useful successors, but we still do not
// known if it is accepting.
//
// A necessary condition for the SCC to be accepting is that
// its it the combination of two accepting SCCs. So let's
// test that first.
unsigned one_state = sccmap_prod.states_of(n).front();
bool accepting =
v[(*sprod)[one_state].first] && v[(*sprod)[one_state].second];
if (!accepting)
continue;
// We can't avoid it any more, we have to check the
// acceptance if the SCC.
std::vector<bool> k;
useful[n] = !sccmap_prod.check_scc_emptiness(n, &k);
}
}
// Now we just have to count the number of states && edges that
......
......@@ -421,6 +421,20 @@ namespace spot
return support;
}
bool scc_info::check_scc_emptiness(unsigned n, std::vector<bool>* k)
{
if (SPOT_UNLIKELY(!aut_->is_existential()))
throw std::runtime_error("scc_info::check_scc_emptiness() "
"does not support alternating automata");
if (SPOT_UNLIKELY(!(options_ & scc_info_options::TRACK_STATES)))
report_need_track_states();
k->assign(aut_->num_states(), false);
auto& node = node_[n];
for (auto i: node.states_)
(*k)[i] = true;
return mask_keep_accessible_states(aut_, *k, node.one_state_)->is_empty();
}
void scc_info::determine_unknown_acceptance()
{
std::vector<bool> k;
......@@ -436,15 +450,8 @@ namespace spot
throw std::runtime_error(
"scc_info::determine_unknown_acceptance() "
"does not support alternating automata");
if (SPOT_UNLIKELY(!(options_ & scc_info_options::TRACK_STATES)))
report_need_track_states();
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.one_state_)
->is_empty())
if (check_scc_emptiness(s, &k))
node.rejecting_ = true;
else
node.accepting_ = true;
......
......@@ -583,10 +583,20 @@ namespace spot
return node(scc).is_rejecting();
}
// Study the SCC that are currently reported neither as accepting
// nor rejecting because of the presence of Fin sets
/// \brief Study the SCCs that are currently reported neither as
/// accepting nor as rejecting because of the presence of Fin sets
///
/// This simply calls check_scc_emptiness() on undeterminate SCCs.
void determine_unknown_acceptance();
/// \brief Recompute whether an SCC is accepting or not.
///
/// This is an internal function of
/// determine_unknown_acceptance(). The Boolean vector k will be
/// used by the method to mark the state that belong to the SCC.
/// It can be shared between multiple calls.
bool check_scc_emptiness(unsigned n, std::vector<bool>* k);
bool is_useful_scc(unsigned scc) const
{
if (SPOT_UNLIKELY(!!(options_ & scc_info_options::STOP_ON_ACC)))
......
......@@ -285,6 +285,7 @@ EOF
run 1 autfilt -q --is-unambiguous smaller.hoa
# These automata come from Simon Jantsch and David Müller.
# They exposed bugs in the optimized version of our unambiguous check.
cat >sjdb.hoa <<EOF
HOA: v1
name: "G(!a | !b) & (Ga | G(b | XGb))"
......@@ -332,6 +333,51 @@ State: 3
State: 4 {0}
[!0&1] 4
--END--
HOA: v1
States: 3
Start: 0
AP: 2 "p0" "p1"
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels trans-acc
--BODY--
State: 0 "((G (! (p0))) R ((! (p1)) | (G (! (p0)))))"
[!0] 1 {0}
[0&!1] 0 {0}
[!0&!1] 2
State: 1 "(G (! (p0)))"
[!0] 1 {0}
State: 2 "((G (! (p0))) R ((! (p1)) | (G (! (p0))))) & (F (p0))"
[0&!1] 0 {0}
[!0&!1] 2
--END--
EOF
test 2 = `autfilt -c --is-unambiguous sjdb.hoa`
test 3 = `autfilt -c --is-unambiguous sjdb.hoa`
# This automaton requires emptiness of SCC with Fin-acceptance.
cat >ambig.hoa<<EOF
HOA: v1
States: 5
Start: 4
AP: 2 "p0" "p1"
Acceptance: 4 Fin(0) & Fin(1)
--BODY--
State: 0
[0] 0 {0}
[!0] 1
State: 1
[1] 1 {1}
[!1] 0
State: 2
[0] 2 {0}
[!0] 3
State: 3
[1] 3 {1}
[!1] 2
State: 4
[0] 0
[0] 2
--END--
EOF
test 0 = `autfilt -c --is-unambiguous ambig.hoa`
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