diff --git a/spot/twa/acc.cc b/spot/twa/acc.cc index 140dad02f..6d6f3ea51 100644 --- a/spot/twa/acc.cc +++ b/spot/twa/acc.cc @@ -1481,6 +1481,51 @@ namespace spot SPOT_UNREACHABLE(); return {}; } + + static acc_cond::acc_code + force_inf_rec(const acc_cond::acc_word* pos, acc_cond::mark_t rem) + { + auto start = pos - pos->sub.size; + switch (pos->sub.op) + { + case acc_cond::acc_op::And: + { + --pos; + auto res = acc_cond::acc_code::t(); + do + { + auto tmp = force_inf_rec(pos, rem) & std::move(res); + std::swap(tmp, res); + pos -= pos->sub.size + 1; + } + while (pos > start); + return res; + } + case acc_cond::acc_op::Or: + { + --pos; + auto res = acc_cond::acc_code::f(); + do + { + auto tmp = force_inf_rec(pos, rem) | std::move(res); + std::swap(tmp, res); + pos -= pos->sub.size + 1; + } + while (pos > start); + return res; + } + case acc_cond::acc_op::Fin: + return acc_cond::acc_code::fin(pos[-1].mark - rem); + case acc_cond::acc_op::Inf: + return acc_cond::acc_code::inf(pos[-1].mark); + case acc_cond::acc_op::FinNeg: + case acc_cond::acc_op::InfNeg: + SPOT_UNREACHABLE(); + return {}; + } + SPOT_UNREACHABLE(); + return {}; + } } acc_cond::acc_code @@ -1499,6 +1544,14 @@ namespace spot return strip_rec(&back(), rem, missing, false); } + acc_cond::acc_code + acc_cond::acc_code::force_inf(mark_t rem) const + { + if (is_t() || is_f()) + return *this; + return force_inf_rec(&back(), rem); + } + acc_cond::mark_t acc_cond::acc_code::used_sets() const { diff --git a/spot/twa/acc.hh b/spot/twa/acc.hh index 5820ee138..9b1b6e20a 100644 --- a/spot/twa/acc.hh +++ b/spot/twa/acc.hh @@ -921,6 +921,8 @@ namespace spot acc_code remove(acc_cond::mark_t rem, bool missing) const; // Same as remove, but also shift numbers acc_code strip(acc_cond::mark_t rem, bool missing) const; + // for all x in m, this replaces Fin(x) by false. + acc_code force_inf(mark_t m) const; // Return the set of sets appearing in the condition. acc_cond::mark_t used_sets() const; @@ -1388,6 +1390,12 @@ namespace spot { num_sets() - (all_sets() & rem).count(), code_.strip(rem, missing) }; } + // For all x in m, this replaces Fin(x) by false. + acc_cond force_inf(mark_t m) const + { + return {num_sets(), code_.force_inf(m)}; + } + // Restrict an acceptance condition to a subset of set numbers // that are occurring at some point. acc_cond restrict_to(mark_t rem) const diff --git a/spot/twaalgos/genem.cc b/spot/twaalgos/genem.cc index 109c5b700..9fb382f98 100644 --- a/spot/twaalgos/genem.cc +++ b/spot/twaalgos/genem.cc @@ -175,7 +175,7 @@ namespace spot )) return false; // Try to accept when Fin(fo) == false - tmp.set(acc.remove({(unsigned) fo}, false)); + tmp.set(acc.force_inf({(unsigned) fo})); return generic_emptiness_check_for_scc_nocopy (si, scc, tocut); return true; diff --git a/tests/python/genem.py b/tests/python/genem.py index 0b67665dd..8eb6d96d5 100644 --- a/tests/python/genem.py +++ b/tests/python/genem.py @@ -106,6 +106,30 @@ HOA: v1 States: 2 Acceptance: 6 (Fin(0)|Fin(1))&(Fin(2)|Fin(3))& (Fin(4)|Fin(5)) Start: 0 AP: 0 --BODY-- State: 0 [t] 0 {0 2 3} [t] 1 {1 4} State: 1 [t] 0 {2 5} [t] 1 {3 0 1} --END--""") +# From issue #360. +a360 = spot.automaton("""HOA: v1 +States: 2 +Start: 0 +AP: 2 "a" "b" +Acceptance: 8 Fin(5) & (Inf(4) | (Fin(3) & (Inf(2) | (Fin(1) & Inf(0))))) & + (Inf(6) | Inf(7)) & (Fin(6)|Fin(7)) +properties: trans-labels explicit-labels trans-acc complete +properties: deterministic +--BODY-- +State: 0 +[0&1] 0 {4 6 7} +[0&!1] 1 {0 6} +[!0&1] 0 {3 7} +[!0&!1] 0 {0} +State: 1 +[0&1] 0 {4 6 7} +[0&!1] 1 {3 6} +[!0&1] 0 {4 7} +[!0&!1] 1 {0} +--END--""") + + + def generic_emptiness2_rec(aut): spot.cleanup_acceptance_here(aut, False) @@ -143,7 +167,7 @@ def generic_emptiness2_rec(aut): if not generic_emptiness2(part): return False whole = si.split_on_sets(scc, [])[0] - whole.set_acceptance(acc.remove([fo], False)) + whole.set_acceptance(acc.force_inf([fo])) if not generic_emptiness2(whole): return False return True @@ -166,4 +190,4 @@ def run_bench(automata): print(res) assert res in ('TTT', 'FFF') -run_bench([a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a11]) +run_bench([a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a11, a360])