From 4260b17fba2e90241dbe0be70c4ee91d712debf3 Mon Sep 17 00:00:00 2001 From: philipp Date: Fri, 13 Aug 2021 14:50:16 +0200 Subject: [PATCH] New game api Introduce a new, uniform way to create and solve games. Games can now be created directly from specification using creat_game, uniformly solved using solve_game and transformed into a strategy using create_strategy. Strategy are mealy machines, which can be minimized. * bin/ltlsynt.cc: Minor adaption * spot/twaalgos/game.cc: solve_game, setters and getters for named properties * spot/twaalgos/game.hh: Here too * spot/twaalgos/mealy_machine.cc: Minor adaption * spot/twaalgos/synthesis.cc: create_game, create_strategy and minimize_strategy * spot/twaalgos/synthesis.hh: Here too * tests/core/ltlsynt.test: Adapting * tests/python/aiger.py , tests/python/games.ipynb , tests/python/mealy.py , tests/python/parity.py , tests/python/split.py: Adapting --- bin/ltlsynt.cc | 13 +- spot/twaalgos/game.cc | 219 +++- spot/twaalgos/game.hh | 131 ++- spot/twaalgos/mealy_machine.cc | 14 +- spot/twaalgos/synthesis.cc | 846 ++++++++++++-- spot/twaalgos/synthesis.hh | 73 +- tests/core/ltlsynt.test | 152 +-- tests/python/aiger.py | 2 +- tests/python/games.ipynb | 1995 +++++++++++++++++++++++++++++++- tests/python/mealy.py | 2 +- tests/python/parity.py | 16 +- tests/python/split.py | 5 +- 12 files changed, 3163 insertions(+), 305 deletions(-) diff --git a/bin/ltlsynt.cc b/bin/ltlsynt.cc index 948376601..a98d0176e 100644 --- a/bin/ltlsynt.cc +++ b/bin/ltlsynt.cc @@ -353,7 +353,7 @@ namespace << paritize_time << " seconds\n"; if (want_time) sw.start(); - dpa = split_2step(tmp, all_inputs, all_outputs, true, true); + dpa = split_2step(tmp, all_outputs, true, false); spot::colorize_parity_here(dpa, true); if (want_time) split_time = sw.stop(); @@ -376,7 +376,7 @@ namespace << " states\n"; if (want_time) sw.start(); - dpa = split_2step(aut, all_inputs, all_outputs, true, true); + dpa = split_2step(aut, all_outputs, true, false); spot::colorize_parity_here(dpa, true); if (want_time) split_time = sw.stop(); @@ -390,7 +390,7 @@ namespace { if (want_time) sw.start(); - auto split = split_2step(aut, all_inputs, all_outputs, + auto split = split_2step(aut, all_outputs, true, false); if (want_time) split_time = sw.stop(); @@ -447,7 +447,7 @@ namespace if (want_time) sw.start(); - dpa = split_2step(dpa, all_inputs, all_outputs, true, true); + dpa = split_2step(dpa, all_outputs, true, false); spot::colorize_parity_here(dpa, true); if (want_time) split_time = sw.stop(); @@ -472,7 +472,7 @@ namespace spot::print_hoa(std::cout, dpa, opt_print_hoa_args) << '\n'; return 0; } - + set_synthesis_outputs(dpa, all_outputs); if (want_time) sw.start(); bool player1winning = solve_parity_game(dpa); @@ -489,8 +489,7 @@ namespace { if (want_time) sw.start(); - auto strat_aut = apply_strategy(dpa, all_outputs, - true, false); + auto strat_aut = apply_strategy(dpa, true, false); if (want_time) strat2aut_time = sw.stop(); diff --git a/spot/twaalgos/game.cc b/spot/twaalgos/game.cc index 2c6fafdc7..545c5d89b 100644 --- a/spot/twaalgos/game.cc +++ b/spot/twaalgos/game.cc @@ -19,6 +19,9 @@ #include "config.h" +#include + +#include #include #include #include @@ -764,12 +767,81 @@ namespace spot } // anonymous + + std::ostream& operator<<(std::ostream& os, game_info::solver s) + { + using solver = game_info::solver; + switch (s) + { + case (solver::DET_SPLIT): + os << "ds"; + break; + case (solver::SPLIT_DET): + os << "sd"; + break; + case (solver::DPA_SPLIT): + os << "ps"; + break; + case (solver::LAR): + os << "lar"; + break; + case (solver::LAR_OLD): + os << "lar.old"; + break; + } + return os; +} + + std::ostream& + operator<<(std::ostream& os, const game_info& gi) + { + os << "force sbacc: " << gi.force_sbacc << '\n' + << "solver: " << gi.s << '\n' + << "minimization-lvl: " << gi.minimize_lvl << '\n' + << (gi.verbose_stream ? "Is verbose\n" : "Is not verbose\n") + << "the bdd_dict used is " << gi.dict.get(); + return os; + } + bool solve_parity_game(const twa_graph_ptr& arena) { parity_game pg; return pg.solve(arena); } + bool solve_game(twa_graph_ptr arena, game_info& gi) + { + stopwatch sw; + if (gi.bv) + sw.start(); + bool dummy1, dummy2; + bool ret; + + if (arena->acc().is_parity(dummy1, dummy2, true)) + { + if (gi.verbose_stream) + *(gi.verbose_stream) << "Identified as parity game.\n"; + ret = solve_parity_game(arena); + } + else + throw std::runtime_error("No solver available for this arena due to its" + "acceptance condition."); + if (gi.bv) + gi.bv->solve_time += sw.stop(); + if (gi.verbose_stream) + *(gi.verbose_stream) << "game solved in " + << gi.bv->solve_time << " seconds\n"; + return ret; + } + + bool + solve_game(twa_graph_ptr arena) + { + game_info dummy1; + return solve_game(arena, dummy1); + } + + void pg_print(std::ostream& os, const const_twa_graph_ptr& arena) { auto owner = ensure_parity_game(arena, "pg_print"); @@ -901,60 +973,86 @@ namespace spot return aut; } - void set_state_players(twa_graph_ptr arena, std::vector owners) + void set_state_players(twa_graph_ptr arena, const region_t& owners) { - std::vector* owners_ptr = new std::vector(owners); - set_state_players(arena, owners_ptr); + set_state_players(arena, region_t(owners)); } - void set_state_players(twa_graph_ptr arena, std::vector* owners) + void set_state_players(twa_graph_ptr arena, region_t&& owners) { - if (owners->size() != arena->num_states()) + if (owners.size() != arena->num_states()) throw std::runtime_error ("set_state_players(): There must be as many owners as states"); - arena->set_named_prop>("state-player", owners); + arena->set_named_prop("state-player", + new region_t(std::forward(owners))); } - void set_state_player(twa_graph_ptr arena, unsigned state, unsigned owner) + void set_state_player(twa_graph_ptr arena, unsigned state, bool owner) { if (state >= arena->num_states()) throw std::runtime_error("set_state_player(): invalid state number"); - std::vector *owners = arena->get_named_prop> - ("state-player"); + region_t *owners = arena->get_named_prop("state-player"); if (!owners) - { - owners = new std::vector(arena->num_states(), false); - arena->set_named_prop>("state-player", owners); - } + throw std::runtime_error("set_state_player(): Can only set the state of " + "an individual " + "state if \"state-player\" already exists."); + if (owners->size() != arena->num_states()) + throw std::runtime_error("set_state_player(): The \"state-player\" " + "vector has a different " + "size comparerd to the automaton! " + "Called new_state in between?"); (*owners)[state] = owner; } - const std::vector& get_state_players(const_twa_graph_ptr arena) + const region_t& get_state_players(const_twa_graph_ptr arena) { - std::vector *owners = arena->get_named_prop> + region_t *owners = arena->get_named_prop ("state-player"); if (!owners) throw std::runtime_error - ("get_state_players(): state-player property not defined, not a game"); + ("get_state_players(): state-player property not defined, not a game?"); return *owners; } - unsigned get_state_player(const_twa_graph_ptr arena, unsigned state) + bool get_state_player(const_twa_graph_ptr arena, unsigned state) { if (state >= arena->num_states()) throw std::runtime_error("get_state_player(): invalid state number"); - std::vector* owners = arena->get_named_prop> - ("state-player"); + region_t* owners = arena->get_named_prop("state-player"); if (!owners) throw std::runtime_error - ("get_state_player(): state-player property not defined, not a game"); + ("get_state_player(): state-player property not defined, not a game?"); - return (*owners)[state] ? 1 : 0; + return (*owners)[state]; + } + + + const strategy_t& get_strategy(const_twa_graph_ptr arena) + { + auto strat_ptr = arena->get_named_prop("strategy"); + if (!strat_ptr) + throw std::runtime_error("get_strategy(): Named prop " + "\"strategy\" not set." + "Arena not solved?"); + return *strat_ptr; + } + + void set_strategy(twa_graph_ptr arena, const strategy_t& strat) + { + set_strategy(arena, strategy_t(strat)); + } + void set_strategy(twa_graph_ptr arena, strategy_t&& strat) + { + if (arena->num_states() != strat.size()) + throw std::runtime_error("set_strategy(): strategies need to have " + "the same size as the automaton."); + arena->set_named_prop("strategy", + new strategy_t(std::forward(strat))); } void set_synthesis_outputs(const twa_graph_ptr& arena, const bdd& outs) @@ -971,6 +1069,85 @@ namespace spot ("get_synthesis_outputs(): synthesis-outputs not defined"); } + std::vector + get_synthesis_output_aps(const const_twa_graph_ptr& arena) + { + std::vector out_names; + + bdd outs = get_synthesis_outputs(arena); + + auto dict = arena->get_dict(); + + auto to_bdd = [&](const auto& x) + { + return bdd_ithvar(dict->has_registered_proposition(x, arena.get())); + }; + + for (const auto& ap : arena->ap()) + if (bdd_implies(outs, to_bdd(ap))) + out_names.push_back(ap.ap_name()); + + return out_names; + } + + + void set_state_winners(twa_graph_ptr arena, const region_t& winners) + { + set_state_winners(arena, region_t(winners)); + } + + void set_state_winners(twa_graph_ptr arena, region_t&& winners) + { + if (winners.size() != arena->num_states()) + throw std::runtime_error + ("set_state_winners(): There must be as many winners as states"); + + arena->set_named_prop("state-winner", + new region_t(std::forward(winners))); + } + + void set_state_winner(twa_graph_ptr arena, unsigned state, bool winner) + { + if (state >= arena->num_states()) + throw std::runtime_error("set_state_winner(): invalid state number"); + + region_t *winners = arena->get_named_prop("state-winner"); + if (!winners) + throw std::runtime_error("set_state_winner(): Can only set the state of " + "an individual " + "state if \"state-winner\" already exists."); + if (winners->size() != arena->num_states()) + throw std::runtime_error("set_state_winner(): The \"state-winnerr\" " + "vector has a different " + "size compared to the automaton! " + "Called new_state in between?"); + + (*winners)[state] = winner; + } + + const region_t& get_state_winners(const_twa_graph_ptr arena) + { + region_t *winners = arena->get_named_prop("state-winner"); + if (!winners) + throw std::runtime_error + ("get_state_winners(): state-winner property not defined, not a game?"); + + return *winners; + } + + bool get_state_winner(const_twa_graph_ptr arena, unsigned state) + { + if (state >= arena->num_states()) + throw std::runtime_error("get_state_winner(): invalid state number"); + + region_t* winners = arena->get_named_prop("state-winner"); + if (!winners) + throw std::runtime_error + ("get_state_winner(): state-winner property not defined, not a game?"); + + return (*winners)[state]; + } + bool solve_safety_game(twa_graph_ptr game) { diff --git a/spot/twaalgos/game.hh b/spot/twaalgos/game.hh index fd079f733..b6f9c4742 100644 --- a/spot/twaalgos/game.hh +++ b/spot/twaalgos/game.hh @@ -26,6 +26,7 @@ #include #include +#include #include #include @@ -88,6 +89,90 @@ namespace spot SPOT_API bool solve_safety_game(twa_graph_ptr game); + /// \brief Benchmarking and options structure for games and synthesis + /// + /// \note This structure is designed to interface with the algorithms + /// found in spot/twaalgos/synthesis.hh + struct SPOT_API game_info + { + + enum class solver + { + DET_SPLIT=0, + SPLIT_DET, + DPA_SPLIT, + LAR, + LAR_OLD, + }; + + struct bench_var + { + double total_time = 0.0; + double trans_time = 0.0; + double split_time = 0.0; + double paritize_time = 0.0; + double solve_time = 0.0; + double strat2aut_time = 0.0; + double aig_time = 0.0; + unsigned nb_states_arena = 0; + unsigned nb_states_arena_env = 0; + unsigned nb_states_parity_game = 0; + unsigned nb_strat_states = 0; + unsigned nb_strat_edges = 0; + unsigned nb_latches = 0; + unsigned nb_gates = 0; + bool realizable = false; + }; + + game_info() + : force_sbacc{false}, + s{solver::LAR}, + minimize_lvl{0}, + out_choice{0}, + bv{}, + verbose_stream{nullptr}, + dict(make_bdd_dict()) + { + } + + bool force_sbacc; + solver s; + int minimize_lvl; + int out_choice; + std::optional bv; + std::ostream* verbose_stream; + option_map opt; + bdd_dict_ptr dict; + }; + + /// \brief Stream solvers + SPOT_API std::ostream& + operator<<(std::ostream& os, game_info::solver s); + + /// \brief Stream benchmarks and options + SPOT_API std::ostream & + operator<<(std::ostream &os, const game_info &gi); + + /// \brief Generic interface for game solving + /// + /// Calls the most suitable solver, depending on the type of game/ + /// acceptance condition + /// + /// \param arena The game arena + /// \param gi struct ofr options and benchmarking + /// \return Whether the initial state is won by player or not + /// \pre Relies on the named properties "state-player" + /// \post The named properties "strategy" and "state-winner" are set + SPOT_API bool + solve_game(twa_graph_ptr arena, game_info& gi); + + /// \brief Generic interface for game solving + /// + /// See solve_game(arena, gi) + SPOT_API bool + solve_game(twa_graph_ptr arena); + + /// \brief Print a max odd parity game using PG-solver syntax SPOT_API void pg_print(std::ostream& os, const const_twa_graph_ptr& arena); @@ -103,26 +188,54 @@ namespace spot /// \brief Set the owner for all the states. SPOT_API - void set_state_players(twa_graph_ptr arena, std::vector owners); + void set_state_players(twa_graph_ptr arena, const region_t& owners); SPOT_API - void set_state_players(twa_graph_ptr arena, std::vector* owners); + void set_state_players(twa_graph_ptr arena, region_t&& owners); /// \brief Set the owner of a state. SPOT_API - void set_state_player(twa_graph_ptr arena, unsigned state, unsigned owner); - - /// \brief Get the owner of all the state. - SPOT_API - const std::vector& get_state_players(const_twa_graph_ptr arena); + void set_state_player(twa_graph_ptr arena, unsigned state, bool owner); /// \brief Get the owner of a state. SPOT_API - unsigned get_state_player(const_twa_graph_ptr arena, unsigned state); + bool get_state_player(const_twa_graph_ptr arena, unsigned state); + /// \brief Get the owner of all states + SPOT_API + const region_t& get_state_players(const_twa_graph_ptr arena); + + /// \brief Get or set the strategy + SPOT_API + const strategy_t& get_strategy(const_twa_graph_ptr arena); + SPOT_API + void set_strategy(twa_graph_ptr arena, const strategy_t& strat); + SPOT_API + void set_strategy(twa_graph_ptr arena, strategy_t&& strat); /// \brief Set all synthesis outputs as a conjunction SPOT_API void set_synthesis_outputs(const twa_graph_ptr& arena, const bdd& outs); - SPOT_API bdd get_synthesis_outputs(const const_twa_graph_ptr& arena); + + /// \brief Get the vector with the names of the output propositions + SPOT_API + std::vector + get_synthesis_output_aps(const const_twa_graph_ptr& arena); + + /// \brief Set the winner for all the states. + SPOT_API + void set_state_winners(twa_graph_ptr arena, const region_t& winners); + SPOT_API + void set_state_winners(twa_graph_ptr arena, region_t&& winners); + + /// \brief Set the winner of a state. + SPOT_API + void set_state_winner(twa_graph_ptr arena, unsigned state, bool winner); + + /// \brief Get the winner of a state. + SPOT_API + bool get_state_winner(const_twa_graph_ptr arena, unsigned state); + /// \brief Get the winner of all states + SPOT_API + const region_t& get_state_winners(const_twa_graph_ptr arena); } diff --git a/spot/twaalgos/mealy_machine.cc b/spot/twaalgos/mealy_machine.cc index 33cc0c2a5..9f78d5426 100644 --- a/spot/twaalgos/mealy_machine.cc +++ b/spot/twaalgos/mealy_machine.cc @@ -507,12 +507,7 @@ namespace spot // Split if the initial aut was split if (orig_is_split) { - bdd ins = bddtrue; - for (const auto& ap : mmc->ap()) - if (!bdd_implies(outs, - bdd_ithvar(mmc->register_ap(ap)))) - ins &= bdd_ithvar(mmc->register_ap(ap)); - mmc = split_2step(mmc, ins, outs, false, false); + mmc = split_2step(mmc, outs, false, false); bool orig_init_player = mm->get_named_prop>("state-player") ->at(mm->get_init_state_number()); @@ -587,12 +582,7 @@ namespace spot mm->purge_unreachable_states(); if (orig_is_split) { - bdd ins = bddtrue; - for (const auto& ap : mm->ap()) - if (!bdd_implies(outs, - bdd_ithvar(mm->register_ap(ap)))) - ins &= bdd_ithvar(mm->register_ap(ap)); - mm = split_2step(mm, ins, outs, false, false); + mm = split_2step(mm, outs, false, false); alternate_players(mm, init_player, false); mm->set_named_prop("synthesis-outputs", new bdd(outs)); } diff --git a/spot/twaalgos/synthesis.cc b/spot/twaalgos/synthesis.cc index 133756c25..2319df666 100644 --- a/spot/twaalgos/synthesis.cc +++ b/spot/twaalgos/synthesis.cc @@ -18,10 +18,22 @@ // along with this program. If not, see . #include "config.h" +#include +#include +#include +#include +#include +#include +#include +#include +#include #include +#include #include #include -#include +#include +#include + #include @@ -122,7 +134,7 @@ namespace{ namespace spot { twa_graph_ptr - split_2step(const const_twa_graph_ptr& aut, const bdd& input_bdd, + split_2step(const const_twa_graph_ptr& aut, const bdd& output_bdd, bool complete_env, bool do_simplify) { @@ -132,6 +144,21 @@ namespace spot split->new_states(aut->num_states()); split->set_init_state(aut->get_init_state_number()); + + bdd input_bdd = bddtrue; + { + bdd allbdd = aut->ap_vars(); + while (allbdd != bddtrue) + { + bdd l = bdd_ithvar(bdd_var(allbdd)); + if (not bdd_implies(output_bdd, l)) + // Input + input_bdd &= l; + allbdd = bdd_high(allbdd); + assert(allbdd != bddfalse); + } + } + // The environment has all states // with num <= aut->num_states(); // So we can first loop over the aut @@ -292,11 +319,10 @@ namespace spot // The named property // compute the owners // env is equal to false - std::vector* owner = - new std::vector(split->num_states(), false); + std::vector owner(split->num_states(), false); // All "new" states belong to the player - std::fill(owner->begin()+aut->num_states(), owner->end(), true); - split->set_named_prop("state-player", owner); + std::fill(owner.begin()+aut->num_states(), owner.end(), true); + set_state_players(split, std::move(owner)); // Done return split; } @@ -312,10 +338,7 @@ namespace spot // split_2step is not guaranteed to produce // states that alternate between env and player do to do_simplify - auto owner_ptr = aut->get_named_prop>("state-player"); - if (!owner_ptr) - throw std::runtime_error("unsplit requires the named prop " - "state-player as set by split_2step"); + auto owner = get_state_players(aut); std::vector state_map(aut->num_states(), unseen_mark); auto seen = [&](unsigned s){return state_map[s] != unseen_mark; }; @@ -338,7 +361,7 @@ namespace spot for (const auto& i : aut->out(cur)) { // if the dst is also owned env - if (!(*owner_ptr)[i.dst]) + if (!owner[i.dst]) { // This can only happen if there is only // one outgoing edges for cur @@ -364,129 +387,730 @@ namespace spot out->set_init_state(map_s(aut->get_init_state_number())); // Try to set outputs if (bdd* outptr = aut->get_named_prop("synthesis-outputs")) - out->set_named_prop("synthesis-outputs", new bdd(*outptr)); + set_synthesis_outputs(out, *outptr); return out; } - + // Improved apply strat, that reduces the number of edges/states + // while keeping the needed edge-properties + // Note, this only deals with deterministic strategies + // Note, assumes that env starts playing spot::twa_graph_ptr apply_strategy(const spot::twa_graph_ptr& arena, - bdd all_outputs, bool unsplit, bool keep_acc) { - std::vector* w_ptr = - arena->get_named_prop>("state-winner"); - std::vector* s_ptr = - arena->get_named_prop>("strategy"); - std::vector* sp_ptr = - arena->get_named_prop>("state-player"); + const auto& win = get_state_winners(arena); + const auto& strat = get_strategy(arena); + const auto& sp = get_state_players(arena); + auto outs = get_synthesis_outputs(arena); - if (!w_ptr || !s_ptr || !sp_ptr) - throw std::runtime_error("Arena missing state-winner, strategy " - "or state-player"); - - if (!(w_ptr->at(arena->get_init_state_number()))) + if (!win[arena->get_init_state_number()]) throw std::runtime_error("Player does not win initial state, strategy " "is not applicable"); - std::vector& w = *w_ptr; - std::vector& s = *s_ptr; + assert((sp[arena->get_init_state_number()] == false) + && "Env needs to have first turn!"); - auto aut = spot::make_twa_graph(arena->get_dict()); - aut->copy_ap_of(arena); + assert(std::all_of(arena->edges().begin(), arena->edges().end(), + [&sp](const auto& e) + { return sp.at(e.src) != sp.at(e.dst); })); + + auto strat_split = spot::make_twa_graph(arena->get_dict()); + strat_split->copy_ap_of(arena); if (keep_acc) - aut->copy_acceptance_of(arena); + strat_split->copy_acceptance_of(arena); + + std::stack todo; + todo.push(arena->get_init_state_number()); + + struct dca{ + unsigned dst; + unsigned condvar; + acc_cond::mark_t acc; + }; + struct dca_hash + { + size_t operator()(const dca& d) const noexcept + { + return pair_hash()(std::make_pair(d.dst, d.condvar)) + ^ d.acc.hash(); + } + }; + struct dca_equal + { + bool operator()(const dca& d1, const dca& d2) const noexcept + { + return std::tie(d1.dst, d1.condvar, d1.acc) + == std::tie(d2.dst, d2.condvar, d2.acc); + } + }; + + //env dst + player cond + acc -> p stat + std::unordered_map p_map; constexpr unsigned unseen_mark = std::numeric_limits::max(); - std::vector todo{arena->get_init_state_number()}; - std::vector pg2aut(arena->num_states(), unseen_mark); - aut->set_init_state(aut->new_state()); - pg2aut[arena->get_init_state_number()] = aut->get_init_state_number(); + std::vector env_map(arena->num_states(), unseen_mark); + strat_split->set_init_state(strat_split->new_state()); + env_map[arena->get_init_state_number()] = + strat_split->get_init_state_number(); + + // The states in the new graph are qualified local + // Get a local environment state + auto get_sel = [&](unsigned s) + { + if (SPOT_UNLIKELY(env_map[s] == unseen_mark)) + env_map[s] = strat_split->new_state(); + return env_map[s]; + }; + + // local dst + // Check if there exists already a local player state + // that has the same dst, cond and (if keep_acc is true) acc + auto get_spl = [&](unsigned dst, const bdd& cond, acc_cond::mark_t acc) + { + dca d{dst, (unsigned) cond.id(), acc}; + auto it = p_map.find(d); + if (it != p_map.end()) + return it->second; + unsigned ns = strat_split->new_state(); + p_map[d] = ns; + strat_split->new_edge(ns, dst, cond, acc); + return ns; + }; while (!todo.empty()) { - unsigned v = todo.back(); - todo.pop_back(); - - // Check if a simplification occurred - // in the aut and we have env -> env - - // Env edge -> keep all - for (auto &e1: arena->out(v)) + unsigned src_env = todo.top(); + unsigned src_envl = get_sel(src_env); + todo.pop(); + // All env edges + for (const auto& e_env : arena->out(src_env)) { - assert(w.at(e1.dst)); - // Check if a simplification occurred - // in the aut and we have env -> env - if (!(*sp_ptr)[e1.dst]) - { - assert(([&arena, v]() - { - auto out_cont = arena->out(v); - return (++(out_cont.begin()) == out_cont.end()); - })()); - // If so we do not need to unsplit - if (pg2aut[e1.dst] == unseen_mark) - { - pg2aut[e1.dst] = aut->new_state(); - todo.push_back(e1.dst); - } - // Create the edge - aut->new_edge(pg2aut[v], - pg2aut[e1.dst], - e1.cond, - keep_acc ? e1.acc : spot::acc_cond::mark_t({})); - // Done - continue; - } - - if (!unsplit) - { - if (pg2aut[e1.dst] == unseen_mark) - pg2aut[e1.dst] = aut->new_state(); - aut->new_edge(pg2aut[v], pg2aut[e1.dst], e1.cond, - keep_acc ? e1.acc : spot::acc_cond::mark_t({})); - } - // Player strat - auto &e2 = arena->edge_storage(s[e1.dst]); - if (pg2aut[e2.dst] == unseen_mark) - { - pg2aut[e2.dst] = aut->new_state(); - todo.push_back(e2.dst); - } - - aut->new_edge(unsplit ? pg2aut[v] : pg2aut[e1.dst], - pg2aut[e2.dst], - unsplit ? (e1.cond & e2.cond) : e2.cond, - keep_acc ? e2.acc : spot::acc_cond::mark_t({})); + // Get the corresponding strat + const auto& e_strat = arena->edge_storage(strat[e_env.dst]); + // Check if already explored + if (env_map[e_strat.dst] == unseen_mark) + todo.push(e_strat.dst); + unsigned dst_envl = get_sel(e_strat.dst); + // The new env edge, player is constructed automatically + auto used_acc = keep_acc ? e_strat.acc : acc_cond::mark_t({}); + strat_split->new_edge(src_envl, + get_spl(dst_envl, e_strat.cond, used_acc), + e_env.cond, used_acc); } } + // All states exists, we can try to further merge them + // Specialized merge + std::vector spnew(strat_split->num_states(), false); + for (const auto& p : p_map) + spnew[p.second] = true; - aut->set_named_prop("synthesis-outputs", new bdd(all_outputs)); - // If no unsplitting is demanded, it remains a two-player arena - // We do not need to track winner as this is a - // strategy automaton - if (!unsplit) + // Sorting edges in place + auto comp_edge = [](const auto& e1, const auto& e2) + { + return std::tuple(e1.dst, e1.acc, e1.cond.id()) + < std::tuple(e2.dst, e2.acc, e2.cond.id()); + }; + auto sort_edges_of = + [&, &split_graph = strat_split->get_graph()](unsigned s) { - const std::vector& sp_pg = * sp_ptr; - std::vector sp_aut(aut->num_states()); - std::vector str_aut(aut->num_states()); - for (unsigned i = 0; i < arena->num_states(); ++i) - { - if (pg2aut[i] == unseen_mark) - // Does not appear in strategy - continue; - sp_aut[pg2aut[i]] = sp_pg[i]; - str_aut[pg2aut[i]] = s[i]; - } - aut->set_named_prop( - "state-player", new std::vector(std::move(sp_aut))); - aut->set_named_prop( - "state-winner", new std::vector(aut->num_states(), true)); - aut->set_named_prop( - "strategy", new std::vector(std::move(str_aut))); - } - return aut; + static std::vector edge_nums; + edge_nums.clear(); + auto eit = strat_split->out(s); + const auto eit_e = eit.end(); + // 0 Check if it is already sorted + if (std::is_sorted(eit.begin(), eit_e, comp_edge)) + return false; // No change + // 1 Get all edges numbers and sort them + std::transform(eit.begin(), eit_e, std::back_inserter(edge_nums), + [&](const auto& e) + { return strat_split->edge_number(e); }); + std::sort(edge_nums.begin(), edge_nums.end(), + [&](unsigned ne1, unsigned ne2) + { return comp_edge(strat_split->edge_storage(ne1), + strat_split->edge_storage(ne2)); }); + // 2 Correct the order + auto& sd = split_graph.state_storage(s); + sd.succ = edge_nums.front(); + sd.succ_tail = edge_nums.back(); + const unsigned n_edges_p = edge_nums.size()-1; + for (unsigned i = 0; i < n_edges_p; ++i) + split_graph.edge_storage(edge_nums[i]).next_succ = edge_nums[i+1]; + split_graph.edge_storage(edge_nums.back()).next_succ = 0; //terminal + // All nicely chained + return true; + }; + auto merge_edges_of = [&](unsigned s) + { + // Call this after sort edges of + // Mergeable edges are nicely chained + bool changed = false; + auto eit = strat_split->out_iteraser(s); + unsigned idx_last = strat_split->edge_number(*eit); + ++eit; + while (eit) + { + auto& e_last = strat_split->edge_storage(idx_last); + if (std::tie(e_last.dst, e_last.acc) + == std::tie(eit->dst, eit->acc)) + { + //Same dest and acc -> or condition + e_last.cond |= eit->cond; + eit.erase(); + changed = true; + } + else + { + idx_last = strat_split->edge_number(*eit); + ++eit; + } + } + return changed; + }; + auto merge_able = [&](unsigned s1, unsigned s2) + { + auto eit1 = strat_split->out(s1); + auto eit2 = strat_split->out(s2); + // Note: No self-loops here + return std::equal(eit1.begin(), eit1.end(), + eit2.begin(), eit2.end(), + [](const auto& e1, const auto& e2) + { + return std::tuple(e1.dst, e1.acc, e1.cond.id()) + == std::tuple(e2.dst, e2.acc, e2.cond.id()); + }); + }; + +// print_hoa(std::cout, strat_split) << '\n'; + + const unsigned n_sstrat = strat_split->num_states(); + std::vector remap(n_sstrat, -1u); + bool changed_any; + std::vector to_check; + to_check.reserve(n_sstrat); + // First iteration -> all env states are candidates + for (unsigned i = 0; i < n_sstrat; ++i) + if (!spnew[i]) + to_check.push_back(i); + + while (true) + { + changed_any = false; + std::for_each(to_check.begin(), to_check.end(), + [&](unsigned s){ sort_edges_of(s); merge_edges_of(s); }); + // Check if we can merge env states + for (unsigned s1 : to_check) + for (unsigned s2 = 0; s2 < n_sstrat; ++s2) + { + if (spnew[s2] || (s1 == s2)) + continue; // Player state or s1 == s2 + if ((remap[s2] < s2)) + continue; //s2 is already remapped + if (merge_able(s1, s2)) + { + changed_any = true; + if (s1 < s2) + remap[s2] = s1; + else + remap[s1] = s2; + break; + } + } + +// std::for_each(remap.begin(), remap.end(), +// [](auto e){std::cout << e << ' ';}); +// std::cout << std::endl; + + if (!changed_any) + break; + // Redirect changed targets and set possibly mergeable states + to_check.clear(); + for (auto& e : strat_split->edges()) + if (remap[e.dst] != -1u) + { + e.dst = remap[e.dst]; + to_check.push_back(e.src); + assert(spnew[e.src]); + } + + // Now check the player states + // We can skip sorting -> only one edge + // todo change when multistrat + changed_any = false; + for (unsigned s1 : to_check) + for (unsigned s2 = 0; s2 < n_sstrat; ++s2) + { + if (!spnew[s2] || (s1 == s2)) + continue; // Env state or s1 == s2 + if ((remap[s2] < s2)) + continue; //s2 is already remapped + if (merge_able(s1, s2)) + { + changed_any = true; + if (s1 < s2) + remap[s2] = s1; + else + remap[s1] = s2; + break; + } + } + +// std::for_each(remap.begin(), remap.end(), [](auto e) +// {std::cout << e << ' '; }); +// std::cout << std::endl; + + if (!changed_any) + break; + // Redirect changed targets and set possibly mergeable states + to_check.clear(); + for (auto& e : strat_split->edges()) + if (remap[e.dst] != -1u) + { + e.dst = remap[e.dst]; + to_check.push_back(e.src); + assert(!spnew[e.src]); + } + } + +// print_hoa(std::cout, strat_split) << std::endl; + + // Defrag and alternate + if (remap[strat_split->get_init_state_number()] != -1u) + strat_split->set_init_state(remap[strat_split->get_init_state_number()]); + unsigned st = 0; + for (auto& s: remap) + if (s == -1U) + s = st++; + else + s = -1U; + + strat_split->defrag_states(remap, st); + +// unsigned n_old; +// do +// { +// n_old = strat_split->num_edges(); +// strat_split->merge_edges(); +// strat_split->merge_states(); +// } while (n_old != strat_split->num_edges()); + + alternate_players(strat_split, false, false); +// print_hoa(std::cout, strat_split) << std::endl; + // What we do now depends on whether we unsplit or not + if (unsplit) + { + auto final = unsplit_2step(strat_split); + set_synthesis_outputs(final, outs); + return final; + } + // Keep the splitted version + set_state_winners(strat_split, region_t(strat_split->num_states(), true)); + + std::vector new_strat(strat_split->num_states(), -1u); + + for (unsigned i = 0; i < strat_split->num_states(); ++i) + { + if (!sp[i]) + continue; + new_strat[i] = strat_split->edge_number(*strat_split->out(i).begin()); + } + set_strategy(strat_split, std::move(new_strat)); + set_synthesis_outputs(strat_split, outs); + return strat_split; } -} // spot \ No newline at end of file + namespace // Anonymous create_game + { + static translator + create_translator(game_info& gi) + { + using solver = game_info::solver; + + option_map& extra_options = gi.opt; + auto sol = gi.s; + const bdd_dict_ptr& dict = gi.dict; + + for (auto&& p : std::vector> + {{"simul", 0}, + {"ba-simul", 0}, + {"det-simul", 0}, + {"tls-impl", 1}, + {"wdba-minimize", 2}}) + extra_options.set(p.first, extra_options.get(p.first, p.second)); + + translator trans(dict, &extra_options); + switch (sol) + { + case solver::LAR: + SPOT_FALLTHROUGH; + case solver::LAR_OLD: + trans.set_type(postprocessor::Generic); + trans.set_pref(postprocessor::Deterministic); + break; + case solver::DPA_SPLIT: + trans.set_type(postprocessor::ParityMaxOdd); + trans.set_pref(postprocessor::Deterministic | postprocessor::Colored); + break; + case solver::DET_SPLIT: + SPOT_FALLTHROUGH; + case solver::SPLIT_DET: + break; + } + return trans; + } + + twa_graph_ptr + ntgba2dpa(const twa_graph_ptr& aut, bool force_sbacc) + { + // if the input automaton is deterministic, degeneralize it to be sure to + // end up with a parity automaton + auto dpa = tgba_determinize(degeneralize_tba(aut), + false, true, true, false); + dpa->merge_edges(); + if (force_sbacc) + dpa = sbacc(dpa); + reduce_parity_here(dpa, true); + change_parity_here(dpa, parity_kind_max, + parity_style_odd); + assert(( + [&dpa]() -> bool { + bool max, odd; + dpa->acc().is_parity(max, odd); + return max && odd; + }())); + assert(is_deterministic(dpa)); + return dpa; + } + } // anonymous + + twa_graph_ptr + create_game(const formula& f, + const std::vector& all_outs, + game_info& gi) + { + using solver = game_info::solver; + + [](std::vector sv, std::string msg) + { + std::sort(sv.begin(), sv.end()); + const unsigned svs = sv.size() - 1; + for (unsigned i = 0; i < svs; ++i) + if (sv[i] == sv[i+1]) + throw std::runtime_error(msg + sv[i]); + }(all_outs, "Output propositions are expected to appear once " + "in all_outs. Violating: "); + + auto trans = create_translator(gi); + // Shortcuts + auto& bv = gi.bv; + auto& vs = gi.verbose_stream; + + stopwatch sw; + + if (bv) + sw.start(); + auto aut = trans.run(f); + if (bv) + bv->trans_time += sw.stop(); + + if (vs) + { + assert(bv); + *vs << "translating formula done in " + << bv->trans_time << " seconds\n"; + *vs << "automaton has " << aut->num_states() + << " states and " << aut->num_sets() << " colors\n"; + } + auto tobdd = [&aut](const std::string& ap_name) + { + return bdd_ithvar(aut->register_ap(ap_name)); + }; + auto is_out = [&all_outs](const std::string& ao)->bool + { + return std::find(all_outs.begin(), all_outs.end(), + ao) != all_outs.end(); + }; + + // Check for each ap that actually appears in the graph + // whether its an in or out + bdd ins = bddtrue; + bdd outs = bddtrue; + for (auto&& aap : aut->ap()) + { + if (is_out(aap.ap_name())) + outs &= tobdd(aap.ap_name()); + else + ins &= tobdd(aap.ap_name()); + } + + twa_graph_ptr dpa = nullptr; + + switch (gi.s) + { + case solver::DET_SPLIT: + { + if (bv) + sw.start(); + auto tmp = ntgba2dpa(aut, gi.force_sbacc); + if (vs) + *vs << "determinization done\nDPA has " + << tmp->num_states() << " states, " + << tmp->num_sets() << " colors\n"; + tmp->merge_states(); + if (bv) + bv->paritize_time += sw.stop(); + if (vs) + *vs << "simplification done\nDPA has " + << tmp->num_states() << " states\n" + << "determinization and simplification took " + << bv->paritize_time << " seconds\n"; + if (bv) + sw.start(); + dpa = split_2step(tmp, outs, true, false); + colorize_parity_here(dpa, true); + if (bv) + bv->split_time += sw.stop(); + if (vs) + *vs << "split inputs and outputs done in " << bv->split_time + << " seconds\nautomaton has " + << tmp->num_states() << " states\n"; + break; + } + case solver::DPA_SPLIT: + { + if (bv) + sw.start(); + aut->merge_states(); + if (bv) + bv->paritize_time += sw.stop(); + if (vs) + *vs << "simplification done in " << bv->paritize_time + << " seconds\nDPA has " << aut->num_states() + << " states\n"; + if (bv) + sw.start(); + dpa = split_2step(aut, outs, true, false); + colorize_parity_here(dpa, true); + if (bv) + bv->split_time += sw.stop(); + if (vs) + *vs << "split inputs and outputs done in " << bv->split_time + << " seconds\nautomaton has " + << dpa->num_states() << " states\n"; + break; + } + case solver::SPLIT_DET: + { + sw.start(); + auto split = split_2step(aut, outs, + true, false); + if (bv) + bv->split_time += sw.stop(); + if (vs) + *vs << "split inputs and outputs done in " << bv->split_time + << " seconds\nautomaton has " + << split->num_states() << " states\n"; + if (bv) + sw.start(); + dpa = ntgba2dpa(split, gi.force_sbacc); + if (vs) + *vs << "determinization done\nDPA has " + << dpa->num_states() << " states, " + << dpa->num_sets() << " colors\n"; + dpa->merge_states(); + if (bv) + bv->paritize_time += sw.stop(); + if (vs) + *vs << "simplification done\nDPA has " + << dpa->num_states() << " states\n" + << "determinization and simplification took " + << bv->paritize_time << " seconds\n"; + // The named property "state-player" is set in split_2step + // but not propagated by ntgba2dpa + alternate_players(dpa); + break; + } + case solver::LAR: + SPOT_FALLTHROUGH; + case solver::LAR_OLD: + { + if (bv) + sw.start(); + if (gi.s == solver::LAR) + { + dpa = to_parity(aut); + // reduce_parity is called by to_parity(), + // but with colorization turned off. + colorize_parity_here(dpa, true); + } + else + { + dpa = to_parity_old(aut); + dpa = reduce_parity_here(dpa, true); + } + change_parity_here(dpa, parity_kind_max, parity_style_odd); + if (bv) + bv->paritize_time += sw.stop(); + if (vs) + *vs << "LAR construction done in " << bv->paritize_time + << " seconds\nDPA has " + << dpa->num_states() << " states, " + << dpa->num_sets() << " colors\n"; + + if (bv) + sw.start(); + dpa = split_2step(dpa, outs, true, false); + colorize_parity_here(dpa, true); + if (bv) + bv->split_time += sw.stop(); + if (vs) + *vs << "split inputs and outputs done in " << bv->split_time + << " seconds\nautomaton has " + << dpa->num_states() << " states\n"; + break; + } + } //end switch solver + // Set the named properties + assert(dpa->get_named_prop>("state-player") + && "DPA has no state-players"); + set_synthesis_outputs(dpa, outs); + return dpa; + } + + twa_graph_ptr + create_game(const formula& f, + const std::vector& all_outs) + { + game_info dummy; + return create_game(f, all_outs, dummy); + } + + twa_graph_ptr + create_game(const std::string& f, + const std::vector& all_outs) + { + return create_game(parse_formula(f), all_outs); + } + + twa_graph_ptr + create_game(const std::string& f, + const std::vector& all_outs, + game_info& gi) + { + return create_game(parse_formula(f), all_outs, gi); + } + + void + minimize_strategy_here(twa_graph_ptr& strat, int min_lvl) + { + if (!strat->acc().is_t()) + throw std::runtime_error("minimize_strategy_here(): strategy is expected " + "to accept all runs! Otherwise it does not " + "correspond to a mealy machine and can not be " + "optimized this way."); + // 0 -> No minimization + // 1 -> Regular monitor/DFA minimization + // 2 -> Mealy minimization based on language inclusion + // with output assignement + // 3 -> Exact Mealy minimization using SAT + // 4 -> Monitor min then exact minimization + // 5 -> Mealy minimization based on language inclusion then exact + // minimization + bdd outs = get_synthesis_outputs(strat); + + switch (min_lvl) + { + case 0: + return; + case 1: + { + minimize_mealy_fast_here(strat, false); + break; + } + case 2: + { + minimize_mealy_fast_here(strat, true); + break; + } + case 3: + { + strat = minimize_mealy(strat, -1); + break; + } + case 4: + { + strat = minimize_mealy(strat, 0); + break; + } + case 5: + { + strat = minimize_mealy(strat, 1); + break; + } + default: + throw std::runtime_error("Unknown minimization option"); + } + set_synthesis_outputs(strat, outs); + } + + twa_graph_ptr + minimize_strategy(const_twa_graph_ptr& strat, int min_lvl) + { + auto strat_dup = spot::make_twa_graph(strat, spot::twa::prop_set::all()); + set_synthesis_outputs(strat_dup, + get_synthesis_outputs(strat)); + if (auto sp_ptr = strat->get_named_prop("state-player")) + set_state_players(strat_dup, *sp_ptr); + minimize_strategy_here(strat_dup, min_lvl); + return strat_dup; + } + + twa_graph_ptr + create_strategy(twa_graph_ptr arena, game_info& gi) + { + if (!arena) + throw std::runtime_error("Arena can not be null"); + + spot::stopwatch sw; + + if (gi.bv) + sw.start(); + + if (!get_state_winner(arena, arena->get_init_state_number())) + return nullptr; + + // If we use minimizations 0,1 or 2 -> unsplit + const bool do_unsplit = gi.minimize_lvl < 3; + twa_graph_ptr strat_aut = apply_strategy(arena, do_unsplit, false); + + strat_aut->prop_universal(true); + + minimize_strategy_here(strat_aut, gi.minimize_lvl); + + assert(do_unsplit + || strat_aut->get_named_prop>("state-player")); + if (!do_unsplit) + strat_aut = unsplit_2step(strat_aut); + + if (gi.bv) + { + gi.bv->strat2aut_time += sw.stop(); + gi.bv->nb_strat_states += strat_aut->num_states(); + gi.bv->nb_strat_edges += strat_aut->num_edges(); + } + + return strat_aut; + } + + twa_graph_ptr + create_strategy(twa_graph_ptr arena) + { + game_info dummy; + return create_strategy(arena, dummy); + } + +} // spot diff --git a/spot/twaalgos/synthesis.hh b/spot/twaalgos/synthesis.hh index 7b77e1592..47ed926d8 100644 --- a/spot/twaalgos/synthesis.hh +++ b/spot/twaalgos/synthesis.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2020 Laboratoire de Recherche et +// Copyright (C) 2020-2021 Laboratoire de Recherche et // Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -20,6 +20,7 @@ #pragma once #include +#include #include namespace spot @@ -40,8 +41,8 @@ namespace spot /// This function is used to transform an automaton into a turn-based game in /// the context of LTL reactive synthesis. /// \param aut automaton to be transformed - /// \param input_bdd conjunction of all input AP - /// \param output_bdd conjunction of all output AP + /// \param output_bdd conjunction of all output AP, all APs not present + /// are treated as inputs /// \param complete_env Whether the automaton should be complete for the /// environment, i.e. the player of I /// \param do_simplify If a state has a single outgoing transition @@ -52,7 +53,7 @@ namespace spot /// then egdes between the sinks will be added /// (assuming that the environnement/player of I) plays first SPOT_API twa_graph_ptr - split_2step(const const_twa_graph_ptr& aut, const bdd& input_bdd, + split_2step(const const_twa_graph_ptr& aut, const bdd& output_bdd, bool complete_env, bool do_simplify); /// \brief the reverse of split_2step @@ -62,16 +63,74 @@ namespace spot unsplit_2step(const const_twa_graph_ptr& aut); - /// \brief Takes a solved game and restricts the automat to the + /// \brief Creates a game from a specification and a set of + /// output propositions + /// + /// \param f The specification given as LTL/PSL formula + /// \param all_outs The names of all output propositions + /// \param gi game_info structure + /// \note All propositions in the formula that do not appear in all_outs + /// arer treated as input variables. + SPOT_API twa_graph_ptr + create_game(const formula& f, + const std::vector& all_outs, + game_info& gi); + + /// \brief create_game called with default options + SPOT_API twa_graph_ptr + create_game(const formula& f, + const std::vector& all_outs); + + /// \brief Like create_game but formula given as string + SPOT_API twa_graph_ptr + create_game(const std::string& f, + const std::vector& all_outs, + game_info& gi); + + /// \brief create_game called with default options + SPOT_API twa_graph_ptr + create_game(const std::string& f, + const std::vector& all_outs); + + /// \brief Takes a solved game and restricts the automaton to the /// winning strategy of the player /// /// \param arena twa_graph with named properties "state-player", /// "strategy" and "state-winner" - /// \param all_outputs bdd of all output signals /// \param unsplit Whether or not to unsplit the automaton /// \param keep_acc Whether or not keep the acceptance condition /// \return the resulting twa_graph SPOT_API spot::twa_graph_ptr apply_strategy(const spot::twa_graph_ptr& arena, - bdd all_outputs, bool unsplit, bool keep_acc); + bool unsplit, bool keep_acc); + + /// \brief Minimizes a strategy. Strategies are infact + /// Mealy machines. So we can use techniques designed for them + /// + /// \param strat The machine to minimize + /// \param min_lvl How to minimize the machine: + /// 0: No minimization, 1: Minimizing it like an DFA, + /// means the language is preserved, 2: Inclusion with + /// output assignement, 3: Exact minimization using + /// SAT solving, 4: SAT solving with DFA minimization as + /// preprocessing, 5: SAT solving using inclusion based + /// minimization with output assignment as preprocessing + /// \note min_lvl 1 and 2 work more efficiently on UNSPLIT strategies, + /// whereas min_lvl 3, 4 and 5 mandate a SPLIT strategy + SPOT_API void + minimize_strategy_here(twa_graph_ptr& strat, int min_lvl); + + ///\brief Like minimize_strategy_here + SPOT_API twa_graph_ptr + minimize_strategy(const_twa_graph_ptr& strat, int min_lvl); + + + /// \brief creates a strategy from a solved game taking into account the + /// options given in gi + SPOT_API twa_graph_ptr + create_strategy(twa_graph_ptr arena, game_info& gi); + + SPOT_API twa_graph_ptr + create_strategy(twa_graph_ptr arena); + } \ No newline at end of file diff --git a/tests/core/ltlsynt.test b/tests/core/ltlsynt.test index 33e733d3a..01dbf3f5c 100644 --- a/tests/core/ltlsynt.test +++ b/tests/core/ltlsynt.test @@ -74,17 +74,11 @@ diff out exp cat >exp <exp <exp <exp <exp <exp <exp <exp <exp <exp <exp <\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "Inf(\n", + "❸\n", + ") | (Fin(\n", + "❷\n", + ") & (Inf(\n", + "❶\n", + ") | Fin(\n", + "⓿\n", + ")))\n", + "[parity max odd 4]\n", + "\n", + "\n", + "\n", + "9\n", + "\n", + "9\n", + "\n", + "\n", + "\n", + "I->9\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "24\n", + "\n", + "24\n", + "\n", + "\n", + "\n", + "9->24\n", + "\n", + "\n", + "i0 & i1\n", + "❶\n", + "\n", + "\n", + "\n", + "25\n", + "\n", + "25\n", + "\n", + "\n", + "\n", + "9->25\n", + "\n", + "\n", + "i0 & !i1\n", + "❶\n", + "\n", + "\n", + "\n", + "26\n", + "\n", + "26\n", + "\n", + "\n", + "\n", + "9->26\n", + "\n", + "\n", + "!i0 & i1\n", + "❶\n", + "\n", + "\n", + "\n", + "27\n", + "\n", + "27\n", + "\n", + "\n", + "\n", + "9->27\n", + "\n", + "\n", + "!i0 & !i1\n", + "❶\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "\n", + "10\n", + "\n", + "10\n", + "\n", + "\n", + "\n", + "0->10\n", + "\n", + "\n", + "i1\n", + "❶\n", + "\n", + "\n", + "\n", + "11\n", + "\n", + "11\n", + "\n", + "\n", + "\n", + "0->11\n", + "\n", + "\n", + "!i1\n", + "❶\n", + "\n", + "\n", + "\n", + "10->0\n", + "\n", + "\n", + "o0\n", + "❸\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "11->1\n", + "\n", + "\n", + "o0\n", + "❸\n", + "\n", + "\n", + "\n", + "12\n", + "\n", + "12\n", + "\n", + "\n", + "\n", + "1->12\n", + "\n", + "\n", + "i1\n", + "❶\n", + "\n", + "\n", + "\n", + "13\n", + "\n", + "13\n", + "\n", + "\n", + "\n", + "1->13\n", + "\n", + "\n", + "!i1\n", + "❶\n", + "\n", + "\n", + "\n", + "12->0\n", + "\n", + "\n", + "!o0\n", + "❸\n", + "\n", + "\n", + "\n", + "13->1\n", + "\n", + "\n", + "!o0\n", + "❸\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "\n", + "14\n", + "\n", + "14\n", + "\n", + "\n", + "\n", + "2->14\n", + "\n", + "\n", + "i1\n", + "❶\n", + "\n", + "\n", + "\n", + "15\n", + "\n", + "15\n", + "\n", + "\n", + "\n", + "2->15\n", + "\n", + "\n", + "!i1\n", + "❶\n", + "\n", + "\n", + "\n", + "15->2\n", + "\n", + "\n", + "1\n", + "❸\n", + "\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", + "\n", + "\n", + "\n", + "3->12\n", + "\n", + "\n", + "i1\n", + "❶\n", + "\n", + "\n", + "\n", + "16\n", + "\n", + "16\n", + "\n", + "\n", + "\n", + "3->16\n", + "\n", + "\n", + "!i1\n", + "❶\n", + "\n", + "\n", + "\n", + "16->2\n", + "\n", + "\n", + "o0\n", + "❸\n", + "\n", + "\n", + "\n", + "16->3\n", + "\n", + "\n", + "!o0\n", + "❸\n", + "\n", + "\n", + "\n", + "4\n", + "\n", + "4\n", + "\n", + "\n", + "\n", + "4->14\n", + "\n", + "\n", + "i0\n", + "❶\n", + "\n", + "\n", + "\n", + "17\n", + "\n", + "17\n", + "\n", + "\n", + "\n", + "4->17\n", + "\n", + "\n", + "!i0\n", + "❶\n", + "\n", + "\n", + "\n", + "17->4\n", + "\n", + "\n", + "1\n", + "❸\n", + "\n", + "\n", + "\n", + "5\n", + "\n", + "5\n", + "\n", + "\n", + "\n", + "5->14\n", + "\n", + "\n", + "i0 & i1\n", + "❶\n", + "\n", + "\n", + "\n", + "5->15\n", + "\n", + "\n", + "i0 & !i1\n", + "❶\n", + "\n", + "\n", + "\n", + "5->17\n", + "\n", + "\n", + "!i0 & i1\n", + "❶\n", + "\n", + "\n", + "\n", + "18\n", + "\n", + "18\n", + "\n", + "\n", + "\n", + "5->18\n", + "\n", + "\n", + "!i0 & !i1\n", + "❶\n", + "\n", + "\n", + "\n", + "18->5\n", + "\n", + "\n", + "1\n", + "❸\n", + "\n", + "\n", + "\n", + "6\n", + "\n", + "6\n", + "\n", + "\n", + "\n", + "6->10\n", + "\n", + "\n", + "i0 & i1\n", + "❶\n", + "\n", + "\n", + "\n", + "6->11\n", + "\n", + "\n", + "i0 & !i1\n", + "❶\n", + "\n", + "\n", + "\n", + "19\n", + "\n", + "19\n", + "\n", + "\n", + "\n", + "6->19\n", + "\n", + "\n", + "!i0 & i1\n", + "❶\n", + "\n", + "\n", + "\n", + "20\n", + "\n", + "20\n", + "\n", + "\n", + "\n", + "6->20\n", + "\n", + "\n", + "!i0 & !i1\n", + "❶\n", + "\n", + "\n", + "\n", + "19->4\n", + "\n", + "\n", + "!o0\n", + "❸\n", + "\n", + "\n", + "\n", + "19->6\n", + "\n", + "\n", + "o0\n", + "❸\n", + "\n", + "\n", + "\n", + "20->4\n", + "\n", + "\n", + "!o0\n", + "❸\n", + "\n", + "\n", + "\n", + "7\n", + "\n", + "7\n", + "\n", + "\n", + "\n", + "20->7\n", + "\n", + "\n", + "o0\n", + "❸\n", + "\n", + "\n", + "\n", + "7->12\n", + "\n", + "\n", + "i0 & i1\n", + "❶\n", + "\n", + "\n", + "\n", + "7->13\n", + "\n", + "\n", + "i0 & !i1\n", + "❶\n", + "\n", + "\n", + "\n", + "21\n", + "\n", + "21\n", + "\n", + "\n", + "\n", + "7->21\n", + "\n", + "\n", + "!i0 & i1\n", + "❶\n", + "\n", + "\n", + "\n", + "22\n", + "\n", + "22\n", + "\n", + "\n", + "\n", + "7->22\n", + "\n", + "\n", + "!i0 & !i1\n", + "❶\n", + "\n", + "\n", + "\n", + "21->4\n", + "\n", + "\n", + "o0\n", + "❸\n", + "\n", + "\n", + "\n", + "21->6\n", + "\n", + "\n", + "!o0\n", + "❸\n", + "\n", + "\n", + "\n", + "22->4\n", + "\n", + "\n", + "o0\n", + "❸\n", + "\n", + "\n", + "\n", + "22->7\n", + "\n", + "\n", + "!o0\n", + "❸\n", + "\n", + "\n", + "\n", + "8\n", + "\n", + "8\n", + "\n", + "\n", + "\n", + "8->12\n", + "\n", + "\n", + "i0 & i1\n", + "❶\n", + "\n", + "\n", + "\n", + "8->16\n", + "\n", + "\n", + "i0 & !i1\n", + "❶\n", + "\n", + "\n", + "\n", + "8->21\n", + "\n", + "\n", + "!i0 & i1\n", + "❶\n", + "\n", + "\n", + "\n", + "23\n", + "\n", + "23\n", + "\n", + "\n", + "\n", + "8->23\n", + "\n", + "\n", + "!i0 & !i1\n", + "❶\n", + "\n", + "\n", + "\n", + "23->5\n", + "\n", + "\n", + "o0\n", + "❸\n", + "\n", + "\n", + "\n", + "23->8\n", + "\n", + "\n", + "!o0\n", + "❸\n", + "\n", + "\n", + "\n", + "24->0\n", + "\n", + "\n", + "1\n", + "❸\n", + "\n", + "\n", + "\n", + "25->3\n", + "\n", + "\n", + "1\n", + "❸\n", + "\n", + "\n", + "\n", + "26->6\n", + "\n", + "\n", + "1\n", + "❸\n", + "\n", + "\n", + "\n", + "27->8\n", + "\n", + "\n", + "1\n", + "❸\n", + "\n", + "\n", + "\n" + ], + "text/plain": [ + " *' at 0x7f7249801c30> >" + ] + }, + "metadata": {}, + "output_type": "display_data" + } + ], + "source": [ + "#Create the game\n", + "gi = spot.game_info()\n", + "gi.s = spot.game_info.solver_LAR #Use lar solver\n", + "\n", + "#Todo arena changes when executed multiple times\n", + "game = spot.create_game(\"G((F(i0) && F(i1))->(G(i1<->(X(o0)))))\", [\"o0\"], gi)\n", + "print(\"game has \", game.num_states(), \" states, and \", game.num_edges(), \" edges.\")\n", + "print(\"output propositions are \", spot.get_synthesis_output_aps(game))\n", + "display(game)" + ] + }, + { + "cell_type": "code", + "execution_count": 9, + "metadata": {}, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "Found a solution: True\n" + ] + }, + { + "data": { + "image/svg+xml": [ + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "Inf(\n", + "❸\n", + ") | (Fin(\n", + "❷\n", + ") & (Inf(\n", + "❶\n", + ") | Fin(\n", + "⓿\n", + ")))\n", + "[parity max odd 4]\n", + "\n", + "\n", + "\n", + "9\n", + "\n", + "9\n", + "\n", + "\n", + "\n", + "I->9\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "24\n", + "\n", + "24\n", + "\n", + "\n", + "\n", + "9->24\n", + "\n", + "\n", + "❶\n", + "\n", + "\n", + "\n", + "25\n", + "\n", + "25\n", + "\n", + "\n", + "\n", + "9->25\n", + "\n", + "\n", + "❶\n", + "\n", + "\n", + "\n", + "26\n", + "\n", + "26\n", + "\n", + "\n", + "\n", + "9->26\n", + "\n", + "\n", + "❶\n", + "\n", + "\n", + "\n", + "27\n", + "\n", + "27\n", + "\n", + "\n", + "\n", + "9->27\n", + "\n", + "\n", + "❶\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "\n", + "10\n", + "\n", + "10\n", + "\n", + "\n", + "\n", + "0->10\n", + "\n", + "\n", + "❶\n", + "\n", + "\n", + "\n", + "11\n", + "\n", + "11\n", + "\n", + "\n", + "\n", + "0->11\n", + "\n", + "\n", + "❶\n", + "\n", + "\n", + "\n", + "10->0\n", + "\n", + "\n", + "❸\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "11->1\n", + "\n", + "\n", + "❸\n", + "\n", + "\n", + "\n", + "12\n", + "\n", + "12\n", + "\n", + "\n", + "\n", + "1->12\n", + "\n", + "\n", + "❶\n", + "\n", + "\n", + "\n", + "13\n", + "\n", + "13\n", + "\n", + "\n", + "\n", + "1->13\n", + "\n", + "\n", + "❶\n", + "\n", + "\n", + "\n", + "12->0\n", + "\n", + "\n", + "❸\n", + "\n", + "\n", + "\n", + "13->1\n", + "\n", + "\n", + "❸\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "\n", + "14\n", + "\n", + "14\n", + "\n", + "\n", + "\n", + "2->14\n", + "\n", + "\n", + "❶\n", + "\n", + "\n", + "\n", + "15\n", + "\n", + "15\n", + "\n", + "\n", + "\n", + "2->15\n", + "\n", + "\n", + "❶\n", + "\n", + "\n", + "\n", + "15->2\n", + "\n", + "\n", + "❸\n", + "\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", + "\n", + "\n", + "\n", + "3->12\n", + "\n", + "\n", + "❶\n", + "\n", + "\n", + "\n", + "16\n", + "\n", + "16\n", + "\n", + "\n", + "\n", + "3->16\n", + "\n", + "\n", + "❶\n", + "\n", + "\n", + "\n", + "16->2\n", + "\n", + "\n", + "❸\n", + "\n", + "\n", + "\n", + "16->3\n", + "\n", + "\n", + "❸\n", + "\n", + "\n", + "\n", + "4\n", + "\n", + "4\n", + "\n", + "\n", + "\n", + "4->14\n", + "\n", + "\n", + "❶\n", + "\n", + "\n", + "\n", + "17\n", + "\n", + "17\n", + "\n", + "\n", + "\n", + "4->17\n", + "\n", + "\n", + "❶\n", + "\n", + "\n", + "\n", + "17->4\n", + "\n", + "\n", + "❸\n", + "\n", + "\n", + "\n", + "5\n", + "\n", + "5\n", + "\n", + "\n", + "\n", + "5->14\n", + "\n", + "\n", + "❶\n", + "\n", + "\n", + "\n", + "5->15\n", + "\n", + "\n", + "❶\n", + "\n", + "\n", + "\n", + "5->17\n", + "\n", + "\n", + "❶\n", + "\n", + "\n", + "\n", + "18\n", + "\n", + "18\n", + "\n", + "\n", + "\n", + "5->18\n", + "\n", + "\n", + "❶\n", + "\n", + "\n", + "\n", + "18->5\n", + "\n", + "\n", + "❸\n", + "\n", + "\n", + "\n", + "6\n", + "\n", + "6\n", + "\n", + "\n", + "\n", + "6->10\n", + "\n", + "\n", + "❶\n", + "\n", + "\n", + "\n", + "6->11\n", + "\n", + "\n", + "❶\n", + "\n", + "\n", + "\n", + "19\n", + "\n", + "19\n", + "\n", + "\n", + "\n", + "6->19\n", + "\n", + "\n", + "❶\n", + "\n", + "\n", + "\n", + "20\n", + "\n", + "20\n", + "\n", + "\n", + "\n", + "6->20\n", + "\n", + "\n", + "❶\n", + "\n", + "\n", + "\n", + "19->4\n", + "\n", + "\n", + "❸\n", + "\n", + "\n", + "\n", + "19->6\n", + "\n", + "\n", + "❸\n", + "\n", + "\n", + "\n", + "20->4\n", + "\n", + "\n", + "❸\n", + "\n", + "\n", + "\n", + "7\n", + "\n", + "7\n", + "\n", + "\n", + "\n", + "20->7\n", + "\n", + "\n", + "❸\n", + "\n", + "\n", + "\n", + "7->12\n", + "\n", + "\n", + "❶\n", + "\n", + "\n", + "\n", + "7->13\n", + "\n", + "\n", + "❶\n", + "\n", + "\n", + "\n", + "21\n", + "\n", + "21\n", + "\n", + "\n", + "\n", + "7->21\n", + "\n", + "\n", + "❶\n", + "\n", + "\n", + "\n", + "22\n", + "\n", + "22\n", + "\n", + "\n", + "\n", + "7->22\n", + "\n", + "\n", + "❶\n", + "\n", + "\n", + "\n", + "21->4\n", + "\n", + "\n", + "❸\n", + "\n", + "\n", + "\n", + "21->6\n", + "\n", + "\n", + "❸\n", + "\n", + "\n", + "\n", + "22->4\n", + "\n", + "\n", + "❸\n", + "\n", + "\n", + "\n", + "22->7\n", + "\n", + "\n", + "❸\n", + "\n", + "\n", + "\n", + "8\n", + "\n", + "8\n", + "\n", + "\n", + "\n", + "8->12\n", + "\n", + "\n", + "❶\n", + "\n", + "\n", + "\n", + "8->16\n", + "\n", + "\n", + "❶\n", + "\n", + "\n", + "\n", + "8->21\n", + "\n", + "\n", + "❶\n", + "\n", + "\n", + "\n", + "23\n", + "\n", + "23\n", + "\n", + "\n", + "\n", + "8->23\n", + "\n", + "\n", + "❶\n", + "\n", + "\n", + "\n", + "23->5\n", + "\n", + "\n", + "❸\n", + "\n", + "\n", + "\n", + "23->8\n", + "\n", + "\n", + "❸\n", + "\n", + "\n", + "\n", + "24->0\n", + "\n", + "\n", + "❸\n", + "\n", + "\n", + "\n", + "25->3\n", + "\n", + "\n", + "❸\n", + "\n", + "\n", + "\n", + "26->6\n", + "\n", + "\n", + "❸\n", + "\n", + "\n", + "\n", + "27->8\n", + "\n", + "\n", + "❸\n", + "\n", + "\n", + "\n" + ], + "text/plain": [ + "" + ] + }, + "execution_count": 9, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "#Solve the game\n", + "print(\"Found a solution: \", spot.solve_game(game))\n", + "spot.highlight_strategy(game)\n", + "game.show('.g')" + ] + }, + { + "cell_type": "code", + "execution_count": 10, + "metadata": {}, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "minimization lvl 0\n" + ] + }, + { + "data": { + "image/svg+xml": [ + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "t\n", + "[all]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "i0 & i1\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "\n", + "0->2\n", + "\n", + "\n", + "i0 & !i1\n", + "\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", + "\n", + "\n", + "\n", + "0->3\n", + "\n", + "\n", + "!i0 & i1\n", + "\n", + "\n", + "\n", + "4\n", + "\n", + "4\n", + "\n", + "\n", + "\n", + "0->4\n", + "\n", + "\n", + "!i0 & !i1\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "i1 & o0\n", + "\n", + "\n", + "\n", + "5\n", + "\n", + "5\n", + "\n", + "\n", + "\n", + "1->5\n", + "\n", + "\n", + "!i1 & o0\n", + "\n", + "\n", + "\n", + "2->1\n", + "\n", + "\n", + "i1 & !o0\n", + "\n", + "\n", + "\n", + "2->2\n", + "\n", + "\n", + "!i1 & !o0\n", + "\n", + "\n", + "\n", + "3->1\n", + "\n", + "\n", + "i0 & i1 & o0\n", + "\n", + "\n", + "\n", + "3->3\n", + "\n", + "\n", + "!i0 & i1 & o0\n", + "\n", + "\n", + "\n", + "3->5\n", + "\n", + "\n", + "i0 & !i1 & o0\n", + "\n", + "\n", + "\n", + "6\n", + "\n", + "6\n", + "\n", + "\n", + "\n", + "3->6\n", + "\n", + "\n", + "!i0 & !i1 & o0\n", + "\n", + "\n", + "\n", + "4->1\n", + "\n", + "\n", + "i0 & i1 & !o0\n", + "\n", + "\n", + "\n", + "4->2\n", + "\n", + "\n", + "i0 & !i1 & !o0\n", + "\n", + "\n", + "\n", + "4->3\n", + "\n", + "\n", + "!i0 & i1 & !o0\n", + "\n", + "\n", + "\n", + "4->4\n", + "\n", + "\n", + "!i0 & !i1 & !o0\n", + "\n", + "\n", + "\n", + "5->1\n", + "\n", + "\n", + "i1 & !o0\n", + "\n", + "\n", + "\n", + "5->5\n", + "\n", + "\n", + "!i1 & !o0\n", + "\n", + "\n", + "\n", + "6->1\n", + "\n", + "\n", + "i0 & i1 & !o0\n", + "\n", + "\n", + "\n", + "6->3\n", + "\n", + "\n", + "!i0 & i1 & !o0\n", + "\n", + "\n", + "\n", + "6->5\n", + "\n", + "\n", + "i0 & !i1 & !o0\n", + "\n", + "\n", + "\n", + "6->6\n", + "\n", + "\n", + "!i0 & !i1 & !o0\n", + "\n", + "\n", + "\n" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "name": "stdout", + "output_type": "stream", + "text": [ + "minimization lvl 1\n" + ] + }, + { + "data": { + "image/svg+xml": [ + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "t\n", + "[all]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "i0 & i1\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "!i0 & i1\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "\n", + "0->2\n", + "\n", + "\n", + "i0 & !i1\n", + "\n", + "\n", + "\n", + "0->2\n", + "\n", + "\n", + "!i0 & !i1\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "i1 & o0\n", + "\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "!i1 & o0\n", + "\n", + "\n", + "\n", + "2->1\n", + "\n", + "\n", + "i1 & !o0\n", + "\n", + "\n", + "\n", + "2->2\n", + "\n", + "\n", + "!i1 & !o0\n", + "\n", + "\n", + "\n" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "name": "stdout", + "output_type": "stream", + "text": [ + "minimization lvl 2\n" + ] + }, + { + "data": { + "image/svg+xml": [ + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "t\n", + "[all]\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "I->1\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "!i1 & !o0\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + "i1 & !o0\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "!i1 & o0\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "i1 & o0\n", + "\n", + "\n", + "\n" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "name": "stdout", + "output_type": "stream", + "text": [ + "minimization lvl 3\n" + ] + }, + { + "data": { + "image/svg+xml": [ + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "t\n", + "[all]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!i1 & !o0\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "i1 & !o0\n", + "\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + "!i1 & o0\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "i1 & o0\n", + "\n", + "\n", + "\n" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "name": "stdout", + "output_type": "stream", + "text": [ + "minimization lvl 4\n" + ] + }, + { + "data": { + "image/svg+xml": [ + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "t\n", + "[all]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "i1 & o0\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "!i1 & o0\n", + "\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + "i1 & !o0\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "!i1 & !o0\n", + "\n", + "\n", + "\n" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "name": "stdout", + "output_type": "stream", + "text": [ + "minimization lvl 5\n" + ] + }, + { + "data": { + "image/svg+xml": [ + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "t\n", + "[all]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!i1 & !o0\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "i1 & !o0\n", + "\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + "!i1 & o0\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "i1 & o0\n", + "\n", + "\n", + "\n" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + } + ], + "source": [ + "# Create the strategy\n", + "# We have different strategies for minimization:\n", + "# 0 : No minimizaiton\n", + "# 1 : DFA minimization\n", + "# 2 : Inclusion based minimization with output assignement\n", + "# 3 : SAT based exact minimization\n", + "# 4 : First 1 then 3 (exact)\n", + "# 5 : First 2 then 3 (not exact)\n", + "for i in range(6):\n", + " print(\"minimization lvl \", i)\n", + " gi.minimize_lvl = i #Use inclusion with output assignement to minimize the strategy\n", + " strat = spot.create_strategy(game, gi)\n", + " display(strat.show())" + ] + }, { "cell_type": "markdown", "metadata": {}, @@ -675,7 +2634,7 @@ }, { "cell_type": "code", - "execution_count": 8, + "execution_count": 11, "metadata": {}, "outputs": [ { @@ -912,10 +2871,10 @@ "\n" ], "text/plain": [ - " *' at 0x7fbc7c65c660> >" + " *' at 0x7f724981b2d0> >" ] }, - "execution_count": 8, + "execution_count": 11, "metadata": {}, "output_type": "execute_result" } @@ -936,7 +2895,7 @@ }, { "cell_type": "code", - "execution_count": 9, + "execution_count": 12, "metadata": {}, "outputs": [ { @@ -998,7 +2957,7 @@ }, { "cell_type": "code", - "execution_count": 10, + "execution_count": 13, "metadata": {}, "outputs": [ { @@ -1007,7 +2966,7 @@ "True" ] }, - "execution_count": 10, + "execution_count": 13, "metadata": {}, "output_type": "execute_result" } @@ -1018,7 +2977,7 @@ }, { "cell_type": "code", - "execution_count": 11, + "execution_count": 14, "metadata": {}, "outputs": [ { @@ -1255,10 +3214,10 @@ "\n" ], "text/plain": [ - " *' at 0x7fbc7c250240> >" + " *' at 0x7f724981bdb0> >" ] }, - "execution_count": 11, + "execution_count": 14, "metadata": {}, "output_type": "execute_result" } @@ -1293,7 +3252,7 @@ }, { "cell_type": "code", - "execution_count": 12, + "execution_count": 15, "metadata": {}, "outputs": [ { @@ -1336,7 +3295,7 @@ }, { "cell_type": "code", - "execution_count": 13, + "execution_count": 16, "metadata": {}, "outputs": [], "source": [ @@ -1345,7 +3304,7 @@ }, { "cell_type": "code", - "execution_count": 14, + "execution_count": 17, "metadata": {}, "outputs": [ { @@ -1469,7 +3428,7 @@ }, { "cell_type": "code", - "execution_count": 15, + "execution_count": 18, "metadata": {}, "outputs": [ { @@ -1498,7 +3457,7 @@ }, { "cell_type": "code", - "execution_count": 16, + "execution_count": 19, "metadata": {}, "outputs": [ { @@ -1526,7 +3485,7 @@ }, { "cell_type": "code", - "execution_count": 17, + "execution_count": 20, "metadata": {}, "outputs": [ { @@ -1568,7 +3527,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fbc7c1f07b0> >" + " *' at 0x7f72497abfc0> >" ] }, "metadata": {}, diff --git a/tests/python/mealy.py b/tests/python/mealy.py index 382bfc786..ef4c6933e 100644 --- a/tests/python/mealy.py +++ b/tests/python/mealy.py @@ -378,7 +378,7 @@ for (mealy_str, nenv_min) in test_auts: ins = ins & buddy.bdd_ithvar(mealy.register_ap(aap.ap_name())) else: assert("""Aps must start with either "i" or "o".""") - mealy_min_us_s = spot.split_2step(mealy_min_us, ins, outs, False, False) + mealy_min_us_s = spot.split_2step(mealy_min_us, outs, False, False) assert(spot.is_mealy_specialization(mealy, mealy_min_us_s, True)) diff --git a/tests/python/parity.py b/tests/python/parity.py index 96affc116..dfeb24d3d 100644 --- a/tests/python/parity.py +++ b/tests/python/parity.py @@ -124,10 +124,16 @@ except RuntimeError as e: else: report_missing_exception() -spot.set_state_player(a, 1, 1) -assert spot.get_state_players(a) == (False, True, False) -assert spot.get_state_player(a, 0) == 0 -assert spot.get_state_player(a, 1) == 1 +try: + spot.set_state_player(a, 1, True) +except RuntimeError as e: + assert "Can only" in str(e) +else: + report_missing__exception() +spot.set_state_players(a, (False, True, False)) +assert spot.get_state_player(a, 0) == False +assert spot.get_state_player(a, 1) == True +assert spot.get_state_player(a, 2) == False try: spot.set_state_players(a, [True, False, False, False]) @@ -144,7 +150,7 @@ else: report_missing_exception() try: - spot.set_state_player(a, 4, 1) + spot.set_state_player(a, 4, True) except RuntimeError as e: assert "invalid state number" in str(e) else: diff --git a/tests/python/split.py b/tests/python/split.py index d604df855..f20200176 100644 --- a/tests/python/split.py +++ b/tests/python/split.py @@ -43,13 +43,10 @@ def equiv(a, b): def do_split(f, in_list, out_list): aut = spot.translate(f) - inputs = spot.buddy.bddtrue - for a in in_list: - inputs &= spot.buddy.bdd_ithvar(aut.get_dict().varnum(spot.formula(a))) outputs = spot.buddy.bddtrue for a in out_list: outputs &= spot.buddy.bdd_ithvar(aut.get_dict().varnum(spot.formula(a))) - s = spot.split_2step(aut, inputs, outputs, False, False) + s = spot.split_2step(aut, outputs, False, False) return aut, s def str_diff(expect, obtained):