diff --git a/spot/twaalgos/totgba.cc b/spot/twaalgos/totgba.cc index 01bbc0c5d..ea8f981ac 100644 --- a/spot/twaalgos/totgba.cc +++ b/spot/twaalgos/totgba.cc @@ -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> sccfi; + std::vector> 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_mapout(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; } diff --git a/tests/core/remfin.test b/tests/core/remfin.test index ac087e2ee..aa6074496 100755 --- a/tests/core/remfin.test +++ b/tests/core/remfin.test @@ -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 < 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'