diff --git a/NEWS b/NEWS index 1f2303187..c0d4ef704 100644 --- a/NEWS +++ b/NEWS @@ -284,8 +284,11 @@ New in spot 2.9.8.dev (not yet released) Python: - - Bindings for functions related to games and aig-circuits. - See https://spot.lrde.epita.fr/ipynb/games.html for examples. + - Bindings for functions related to games. + See https://spot.lrde.epita.fr/ipynb/games.html and + https://spot.lrde.epita.fr/tut40.html for examples. + + - Bindings for functions related to syntethis and aig-circuits. - spot::twa::prop_set was previously abstent from the Python bindings, making it impossible to call make_twa_graph() for copying diff --git a/doc/org/tut.org b/doc/org/tut.org index d3bd313c8..052cfc985 100644 --- a/doc/org/tut.org +++ b/doc/org/tut.org @@ -37,6 +37,7 @@ three interfaces supported by Spot: shell commands, Python, or C++. - [[file:tut22.org][Creating an automaton by adding states and transitions]] - [[file:tut23.org][Creating an alternating automaton by adding states and transitions]] - [[file:tut24.org][Iterating over alternating automata]] +- [[file:tut40.org][Creating a solving a safety game to decide direct simulation]] - [[file:tut52.org][Creating an explicit Kripke structure]] - [[file:tut90.org][Using the =bdd_dict= to associate atomic proposition to BDD variables, or allocate anonymous BDD variables (advanced)]] diff --git a/doc/org/tut40.org b/doc/org/tut40.org index dc887e7fd..cc94a6ce9 100644 --- a/doc/org/tut40.org +++ b/doc/org/tut40.org @@ -1,25 +1,31 @@ # -*- coding: utf-8 -*- -#+TITLE: Using games to compute simulation -#+DESCRIPTION: Code example for iterating over ω-automata in Spot +#+TITLE: Using games to check a simulation +#+DESCRIPTION: Code example for using games in Spot #+INCLUDE: setup.org #+HTML_LINK_UP: tut.html #+PROPERTY: header-args:sh :results verbatim :exports both #+PROPERTY: header-args:python :results output :exports both #+PROPERTY: header-args:C+++ :results verbatim :exports both -This example demonstrates how to find the simulations between states using -games in C++ and python. This algorithm is describe in Fair Simulation -Relations, Parity Games, and State Space Reduction for Büchi Automata by R. -Schuller Borbely, Kousha Etessami and Thomas Wilke. +This example demonstrates how to use Spot's game interface to compute +a simulation-relation between the states of an automaton. This +algorithm is inspired from [[https://homepages.inf.ed.ac.uk/kousha/siam_j2005.pdf][Fair Simulation Relations, Parity Games, +and State Space Reduction for Büchi Automata (Kousha Etessami and +Thomas Wilke, and Rebecca A. Schuller)]]. -The simulation based reduction (spot.simuation() and spot.reduce_direct_sim()) -does not use this method as is it slower. +The code below is intended for demonstration of how to construct and +use games. Spot contains some other (and faster) implementation to +reduce an automaton using simulation-based reductions (see +=spot.simulation()= and =spot.reduce_direct_sim()=). -When all the moves are in the game, we check if the spoiler has a winning -strategy from a pair of state. If yes, there is simulation otherwise there are -no. +Let us start with a definition of simulation for transition-based +generalized-Büchi automata: A state $s'$ simulates $s$ iff for any +transition $(s,c,a,d)$ leaving $s$, there exists a transition +$(s',c',a',d')$ leaving $s'$ with a condition $c'$ that covers $c$, +some colors $a'\supseteq a$ that covers the colors of $a$ other +transition, and reaching a destination state $d'$ that simulates $d$. -We will compute the simulation between 4 and 0 in the following automaton. +In the following automaton, for instance, XXX #+NAME: tut40in #+BEGIN_SRC hoa @@ -27,23 +33,21 @@ HOA: v1 States: 6 Start: 0 AP: 2 "a" "b" -acc-name: co-Buchi -Acceptance: 1 Fin(0) -properties: trans-labels explicit-labels state-acc very-weak +Acceptance: 1 Inf(0) --BODY-- State: 0 [1] 1 [1] 2 -State: 1 {0} +State: 1 [0&1] 1 State: 2 [0] 3 State: 3 -[1] 3 +[1] 3 {0} State: 4 [1] 5 State: 5 -[0] 5 +[0] 5 {0} --END-- #+END_SRC @@ -52,39 +56,9 @@ State: 5 cat >tut40.hoa <> EOF -autfilt --dot tut40.hoa +autfilt --dot='.#' tut40.hoa #+END_SRC -#+RESULTS: tut40dot -#+begin_example -digraph "" { - rankdir=LR - label=<
[co-Büchi]> - labelloc="t" - node [shape="circle"] - node [style="filled", fillcolor="#ffffa0"] - fontname="Lato" - node [fontname="Lato"] - edge [fontname="Lato"] - node[fontsize=12] fontsize=12 stylesheet="spot.css" edge[arrowhead=vee, arrowsize=.7, fontsize=12] - I [label="", style=invis, width=0] - I -> 0 - 0 [label=<0>] - 0 -> 1 [label=] - 0 -> 2 [label=] - 1 [label=<1>, peripheries=2] - 1 -> 1 [label=] - 2 [label=<2>] - 2 -> 3 [label=] - 3 [label=<3>] - 3 -> 3 [label=] - 4 [label=<4>] - 4 -> 5 [label=] - 5 [label=<5>] - 5 -> 5 [label=] -} -#+end_example - #+BEGIN_SRC dot :file tut40in.svg :var txt=tut40dot :exports results $txt #+END_SRC @@ -92,122 +66,175 @@ digraph "" { #+RESULTS: [[file:tut40in.svg]] + +Whether two states are in simulation can be decided as a game between +two players. If the game is in state $(q,q')$, spoiler (player 0) +first selects a transition from state $q$, and duplicator (player 1) +then has to chose a compatible transition from state $q'$. Duplicator +of course wins if it always manages to select compatibles transitions, +otherwise spoiler wins. + +The game arena can be encoded by associating each state to a pair of +integers. States owned by player 0 (rounded rectangles) are pairs +$(q,q')$ denoting the position of each player. States owned by player +1 (diamonds) are pairs $(e,q')$ where $e$ is the number of the +edges that player 0 just took (those numbers appears as =#1=, =#2=, +etc. in the previous picture). + +Here is how the game arena look like starting from $(q,q')=(4,0)$: + +#+NAME: game40 +#+BEGIN_SRC python :exports results :noweb yes +<> +aut = spot.automaton(""" +<> +""") +g = direct_sim_game(aut, 4, 0) +#+END_SRC + +#+NAME: game40unsolved +#+BEGIN_SRC python :exports none :noweb yes +<> +print(g.to_str('dot', '.g')) +#+END_SRC + +#+BEGIN_SRC dot :file tut40gameunsolved.svg :var txt=game40unsolved :exports results + $txt +#+END_SRC + +#+RESULTS: +[[file:tut40gameunsolved.svg]] + +In this game, player 1, wins if it has a strategy to force the game to +satisfy the acceptance condition. Here the acceptance condition is +just true, so any infinite play will satisfy it. + +Clearly, it is enough for player 1 to always go to $(5,1)$ when +possible. If Spot is used to solve this game, the result can be +presented as follows, where greens states represents states from which +player 1 has a winning strategy, and red states are states from which +player 0 has a winning strategy. The highlighted arrows show those +strategies. + +#+NAME: game40solved +#+BEGIN_SRC python :exports none :noweb yes +<> +spot.solve_safety_game(g) +spot.highlight_strategy(g) +print(g.to_str('dot', '.g')) +#+END_SRC + +#+BEGIN_SRC dot :file tut40gamesolved.svg :var txt=game40solved :exports results +$txt +#+END_SRC + +#+RESULTS: +[[file:tut40gamesolved.svg]] + + +Since player 1 is winning from state $(4,0)$, we know that state 4 +simulates state 0. Also since player 1 would also win from state +$(5,1)$, we can tell that state 5 simulates state 1. We also learn +that state 5 does not simulates states 2 and 3. We could build other +games, or add more state to this game, to learn about other pairs of +states. + * Python +We now look at how to create such a game in Python. - - - - -First a need to create a game. The game is build by alternating the possible -moves of the two players: the spoiler (even) and the duplicator (odd). The -spoiler starts from its state and chose a transition and move to the -destination. Then, the duplicator search for a transition from its state with a -compatible condition and acceptance. +Essentially, a game in Spot is just an automaton equiped with a +special property to indicate the owner of each states. So it can be +created using the usual interface: #+NAME: build_game #+BEGIN_SRC python :exports code -import spot -from spot import buddy -def direct_sim_game(aut, s1, s2): - if s1 >= aut.num_states() or s2 >= aut.num_states(): - raise ValueError('invalid state number') + import spot + from spot import buddy - game = spot.make_twa_graph(aut.get_dict()) + def direct_sim_game(aut, s1, s2): + if s1 >= aut.num_states() or s2 >= aut.num_states(): + raise ValueError('invalid state number') + assert aut.acc().is_generalized_buchi() - # The names are a pair of int. If even owns the state, the first integer - # is the number of the edge that spoiler has taken during this turn (so - # we have the current position of the spoiler (the destination of the - # edge), the condition and acceptance that duplicator must find). If - # it is an odd state, the first integer is the state where the spoiler - # is. In either case, the second is always the duplicator's state. - names = [] - owners = [] + game = spot.make_twa_graph() + # The names of the states are pairs of integers + # (q,q') for states owned by player 0 + # (e,q') for states owned by player 1 + # These arrays are indiced by state numbers. + names = [] + owners = [] + # The reverse assotiation (x,y) -> state number + # must be kept for each player, since (x,y) can mean two different thing. + s_orig_states = {} + d_orig_states = {} + # a list of player 0 states to process + todo = [] - # Keep the game's state from its name. We need two maps as two states can - # have the same name (but not the same owner). For example (0, 1) can - # describe a spoiler state (the edge 0, the state 1) and a duplicator - # state (the states 0 and 1). - s_orig_states = {} - d_orig_states = {} - - todo = [] - - # Create the state (i, j) for a player if it does not exist yet and - # returns its state's number in the game. - def get_and_create_game_state(player, i, j): - orig_state = s_orig_states if player else d_orig_states - - if not (i, j) in orig_state: - s = game.new_state() - - names.append((i, j)) - owners.append(player) - orig_state[(i, j)] = s - - # If it is the duplicator turn and the state does not exist - # yet, we need to process it. - if not player: - todo.append(s) - - return s - else: + # Create the state (i, j) for a player if it does not exist yet and + # returns the state's number in the game. + def get_game_state(player, i, j): + orig_state = s_orig_states if player else d_orig_states + if (i, j) in orig_state: return orig_state[(i, j)] + s = game.new_state() + names.append((i, j)) + owners.append(player) + orig_state[(i, j)] = s + # If it is a new state for Player 0 (spoiler) + # we need to process it. + if not player: + todo.append(s) + return s - get_and_create_game_state(False, s1, s2); - (all_inf, _) = aut.get_acceptance().used_inf_fin_sets() + game.set_init_state(get_game_state(False, s1, s2)) + while todo: + cur = todo.pop() + # todo contains only player 0's states, named with pairs + # of states. + (s_src, d_src) = names[cur] - while todo: - cur = todo.pop() - (s_src, d_src) = names[cur] + # Player 0 is allowed to pick edge from s_src: + for s_edge in aut.out(s_src): + edge_idx = aut.edge_number(s_edge) + st2 = get_game_state(True, edge_idx, d_src) + # label the edge with true, because it's an automaton, + # but we do not use this label for the game. + game.new_edge(cur, st2, buddy.bddtrue) - # Spoiler starts by picking an edge from s_src. If it does not exist - # yet, we add a new edge in the game from (s_src,d_src) to - # (edge_idx,d_src). - for s_edge in aut.out(s_src): - edge_idx = aut.edge_number(s_edge) - cur2 = get_and_create_game_state(True, edge_idx, d_src) + # Player 1 then try to find an edge with the + # a compatible same condition and colors, from d_src. + for d_edge in aut.out(d_src): + if (buddy.bdd_implies(d_edge.cond, s_edge.cond) \ + and d_edge.acc.subset(s_edge.acc)): + st3 = get_game_state(False, s_edge.dst, d_edge.dst) + game.new_edge(st2, st3, buddy.bddtrue) - game.new_edge(cur, cur2, buddy.bddtrue) - - # Duplicator try to find an edge with the same condition from d_src. - # If it does not exist yet, it adds a new edge from - # (s_edge.dst,d_src) to (s_edge.dst, d_edge.dst). - for d_edge in aut.out(d_src): - if buddy.bdd_implies(d_edge.cond, s_edge.cond) \ - and (s_edge.acc ^ all_inf).subset(d_edge.acc ^ all_inf): - - cur3 = get_and_create_game_state(False, s_edge.dst, d_edge.dst) - game.new_edge(cur2, cur3, buddy.bddtrue) - - spot.set_state_players(game, owners) - names = [s for s in map(str, names)] - game.set_state_names(names) - - return game + # Name each state with a string, just so we can read the pairs + # when the automaton is displayed. + game.set_state_names(list(map(str, names))) + # This only line is actually what turns an automaton into a game! + game.set_state_players(owners) + return game #+END_SRC -Then we solve it. This game is a safety game, the odd player tries to block -the even player into a dead end. Even win if it has a winning strategy, aka -there is no dead end in the game. +To solve a safety game =g= that has been created by the above method, +it is enough to just call =solve_safety_game(g)=. This function +returns the player winning in the initial state. However, as a +side-effect it defines additional automaton properties that indicate +the winner of each state, and the associated strategy. -#+BEGIN_SRC :export code -spot.solve_safety_game(g) -#+END_SRC - -Next, we get the winners for each state. We only check the even's state as it -is the only ones that describe states pairs (the odd's ones describe the -edge taken and a state). If odd wins from this state, then the first state -simulates the second. +Therefore to list all simulation pairs we learned from a game starting +in state $(i,j)$, we could proceed as follow: #+NAME: computesim_tut40 #+BEGIN_SRC python :exports code -def compute_simulation(aut, i, j): +def list_simulations(aut, i, j): g = direct_sim_game(aut, i, j) spot.solve_safety_game(g) - winners = spot.get_state_winners(g) - owners = spot.get_state_players(g) + winners = g.get_state_winners() + owners = g.get_state_players() names = g.get_state_names() simulations = [] @@ -218,220 +245,139 @@ def compute_simulation(aut, i, j): return simulations #+END_SRC -#+RESULTS: computesim_tut40 +On our running example, that gives: -Compute all simulations found when checking if 4 simulates 0. - -#+BEGIN_SRC python :exports code -print(compute_simulation(aut, 4, 0)) +#+BEGIN_SRC python :results verbatim :exports both :noweb strip-export + <> + <> + print(list_simulations(aut, 4, 0)) #+END_SRC #+RESULTS: -#+BEGIN_SRC python :exports results :results verbatim :noweb yes -import spot -from spot import buddy - -aut = spot.automaton(''' -<> -''') - -<> - -<> - -print(compute_simulation(aut, 4, 0)) - -#+END_SRC - -#+RESULTS: -: [(4, 0), (5, 1)] - * C++ +Here is some almost equivalent code in C++. -The equivalent code in C++: +Here instead of naming states with strings, we use the "product-states" +property, which is usually used to display pair of integers that come from a +product of automata. #+NAME: cppCompute #+BEGIN_SRC C++ :exports code -#include -#include + #include + #include -spot::twa_graph_ptr direct_sim_game(spot::const_twa_graph_ptr aut, - unsigned s1, unsigned s2) -{ - if (s1 >= aut->num_states() || s2 >= aut->num_states()) - throw std::runtime_error("direct_sim_game(): invalid state number"); - - auto game = spot::make_twa_graph(aut->get_dict()); - game->copy_ap_of(aut); - - auto names = new std::vector>(); - game->set_named_prop("product-states", names); - names->reserve(aut->num_states()); - - auto owners = new std::vector(); - game->set_named_prop("state-player", owners); - owners->reserve(aut->num_states()); - - std::map, unsigned> s_orig_states; - std::map, unsigned> d_orig_states; - std::vector todo; - todo.reserve(aut->num_states()); - auto& g = game->get_graph(); - - auto all_inf = aut->get_acceptance().used_inf_fin_sets().first; - - auto new_state = [&](bool player, unsigned s1, unsigned s2) + spot::twa_graph_ptr direct_sim_game(spot::const_twa_graph_ptr aut, + unsigned s1, unsigned s2) { - unsigned s; - auto& m = player ? s_orig_states : d_orig_states; + if (s1 >= aut->num_states() || s2 >= aut->num_states()) + throw std::runtime_error("direct_sim_game(): invalid state number"); - auto it = std::find_if(m.begin(), m.end(), [s1, s2](auto elm) - { return s1 == elm.first.first && s2 == elm.first.second; }); + auto game = spot::make_twa_graph(spot::make_bdd_dict()); - if (it == m.end()) - { - s = game->new_state(); - names->emplace_back(s1, s2); - owners->push_back(player); - m.insert({{s1, s2}, s}); + auto names = new std::vector>(); + game->set_named_prop("product-states", names); - if (!player) - todo.push_back(s); - } - else - { - s = it->second; - } + auto owners = new std::vector(); + game->set_named_prop("state-player", owners); - return s; - }; + std::map, unsigned> s_orig_states; + std::map, unsigned> d_orig_states; + std::vector todo; - new_state(false, s1, s2); - - while (!todo.empty()) + auto new_state = [&](bool player, unsigned s1, unsigned s2) { - unsigned cur = todo.back(); - unsigned s_src = (*names)[cur].first; - unsigned d_src = (*names)[cur].second; - todo.pop_back(); + auto& m = player ? s_orig_states : d_orig_states; + if (auto it = m.find({s1, s2}); it != m.end()) + return it->second; + unsigned s = game->new_state(); + names->emplace_back(s1, s2); + owners->push_back(player); + m.insert({{s1, s2}, s}); + if (!player) + todo.push_back(s); + return s; + }; - for (const auto& s_edge : aut->out(s_src)) - { - unsigned edge_idx = g.index_of_edge(s_edge); - unsigned cur2 = new_state(true, edge_idx, d_src); - - game->new_edge(cur, cur2, bddtrue); - - for (const auto& d_edge : aut->out(d_src)) - { - if (bdd_implies(d_edge.cond, s_edge.cond) - && (s_edge.acc ^ all_inf).subset(d_edge.acc ^ all_inf)) - { - unsigned cur3 = new_state(false, s_edge.dst, d_edge.dst); - game->new_edge(cur2, cur3, bddtrue); - } - } - } - } - - return game; -} - -bool compute_simulation(spot::const_twa_graph_ptr aut, - unsigned i, unsigned j, - std::vector& can_sim) -{ - auto g = direct_sim_game(aut, i, j); - bool i_simulates_j = spot::solve_safety_game(g); - - std::vector winners = spot::get_state_winners(g); - std::vector owners = spot::get_state_players(g); - - typedef std::vector> names_t; - auto names = *g->get_named_prop("product-states"); - - unsigned n = g->num_states(); - unsigned n_aut = aut->num_states(); - - for (unsigned i = 0; i < n; ++i) - if (winners[i] && !owners[i]) + game->set_init_state(new_state(false, s1, s2)); + while (!todo.empty()) { - auto [u, v] = names[i]; - can_sim[u * n_aut + v] = true; + unsigned cur = todo.back(); + todo.pop_back(); + auto [s_src, d_src] = (*names)[cur]; + + for (const auto& s_edge : aut->out(s_src)) + { + unsigned edge_idx = aut->edge_number(s_edge); + unsigned st2 = new_state(true, edge_idx, d_src); + game->new_edge(cur, st2, bddtrue); + for (const auto& d_edge : aut->out(d_src)) + if (bdd_implies(d_edge.cond, s_edge.cond) + && d_edge.acc.subset(s_edge.acc)) + { + unsigned st3 = new_state(false, s_edge.dst, d_edge.dst); + game->new_edge(st2, st3, bddtrue); + } + } } -return i_simulates_j; -} + return game; + } + + std::vector> + list_simulation(spot::const_twa_graph_ptr aut, + unsigned i, unsigned j) + { + auto g = direct_sim_game(aut, i, j); + spot::solve_safety_game(g); + + const std::vector& winners = spot::get_state_winners(g); + const std::vector& owners = spot::get_state_players(g); + + typedef std::vector> names_t; + auto names = *g->get_named_prop("product-states"); + + std::vector> res; + + unsigned n = g->num_states(); + for (unsigned i = 0; i < n; ++i) + if (winners[i] && !owners[i]) + res.emplace_back(names[i]); + return res; + } #+END_SRC -#+RESULTS: cppCompute - -Computes and print the simulations found when checking if 4 simulates 0. - -#+NAME: cppCallCompute -#+BEGIN_SRC text :exports none - unsigned n = aut->num_states(); - std::vector can_sim(n*n); - - compute_simulation(aut, 4, 0, can_sim); - - for (unsigned i = 0; i < n; ++i) - for (unsigned j = 0; j < n; ++j) - if (can_sim[i * n + j]) - std::cout << i << " simulates " << j << '\n'; -#+END_SRC - -#+BEGIN_SRC C++ :exports code :noweb yes -<> -#+END_SRC - -#+RESULTS: cppCallCompute +Now to execute the above code on our example automaton, we just +need to read the automaton from a file. #+NAME: finalcpp -#+BEGIN_SRC C++ :results verbatim :exports results :noweb yes -#include -#include - -<> - -int main() -{ - spot::bdd_dict_ptr dict = spot::make_bdd_dict(); - spot::twa_graph_ptr aut = make_twa_graph(dict); - - bdd p1 = bdd_ithvar(aut->register_ap("p1")); - bdd p2 = bdd_ithvar(aut->register_ap("p2")); - - aut->set_acceptance(1, "t"); - aut->prop_state_acc(true); - - aut->new_states(6); - aut->set_init_state(0U); - - aut->new_edge(0, 1, p2); - aut->new_edge(1, 1, p1 & p2, {0}); - aut->new_edge(0, 2, p2); - aut->new_edge(2, 3, p1); - aut->new_edge(3, 3, p2); - aut->new_edge(4, 5, p2); - aut->new_edge(5, 5, p1); - - unsigned n = aut->num_states(); - std::vector can_sim(n*n); - - compute_simulation(aut, 4, 0, can_sim); - - for (unsigned i = 0; i < n; ++i) - for (unsigned j = 0; j < n; ++j) - if (can_sim[i * n + j]) - std::cout << i << " simulates " << j << '\n'; - - return 0; -} +#+BEGIN_SRC C++ :results verbatim :exports both :noweb strip-export + #include + #include + #include + <> + int main() + { + spot::parsed_aut_ptr pa = parse_aut("tut40.hoa", spot::make_bdd_dict()); + if (pa->format_errors(std::cerr)) + return 1; + if (pa->aborted) + { + std::cerr << "--ABORT-- read\n"; + return 1; + } + for (auto [i,j]: list_simulation(pa->aut, 4, 0)) + std::cout << i << " simulates " << j << '\n'; + return 0; + } #+END_SRC #+RESULTS: finalcpp : 4 simulates 0 : 5 simulates 1 + + +#+BEGIN_SRC sh :results silent :exports results +rm -f tut40.hoa +#+END_SRC diff --git a/python/spot/__init__.py b/python/spot/__init__.py index c8afe78ca..a351e9c54 100644 --- a/python/spot/__init__.py +++ b/python/spot/__init__.py @@ -1031,7 +1031,10 @@ def _add_twa_graph(meth, name=None): for meth in ('scc_filter', 'scc_filter_states', 'is_deterministic', 'is_unambiguous', - 'contains'): + 'contains', 'get_strategy', + 'set_state_players', 'get_state_players', + 'set_state_player', 'get_state_player', + 'get_state_winners', 'get_state_winner'): _add_twa_graph(meth) _add_twa_graph('are_equivalent', 'equivalent_to')