From 82401b3254c4c9fa49d4e60cc7b4c0ff0b156254 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Mon, 2 Dec 2024 23:24:30 +0100 Subject: [PATCH] correct to_finite This fixes issue #596. * spot/twaalgos/remprop.cc: Rewrite main loop. * tests/core/ltlf.test: Add test case. * tests/python/game.py: Remove a test that appears to make incorrect assumptions about to_finite. * NEWS: Mention the bug. --- NEWS | 3 + spot/twaalgos/remprop.cc | 21 +++--- tests/core/ltlf.test | 37 +++++++---- tests/python/game.py | 137 --------------------------------------- 4 files changed, 39 insertions(+), 159 deletions(-) diff --git a/NEWS b/NEWS index 9730a59d5..655914f1d 100644 --- a/NEWS +++ b/NEWS @@ -117,6 +117,9 @@ New in spot 2.12.1.dev (not yet released) status and the AIG circuit; it now does the job silently as requested. + - to_finite() was dealing incorrectly with edges that were + both alive and dead. (Issue #596.) + New in spot 2.12.1 (2024-09-23) Bug fixes: diff --git a/spot/twaalgos/remprop.cc b/spot/twaalgos/remprop.cc index 14570f148..eb7c54dd0 100644 --- a/spot/twaalgos/remprop.cc +++ b/spot/twaalgos/remprop.cc @@ -19,6 +19,7 @@ #include "config.h" #include #include +#include #include #include @@ -180,6 +181,8 @@ namespace spot make_twa_graph(aut, { false, false, true, false, false, false }); + scc_info si(aut, scc_info_options::TRACK_SUCCS); + bdd rem = bddtrue; bdd neg = bddfalse; int v = res->get_dict()-> @@ -194,18 +197,18 @@ namespace spot unsigned ns = res->num_states(); std::vector isacc(ns, false); for (unsigned s = 0; s < ns; ++s) - { - for (auto& e: res->out(s)) - if (bdd_implies(e.cond, neg)) + for (auto& e: res->out(s)) + { + if (!si.is_useful_state(e.dst)) { - isacc[e.src] = true; e.cond = bddfalse; + continue; } - else - { - e.cond = bdd_restrict(e.cond, rem); - } - } + if (bdd_have_common_assignment(e.cond, neg)) + isacc[e.src] = true; + e.cond = bdd_restrict(e.cond, rem); + } + res->set_buchi(); res->prop_state_acc(true); diff --git a/tests/core/ltlf.test b/tests/core/ltlf.test index b8691adc8..77e68d8d8 100755 --- a/tests/core/ltlf.test +++ b/tests/core/ltlf.test @@ -173,51 +173,62 @@ cmp out3 out4 && exit 1 # make sure we did remove something autfilt out3 > out4 diff out4 expected3 -# Issue #526 -ltlfilt -f '(i->XXo)|G(i<->Xo2)' --from-ltlf | ltl2tgba -D |\ +# Issue #526 and Issue #596 +ltlfilt -f '(i->XXo)|G(i<->Xo2)' -f XXXo --from-ltlf | ltl2tgba -D |\ autfilt -C --to-finite > out cat >exp < selfloop - # 2 Prune - acc_state = set() - sp = list(spot.get_state_players(auts)) - for e in auts.edges(): - if e.acc: - acc_state.add(e.src) - for s in acc_state: - e_kill = auts.out_iteraser(s) - while (e_kill): - e_kill.erase() - for s in acc_state: - sprime = auts.new_state() - sp.append(not sp[s]) - auts.new_edge(s, sprime, buddy.bddtrue, [0]) - auts.new_edge(sprime, s, buddy.bddtrue, [0]) - spot.set_state_players(auts, sp) - auts.purge_dead_states() - spot.alternate_players(auts, False, False) - return auts - -def is_input_complete(auts): - sp = spot.get_state_players(auts) - for s in range(auts.num_states()): - if sp[s]: - continue # Player - cumul = buddy.bddfalse - for e in auts.out(s): - cumul |= e.cond - if cumul != buddy.bddtrue: - return False - - return True - -def synt_from_ltlf(f:str, outs): - ff = spot.from_ltlf(f, alive) - aut = ff.translate("buchi", "sbacc") - outbdd = buddy.bddtrue - for out in outs: - outbdd &= buddy.bdd_ithvar(aut.register_ap(out)) - alive_bdd = buddy.bdd_ithvar(aut.register_ap(alive)) - auts = spot.split_2step(aut, outbdd & alive_bdd, False) - auts = spot.to_finite(auts, alive) - spot.alternate_players(auts, False, False) - spot.set_synthesis_outputs(auts, outbdd) - if not is_input_complete(auts): - print("Not synthesizable") - return None - auts = finite_existential(auts) - - return auts - -def synt_ltlf(f:str, outs, res:str = "aut"): - auts = synt_from_ltlf(f, outs) - - succ = spot.solve_parity_game(auts) - if not succ: - if res == "aut": - return False, auts - else: - return False, None - - mealy_cc = spot.solved_game_to_split_mealy(auts) - - if res == "aut": - return True, mealy_cc - elif res == "aig": - return True, spot.mealy_machine_to_aig(mealy_cc, "isop") - else: - raise RuntimeError("Unknown option") - - -sink_player = None - -def negate_ltlf(f:str, outs, opt = "buchi"): - - global sink_player - sink_player = None - - aut = synt_from_ltlf(f, outs) - # Implies input completeness - # We need output completeness - acc = [] - - sp = list(spot.get_state_players(aut)) - - def get_sink(): - global sink_player - if sink_player is None: - sink_player = aut.new_states(2) - aut.new_edge(sink_player, sink_player + 1, buddy.bddtrue, acc) - aut.new_edge(sink_player + 1, sink_player, buddy.bddtrue, acc) - sp.append(False) - sp.append(True) - spot.set_state_players(aut, sp) - return sink_player - - for s in range(aut.num_states()): - if not sp[s]: - continue - rem = buddy.bddtrue - for e in aut.out(s): - rem -= e.cond - if rem != buddy.bddfalse: - aut.new_edge(s, get_sink(), rem) - - # Better to invert colors or condition? - if opt == "buchi": - for e in aut.edges(): - if e.acc: - e.acc = spot.mark_t() - else: - e.acc = spot.mark_t([0]) - elif opt == "cobuchi": - aut.set_co_buchi() - else: - raise RuntimeError("Unknown opt") - return aut - -# Game where the edge_vector is larger -# than the number of transitions -f1 = "((((G (F (idle))) && (G (((idle) && (X ((! (grant_0)) \ - && (! (grant_1))))) -> (X (idle))))) && (G ((X (! (grant_0))) \ - || (X (((! (request_0)) && (! (idle))) U ((! (request_0)) \ - && (idle))))))) -> (((G (((((X (((! (grant_0)) && (true)) \ - || ((true) && (! (grant_1))))) && ((X (grant_0)) -> (request_0))) \ - && ((X (grant_1)) -> (request_1))) && ((request_0) -> (grant_1))) \ - && ((! (idle)) -> (X ((! (grant_0)) && (! (grant_1))))))) \ - && (! (F (G ((request_0) && (X (! (grant_0)))))))) \ - && (! (F (G ((request_1) && (X (! (grant_1)))))))))" -outs = ["grant_0", "grant1"] -tc.assertEqual(synt_ltlf(f1, outs)[0], False)