# -*- coding: utf-8 -*- #+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 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 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()=). 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$. In the following automaton, for instance, XXX #+NAME: tut40in #+BEGIN_SRC hoa HOA: v1 States: 6 Start: 0 AP: 2 "a" "b" Acceptance: 1 Inf(0) --BODY-- State: 0 [1] 1 [1] 2 State: 1 [0&1] 1 State: 2 [0] 3 State: 3 [1] 3 {0} State: 4 [1] 5 State: 5 [0] 5 {0} --END-- #+END_SRC #+NAME: tut40dot #+BEGIN_SRC sh :exports none :noweb yes cat >tut40.hoa <> EOF autfilt --dot='.#' tut40.hoa #+END_SRC #+BEGIN_SRC dot :file tut40in.svg :var txt=tut40dot :exports results $txt #+END_SRC #+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. 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') assert aut.acc().is_generalized_buchi() 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 = [] # 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 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] # 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) # 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) # 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 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. 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 list_simulations(aut, i, j): g = direct_sim_game(aut, i, j) spot.solve_safety_game(g) winners = g.get_state_winners() owners = g.get_state_players() names = g.get_state_names() simulations = [] for i in range(0, g.num_states()): if winners[i] and not owners[i]: simulations.append(tuple(map(int, names[i][1:-1].split(', ')))) return simulations #+END_SRC On our running example, that gives: #+BEGIN_SRC python :results verbatim :exports both :noweb strip-export <> <> print(list_simulations(aut, 4, 0)) #+END_SRC #+RESULTS: * C++ Here is some almost 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 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(spot::make_bdd_dict()); auto names = new std::vector>(); game->set_named_prop("product-states", names); auto owners = new std::vector(); game->set_named_prop("state-player", owners); std::map, unsigned> s_orig_states; std::map, unsigned> d_orig_states; std::vector todo; auto new_state = [&](bool player, unsigned s1, unsigned s2) { 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; }; game->set_init_state(new_state(false, s1, s2)); while (!todo.empty()) { 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 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 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 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