Commit 32087f29 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

streett_to_generalized_buchi: fix incorrect algorithm

Fixes #284, reported by Juraj Major.

* spot/twaalgos/totgba.cc: Fix the algorithm.
* spot/twa/acc.hh: More doc for future generations.
* tests/core/scc.test: More test cases.
* NEWS: Mention the issues.
parent cfa80ed8
...@@ -5,6 +5,13 @@ New in spot 2.4.0.dev (not yet released) ...@@ -5,6 +5,13 @@ New in spot 2.4.0.dev (not yet released)
- spot::scc_info::determine_unknown_acceptance() incorrectly - spot::scc_info::determine_unknown_acceptance() incorrectly
considered some rejecting SCC as accepting. considered some rejecting SCC as accepting.
- spot::streett_to_generalized_buchi() could generate automata with
empty language if some Fin set did not intersect all accepting
SCCs. As a consequence, some Streett-like automata were
considered empty even though they were not. Also, the same
function could crash on input that had a Streett-like acceptance
not using all declared sets.
- 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
......
...@@ -1046,6 +1046,15 @@ namespace spot ...@@ -1046,6 +1046,15 @@ namespace spot
// Returns a number of pairs (>=0) if Streett, or -1 else. // Returns a number of pairs (>=0) if Streett, or -1 else.
int is_streett() const; int is_streett() const;
/// \brief Rabin/streett pairs used by is_rabin_like and is_streett_like.
///
/// These pairs hold two marks which can each contain one or no set.
///
/// For instance is_streett_like() rewrites Inf(0)&(Inf(2)|Fin(1))&Fin(3)
/// as three pairs: [(fin={},inf={0}),(fin={1},inf={2}),(fin={3},inf={})].
///
/// Empty marks should be interpreted in a way that makes them
/// false in Streett, and true in Rabin.
struct SPOT_API rs_pair struct SPOT_API rs_pair
{ {
rs_pair() = default; rs_pair() = default;
......
...@@ -130,7 +130,9 @@ namespace spot ...@@ -130,7 +130,9 @@ namespace spot
acc_cond::mark_t fin; acc_cond::mark_t fin;
std::tie(inf, fin) = in->get_acceptance().used_inf_fin_sets(); std::tie(inf, fin) = in->get_acceptance().used_inf_fin_sets();
unsigned p = inf.count(); unsigned p = inf.count();
acc_cond::mark_t fin_not_inf = fin - inf; // At some point we will remove anything that is not used as Inf.
acc_cond::mark_t to_strip = in->acc().all_sets() - inf;
acc_cond::mark_t inf_alone = 0U;
if (!p) if (!p)
return remove_fin(in); return remove_fin(in);
...@@ -140,8 +142,11 @@ namespace spot ...@@ -140,8 +142,11 @@ namespace spot
std::vector<acc_cond::mark_t> inf_to_finpairs(numsets, 0U); std::vector<acc_cond::mark_t> inf_to_finpairs(numsets, 0U);
for (auto pair: pairs) for (auto pair: pairs)
{ {
for (unsigned mark: pair.fin.sets()) if (pair.fin)
fin_to_infpairs[mark] |= pair.inf; for (unsigned mark: pair.fin.sets())
fin_to_infpairs[mark] |= pair.inf;
else
inf_alone |= pair.inf;
for (unsigned mark: pair.inf.sets()) for (unsigned mark: pair.inf.sets())
inf_to_finpairs[mark] |= pair.fin; inf_to_finpairs[mark] |= pair.fin;
...@@ -231,11 +236,14 @@ namespace spot ...@@ -231,11 +236,14 @@ namespace spot
for (unsigned mark: (t.acc & fin).sets()) for (unsigned mark: (t.acc & fin).sets())
pend |= fin_to_infpairs[mark]; pend |= fin_to_infpairs[mark];
// If we see some Inf set immediately, they are not
// pending anymore.
pend -= t.acc & inf; pend -= t.acc & inf;
// Label this transition with all non-pending // Label this transition with all non-pending
// inf sets. The strip will shift everything // inf sets. The strip will shift everything
// to the correct numbers in the targets. // to the correct numbers in the targets.
acc = (inf - pend).strip(fin - inf); acc = (inf - pend).strip(to_strip);
// Adjust the pending sets to what will be necessary // Adjust the pending sets to what will be necessary
// required on the destination state. // required on the destination state.
if (sbacc) if (sbacc)
...@@ -248,14 +256,14 @@ namespace spot ...@@ -248,14 +256,14 @@ namespace spot
pend -= a & inf; pend -= a & inf;
} }
pend |= scc_inf_wo_fin; pend |= inf_alone;
} }
else if (no_fin && maybe_acc) else if (no_fin && maybe_acc)
{ {
// If the acceptance is (Fin(0) | Inf(1)) & Inf(2) // If the acceptance is (Fin(0) | Inf(1)) & Inf(2)
// but we do not see any Fin set in this SCC, an // but we do not see any Fin set in this SCC, a
// mark {2} should become {1,2} before striping. // mark {2} should become {1,2} before striping.
acc = (t.acc | (inf - scc_inf_wo_fin)).strip(fin_not_inf); acc = (t.acc | (inf - scc_inf_wo_fin)).strip(to_strip);
} }
assert((acc & out->acc().all_sets()) == acc); assert((acc & out->acc().all_sets()) == acc);
...@@ -291,7 +299,7 @@ namespace spot ...@@ -291,7 +299,7 @@ namespace spot
stpend -= a & inf; stpend -= a & inf;
} }
st2gba_state d(t.dst, stpend | scc_inf_wo_fin); st2gba_state d(t.dst, stpend | inf_alone);
// Have we already seen this destination? // Have we already seen this destination?
unsigned dest; unsigned dest;
auto dres = bs2num.emplace(d, 0); auto dres = bs2num.emplace(d, 0);
......
...@@ -139,3 +139,56 @@ State: 3 {1} ...@@ -139,3 +139,56 @@ State: 3 {1}
--END-- --END--
EOF EOF
test 2 = `autfilt --stats=%[a]c in.hoa` test 2 = `autfilt --stats=%[a]c in.hoa`
# From issue #284, reported by Juraj Major.
cat >in.hoa <<EOF
HOA: v1
States: 4
Start: 0
AP: 1 "a"
Acceptance: 8 Fin(5) & Fin(3) & (Inf(6) | Fin(7)) &
(Inf(2) | Fin(1)) & (Inf(4) | Fin(0))
properties: trans-labels explicit-labels trans-acc complete
spot.highlight.edges: 3 5 11 5 14 5
--BODY--
State: 0
[t] 0 {0}
[0] 1 {4}
[!0] 2 {4}
[0] 0 {2 3}
[!0] 0 {1}
State: 1
[!0] 1 {0}
[!0] 3 {4}
[!0] 1 {1}
[0] 1 {4 5}
[0] 1 {2 3 5}
State: 2
[0] 2 {0 6}
[0] 3 {4 6}
[0] 2 {2 3 6}
[!0] 2 {4 7}
State: 3
[0] 3 {4 5 6}
[0] 3 {2 3 5 6}
[!0] 3 {4 7}
--END--
/* this variant also cause some issues while fixing the above */
HOA: v1
States: 1
Start: 0
AP: 1 "a"
Acceptance: 5 Fin(0) & (Inf(1) | Fin(2)) & (Inf(4))
--BODY--
State: 0
[0] 0 {1}
[0] 0 {0 1}
[!0] 0 {4 2}
--END--
EOF
autfilt --stats='%[a]c' in.hoa >out
cat >exp <<EOF
1
1
EOF
diff out exp
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