alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity
spot/doc/org/tut40.org
Alexandre Duret-Lutz cdbf830010 * doc/org/tut40.org: Finish a sentence.
2022-01-14 20:29:10 +01:00

388 lines
12 KiB
Org Mode
Raw Permalink Blame History

# -*- 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, state 5 simulates state 1,
and state 4 simulates state 0.
#+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
<<tut40in>>
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
<<build_game>>
aut = spot.automaton("""
<<tut40in>>
""")
g = direct_sim_game(aut, 4, 0)
#+END_SRC
#+NAME: game40unsolved
#+BEGIN_SRC python :exports none :noweb yes
<<game40>>
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
<<game40>>
spot.solve_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)=. The function
=solve_game(g)= used below is a more generic interface that looks at
the acceptance condition of the game to dispatch to the more specific
game solver. These functions returns the player winning in the
initial state. However, as a side-effect they define 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_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
<<game40>>
<<computesim_tut40>>
print(list_simulations(aut, 4, 0))
#+END_SRC
#+RESULTS:
: [(4, 0), (5, 1)]
* 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 <spot/twaalgos/game.hh>
#include <spot/twa/twagraph.hh>
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<std::pair<unsigned, unsigned>>();
game->set_named_prop("product-states", names);
auto owners = new std::vector<bool>();
game->set_named_prop("state-player", owners);
std::map<std::pair<unsigned, unsigned>, unsigned> s_orig_states;
std::map<std::pair<unsigned, unsigned>, unsigned> d_orig_states;
std::vector<unsigned> 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<std::pair<int,int>>
list_simulation(spot::const_twa_graph_ptr aut,
unsigned i, unsigned j)
{
auto g = direct_sim_game(aut, i, j);
spot::solve_game(g);
const std::vector<bool>& winners = spot::get_state_winners(g);
const std::vector<bool>& owners = spot::get_state_players(g);
typedef std::vector<std::pair<unsigned, unsigned>> names_t;
auto names = *g->get_named_prop<names_t>("product-states");
std::vector<std::pair<int,int>> 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 <iostream>
#include <spot/twa/twagraph.hh>
#include <spot/parseaut/public.hh>
<<cppCompute>>
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
Reference in a new issue View git blame Copy permalink