diff --git a/spot/twaalgos/game.cc b/spot/twaalgos/game.cc index faf29b2ba..add0926fe 100644 --- a/spot/twaalgos/game.cc +++ b/spot/twaalgos/game.cc @@ -272,12 +272,16 @@ namespace spot // Only the states owned by the winner need a strategy assert([&]() { + std::unordered_set valid_strat; + for (const auto& e : arena_->edges()) + valid_strat.insert(arena_->edge_number(e)); + for (unsigned v = 0; v < arena_->num_states(); ++v) { if (!solve_globally && (info_->scc_of(v) == -1u)) continue; if (((*owner_ptr_)[v] == w_.winner(v)) - && ((s_[v] <= 0) || (s_[v] > arena_->num_edges()))) + && (valid_strat.count(s_.at(v)) == 0)) return false; } return true; diff --git a/tests/python/game.py b/tests/python/game.py index a7080b696..857390335 100644 --- a/tests/python/game.py +++ b/tests/python/game.py @@ -384,4 +384,141 @@ spot.solve_game(aut) S1 = list(spot.get_strategy(aut)) spot.solve_game(aut) S2 = list(spot.get_strategy(aut)) -tc.assertEqual(S1, S2) \ No newline at end of file +tc.assertEqual(S1, S2) + + +# Finite games +alive = "__alive__" +def finite_existential(auts): + # 1 Accepting state -> 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) \ No newline at end of file