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

fix tra_to_tba()

Fixes #324, reported by Tobias Meggendorfer and František Blahoudek.

* spot/twa/acc.hh (rs_pairs_view::paired_with): Rename as...
(rs_pairs_view::paired_with_fin):... this and adjust the code.
* spot/twaalgos/remfin.cc: Use paired_with_fin instead of
paired_with, and do it once per pair.
* tests/core/remfin.test: Add a test case.
* NEWS: Mention the issue.
parent 5c390635
......@@ -18,6 +18,13 @@ New in spot 2.5.0.dev (not yet released)
as Fin(0)|(Fin(1)&Inf(2)) instead. Likewise for
is_generalized_streett
- the conversion from Rabin to Büchi was broken on Rabin-like
acceptance condition where one pair used Fin(x) and another pair
used Inf(x) with the same x. Unfortunately, this situation could
also occur as a side effect of simplifying the acceptance
condition (by merging identical set) prior to running the
conversion to Büchi.
New in spot 2.5 (2018-01-20)
Build:
......
......@@ -1397,19 +1397,12 @@ namespace spot
});
}
acc_cond::mark_t paired_with(unsigned mark) const
acc_cond::mark_t paired_with_fin(unsigned mark) const
{
acc_cond::mark_t res = 0U;
for (const auto& p: pairs_)
{
if (visible(p.fin) && visible(p.inf))
{
if (p.fin.has(mark))
res |= p.inf;
if (p.inf.has(mark))
res |= p.fin;
}
}
if (p.fin.has(mark) && visible(p.fin) && visible(p.inf))
res |= p.inf;
return res;
}
......
......@@ -312,7 +312,7 @@ namespace spot
for (const auto& e: si.edges_of(scc))
{
bool acc{e.acc & scc_infs_alone};
bool acc = (e.acc & scc_infs_alone) != 0;
res->new_acc_edge(e.src, e.dst, e.cond, acc);
}
......@@ -320,6 +320,7 @@ namespace spot
for (auto r: scc_pairs.fins().sets())
{
acc_cond::mark_t pairinf = scc_pairs.paired_with_fin(r);
unsigned base = res->new_states(states.size());
for (auto s: states)
state_map[s] = base++;
......@@ -329,9 +330,7 @@ namespace spot
continue;
auto src = state_map[e.src];
auto dst = state_map[e.dst];
bool cacc = fins_alone.has(r)
? true
: ((scc_pairs.paired_with(r) & e.acc) != 0);
bool cacc = fins_alone.has(r) || (pairinf & e.acc) != 0;
res->new_acc_edge(src, dst, e.cond, cacc);
// We need only one non-deterministic jump per
// cycle. As an approximation, we only do
......
......@@ -1504,6 +1504,27 @@ run 0 autfilt -H --tgba test1 > output
cat output
diff -u output expected-tgba
# Issue #324.
cat > 324 <<EOF
HOA: v1
States: 2
Start: 1
AP: 2 "a" "b"
acc-name: Rabin 3
Acceptance: 6 (Fin(0) & Inf(1)) | (Fin(2) & Inf(3)) | (Fin(4) & Inf(5))
properties: trans-labels explicit-labels trans-acc deterministic
--BODY--
State: 0
[!0&!1] 0 {0 4}
[!0&1] 0 {0 3 4}
[0&!1] 0 {2 5}
[0&1] 0 {1 2 5}
State: 1
[0] 0
--END--
EOF
autfilt --remove-fin 324 > out
test 2 = `autfilt -c --reject-word='a;cycle{!a&!b}' 324 out`
# Add 10 small random automata for the next case
randaut -A'random 6' -Q10 -n10 3 -Hl >> test1
......
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