alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

streett_to_generalize_buchi: fix handling of SCCs without Fin

Browse source 
The generalization to Streett-like of 7b5b8f34 was incomplete for this
case.  Thanks to František Blahoudek for reporting the bug.
Fixes #279.

* spot/twaalgos/totgba.cc (streett_to_generalized_buchi): Here.
* tests/core/remfin.test: Add more tests.
This commit is contained in:
Alexandre Duret-Lutz 2017-09-01 20:22:21 +02:00
parent 7b9cedc697
commit f7ba490898
2 changed files with 82 additions and 26 deletions
Download patch file Download diff file Expand all files Collapse all files

37
spot/twaalgos/totgba.cc
View file

@ -130,6 +130,7 @@ namespace spot
acc_cond::mark_t fin;
std::tie(inf, fin) = in->get_acceptance().used_inf_fin_sets();
unsigned p = inf.count();
acc_cond::mark_t fin_not_inf = fin - inf;
if (!p)
return remove_fin(in);
@ -150,7 +151,8 @@ namespace spot
// Compute the acceptance sets present in each SCC
unsigned nscc = si.scc_count();
std::vector<std::tuple<acc_cond::mark_t, acc_cond::mark_t, bool>> sccfi;
std::vector<std::tuple<acc_cond::mark_t, acc_cond::mark_t,
bool, bool>> sccfi;
sccfi.reserve(nscc);
for (unsigned s = 0; s < nscc; ++s)
{
@ -160,21 +162,21 @@ namespace spot
acc_cond::mark_t fin_wo_inf = 0U;
for (unsigned mark: acc_fin.sets())
if (!fin_to_infpairs[mark] || (fin_to_infpairs[mark] - acc_inf))
fin_wo_inf |= {mark};
fin_wo_inf.set(mark);
acc_cond::mark_t inf_wo_fin = 0U;
for (unsigned mark: acc_inf.sets())
if (!inf_to_finpairs[mark] || (inf_to_finpairs[mark] - acc_fin))
inf_wo_fin |= {mark};
inf_wo_fin.set(mark);
sccfi.emplace_back(fin_wo_inf, inf_wo_fin, acc_fin == 0U);
sccfi.emplace_back(fin_wo_inf, inf_wo_fin,
acc_fin == 0U, acc_inf == 0U);
}
auto out = make_twa_graph(in->get_dict());
out->copy_ap_of(in);
out->prop_copy(in, {false, false, false, false, false, true});
out->set_generalized_buchi(p);
acc_cond::mark_t outall = out->acc().all_sets();
// Map st2gba pairs to the state numbers used in out.
typedef std::unordered_map<st2gba_state, unsigned,
@ -207,7 +209,9 @@ namespace spot
acc_cond::mark_t scc_fin_wo_inf;
acc_cond::mark_t scc_inf_wo_fin;
bool no_fin;
std::tie(scc_fin_wo_inf, scc_inf_wo_fin, no_fin) = sccfi[scc_src];
bool no_inf;
std::tie(scc_fin_wo_inf, scc_inf_wo_fin, no_fin, no_inf)
= sccfi[scc_src];
for (auto& t: in->out(s.s))
{
@ -215,7 +219,6 @@ namespace spot
acc_cond::mark_t acc = 0U;
bool maybe_acc = maybe_acc_scc && (scc_src == si.scc_of(t.dst));
if (pend != orig_copy)
{
if (!maybe_acc)
@ -232,7 +235,7 @@ namespace spot
// Label this transition with all non-pending
// inf sets. The strip will shift everything
// to the correct numbers in the targets.
acc = (inf - pend).strip(fin - inf) & outall;
acc = (inf - pend).strip(fin - inf);
// Adjust the pending sets to what will be necessary
// required on the destination state.
if (sbacc)
@ -249,9 +252,12 @@ namespace spot
}
else if (no_fin && maybe_acc)
{
assert(maybe_acc);
acc = outall;
// If the acceptance is (Fin(0) | Inf(1)) & Inf(2)
// but we do not see any Fin set in this SCC, an
// mark {2} should become {1,2} before striping.
acc = (t.acc | (inf - scc_inf_wo_fin)).strip(fin_not_inf);
}
assert((acc & out->acc().all_sets()) == acc);
st2gba_state d(t.dst, pend);
// Have we already seen this destination?
@ -302,17 +308,6 @@ namespace spot
}
}
}
// for (auto s: bs2num)
// {
// std::cerr << s.second << " ("
// << s.first.s << ", ";
// if (s.first.pend == orig_copy)
// std::cerr << "-)\n";
// else
// std::cerr << s.first.pend << ")\n";
// }
return out;
}

71
tests/core/remfin.test
View file

@ -264,6 +264,12 @@ trans-acc --BODY-- State: 0 [!0&1] 5 [!0&1] 7 State: 1 [0&!1] 2 {2}
[!0&1] 4 State: 7 [0&!1] 8 {3} [!0&!1] 7 {2} [0&!1] 3 {2} [!0&1] 5 {1}
State: 8 [!0&1] 8 {2} [!0&!1] 3 {1} [!0&1] 4 State: 9 [0&!1] 6 {0 3}
[!0&1] 2 --END--
/* Exposed the bug from #279 */
HOA: v1 States: 3 Start: 0 AP: 2 "b" "c" Acceptance: 3 Fin(0) &
(Inf(1)&Inf(2)) properties: trans-labels explicit-labels trans-acc
complete --BODY-- State: 0 [!0] 0 {1 2} [0] 0 {0 1 2} [0&!1] 1 [0&1] 2
State: 1 [!0 | !1] 1 {1 2} [0&1] 2 {1} State: 2 [!1] 1 {1 2} [1] 2 {1}
--END--
EOF
acctwelve='Inf(0)&Inf(1)&Inf(2)&Inf(3)&Inf(4)&Inf(5)'
@ -814,6 +820,30 @@ State: 20 {0}
[0&1] 16
[!0&1] 20
--END--
HOA: v1
States: 4
Start: 0
AP: 2 "b" "c"
acc-name: generalized-Buchi 2
Acceptance: 2 Inf(0)&Inf(1)
properties: trans-labels explicit-labels trans-acc
--BODY--
State: 0
[!0] 0
[!0] 1
[0] 0
[0] 1
[0&!1] 2
[0&1] 3
State: 1
[!0] 1 {0 1}
State: 2
[!0 | !1] 2 {0 1}
[0&1] 3 {0}
State: 3
[!1] 2 {0 1}
[1] 3 {0}
--END--
EOF
cat >expected-tgba <<EOF
@ -1358,6 +1388,28 @@ State: 20
[0&1] 16 {0}
[!0&1] 20 {0}
--END--
HOA: v1
States: 4
Start: 0
AP: 2 "b" "c"
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels trans-acc
--BODY--
State: 0
[t] 0
[t] 1
[0&!1] 2
[0&1] 3
State: 1
[!0] 1 {0}
State: 2
[!0 | !1] 2 {0}
[0&1] 3
State: 3
[!1] 2 {0}
[1] 3
--END--
EOF
run 0 $autfilt -H --remove-fin test1 > output
@ -1368,9 +1420,18 @@ run 0 $autfilt -H --tgba test1 > output
cat output
diff -u output expected-tgba
# make sure the above expected automata are correct
autcross --language-preserved 'autfilt --remove-fin' 'autfilt --tgba' -Ftest1
# try 10 small random automata just in case
randaut -A'random 6' -Q10 -n10 3 |
autcross --verbose --language-preserved 'autfilt --remove-fin' 'autfilt --tgba'
# Add 10 small random automata for the next case
randaut -A'random 6' -Q10 -n10 3 -Hl >> test1
# make sure the above expected automata are correct
autcross --verbose --language-preserved -Ftest1 \
'autfilt --remove-fin' 'autfilt --tgba'
# do it again, but make sure autfilt uses streett_to_generalized_buchi
# whenever buchi, and that autcross does not. This helps findings bug
# in streett_to_generalized_buchi().
SPOT_STREETT_CONV_MIN=0 \
autcross --language-preserved -Ftest1 \
'SPOT_STREETT_CONV_MIN=1 autfilt --remove-fin %H>%O' \
'SPOT_STREETT_CONV_MIN=1 autfilt --tgba %H>%O'