{
"cells": [
{
"cell_type": "code",
"execution_count": 1,
"metadata": {},
"outputs": [],
"source": [
"import spot\n",
"from buddy import bddtrue\n",
"spot.setup()"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"# Support for games\n",
"\n",
"The support for games is currently quite rudimentary, as Spot currently only uses those games in `ltlsynt`.\n",
"\n",
"In essence, agame is just an ω-automaton with a property named `state-player` that stores the player owning each state. The players are named 0 and 1. The player owning a state can decide what the next transition from this state should be. The goal for player 1 is to force the play to be infinite and to satisfy the acceptance condition of the automaton, while the goal for player 0 is to prevent it by either forcing a finite play, or forcing an infinite play that does not satisfy the acceptance condition.\n",
"\n",
"The support is currently restricted to games that use:\n",
"- `t` acceptance: all infinite run are accepting, and player 0 can only win if it manages to force a finite play (this requires reaching states without successors).\n",
"- max odd parity acceptance: player 0 can win if the maximal value seen infinitely often is even"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"# Creating games from scratch\n",
"\n",
"Games can be [created like any automaton](https://spot.lrde.epita.fr/tut22.html). \n",
"Using `set_state_players()` will fix the state owners."
]
},
{
"cell_type": "code",
"execution_count": 2,
"metadata": {},
"outputs": [
{
"data": {
"image/svg+xml": [
"\n",
"\n",
"\n",
"\n",
"\n"
],
"text/plain": [
""
]
},
"execution_count": 2,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"bdict = spot.make_bdd_dict();\n",
"game = spot.make_twa_graph(bdict)\n",
"game.new_states(9)\n",
"for (s, d) in ((0,1), (0, 3), \n",
" (1, 0), (1, 2),\n",
" (2, 1), (2, 5),\n",
" (3, 2), (3, 4), (3, 6),\n",
" (6, 7),\n",
" (7, 6), (7, 8),\n",
" (8, 5)):\n",
" game.new_edge(s, d, bddtrue)\n",
"spot.set_state_players(game, [True, False, True, False, True, True, True, False, False])\n",
"game.show('.g') # Use \"g\" to hide the irrelevant edge labels."
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"The `set_state_players()` function takes a list of owner for each of the states in the automaton. In the output,\n",
"states from player 0 use circles, ellispes, or rectangle with rounded corners (mnemonic: 0 is round) while states from player 1 have a losanse shape (1 has only straight lines). \n",
"\n",
"\n",
"State ownership can also be manipulated by the following functions:"
]
},
{
"cell_type": "code",
"execution_count": 3,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"(True, False, True, False, True, True, True, False, False)"
]
},
"execution_count": 3,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"spot.get_state_players(game)"
]
},
{
"cell_type": "code",
"execution_count": 4,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"1"
]
},
"execution_count": 4,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"spot.get_state_player(game, 4)"
]
},
{
"cell_type": "code",
"execution_count": 5,
"metadata": {},
"outputs": [
{
"data": {
"image/svg+xml": [
"\n",
"\n",
"\n",
"\n",
"\n"
],
"text/plain": [
""
]
},
"execution_count": 5,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"spot.set_state_player(game, 4, False)\n",
"game.show('.g')"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"# Solving a game\n",
"\n",
"Solving a game is done my calling `solve_safety_game()` or `solve_parity_game()`. This will attach two additional vectors into the game automaton: one vector stores the winner of each state, and one vector stores (memory-less) strategy for each state, i.e., the transition that should always be taken by the owner of this state in order to win. \n",
"\n",
"The return value of those function is simply the winner for the initial state."
]
},
{
"cell_type": "code",
"execution_count": 6,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"True"
]
},
"execution_count": 6,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"spot.solve_safety_game(game)"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Calling the `highlight_strategy()` function can be used to decorate the `game` automaton using the winning regions and strategies. Below, green represent the winning region/strategy for player 1 and red those for player 0."
]
},
{
"cell_type": "code",
"execution_count": 7,
"metadata": {},
"outputs": [
{
"data": {
"image/svg+xml": [
"\n",
"\n",
"\n",
"\n",
"\n"
],
"text/plain": [
""
]
},
"execution_count": 7,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"spot.highlight_strategy(game)\n",
"game.show('.g')"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"## Input/Output\n",
"\n",
"An extension of the HOA format makes it possible to store the `state-player` property. This allows us to read the parity game constructed by `ltlsynt` using `spot.automaton()` like any other automaton."
]
},
{
"cell_type": "code",
"execution_count": 8,
"metadata": {},
"outputs": [
{
"data": {
"image/svg+xml": [
"\n",
"\n",
"\n",
"\n",
"\n"
],
"text/plain": [
" *' at 0x7fa3979355d0> >"
]
},
"execution_count": 8,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"game = spot.automaton(\"ltlsynt --ins=a --outs=b -f '!b & GFa <-> Gb' --print-game-hoa |\");\n",
"game"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"In the graphical output, player 0 is represented by circles (or ellipses or rounded rectangles depending on the situations), while player 1's states are diamond shaped. In the case of `ltlsynt`, player 0 plays the role of the environment, and player 1 plays the role of the controler.\n",
"\n",
"In the HOA output, a header `spot-state-player` (or `spot.state-player` in HOA 1.1) lists the owner of each state."
]
},
{
"cell_type": "code",
"execution_count": 9,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"HOA: v1\n",
"States: 11\n",
"Start: 0\n",
"AP: 2 \"b\" \"a\"\n",
"acc-name: parity max odd 3\n",
"Acceptance: 3 Fin(2) & (Inf(1) | Fin(0))\n",
"properties: trans-labels explicit-labels trans-acc colored complete\n",
"properties: deterministic\n",
"spot-state-player: 0 1 1 0 0 0 1 1 1 0 1\n",
"--BODY--\n",
"State: 0\n",
"[!1] 1 {1}\n",
"[1] 2 {1}\n",
"State: 1\n",
"[!0] 3 {1}\n",
"[0] 4 {1}\n",
"State: 2\n",
"[0] 4 {1}\n",
"[!0] 5 {1}\n",
"State: 3\n",
"[!1] 6 {1}\n",
"[1] 7 {2}\n",
"State: 4\n",
"[t] 8 {2}\n",
"State: 5\n",
"[1] 7 {2}\n",
"[!1] 6 {1}\n",
"State: 6\n",
"[t] 3 {1}\n",
"State: 7\n",
"[t] 5 {2}\n",
"State: 8\n",
"[0] 4 {2}\n",
"[!0] 9 {1}\n",
"State: 9\n",
"[t] 10 {1}\n",
"State: 10\n",
"[t] 9 {1}\n",
"--END--\n"
]
}
],
"source": [
"print(game.to_str('hoa'))"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Here is the solution of this particular game."
]
},
{
"cell_type": "code",
"execution_count": 10,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"True"
]
},
"execution_count": 10,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"spot.solve_parity_game(game)"
]
},
{
"cell_type": "code",
"execution_count": 11,
"metadata": {},
"outputs": [
{
"data": {
"image/svg+xml": [
"\n",
"\n",
"\n",
"\n",
"\n"
],
"text/plain": [
" *' at 0x7fa37f087db0> >"
]
},
"execution_count": 11,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"spot.highlight_strategy(game)"
]
},
{
"cell_type": "code",
"execution_count": null,
"metadata": {},
"outputs": [],
"source": []
}
],
"metadata": {
"kernelspec": {
"display_name": "Python 3",
"language": "python",
"name": "python3"
},
"language_info": {
"codemirror_mode": {
"name": "ipython",
"version": 3
},
"file_extension": ".py",
"mimetype": "text/x-python",
"name": "python",
"nbconvert_exporter": "python",
"pygments_lexer": "ipython3",
"version": "3.9.1rc1"
}
},
"nbformat": 4,
"nbformat_minor": 4
}