{
"cells": [
{
"cell_type": "code",
"execution_count": 1,
"metadata": {},
"outputs": [],
"source": [
"import spot\n",
"spot.setup()"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"# Support for parity games\n",
"\n",
"The support for parity games is currently quite rudimentary, as Spot currently only uses those games in `ltlsynt`.\n",
"\n",
"In essence, a parity game is just a parity automaton with a property named `state-player` that stores the player owning each state. The players are named 0 and 1.\n",
"\n",
"Player 1 is winning if it has a strategy to satisfy the acceptance condition regardless of player 0's moves.\n",
"Player 0 is winning if it has a strategy to not satisfy the acceptance codition regardless of player 1's moves."
]
},
{
"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": 2,
"metadata": {},
"outputs": [
{
"data": {
"image/svg+xml": [
"\n",
"\n",
"\n",
"\n",
"\n"
],
"text/plain": [
" *' at 0x7fcb3c55f9f0> >"
]
},
"execution_count": 2,
"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": 3,
"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": [
"# Solving games"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"The `parity_game_solve()` function returns a `solved_game` object."
]
},
{
"cell_type": "code",
"execution_count": 4,
"metadata": {},
"outputs": [],
"source": [
"sol = spot.parity_game_solve(game)"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"The solved game can be queried to know if a player is winning when the game starts in some given."
]
},
{
"cell_type": "code",
"execution_count": 5,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"True"
]
},
"execution_count": 5,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"sol.player_winning_at(1, game.get_init_state_number())"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Calling the `highlight_strategy` method will decorate the original game with colors showing the winning region (states from which a player has a strategy to win), and strategy (which transition should be used for each winning state owned by that player) of a given player. Let's paint the strategy of player 1 in green (color 4) for this example:"
]
},
{
"cell_type": "code",
"execution_count": 6,
"metadata": {},
"outputs": [
{
"data": {
"image/svg+xml": [
"\n",
"\n",
"\n",
"\n",
"\n"
],
"text/plain": [
" *' at 0x7fcb3c55a1e0> >"
]
},
"execution_count": 6,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"sol.highlight_strategy(1, 4)"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Because `highlight_strategy` simply decorates the original automaton, we can call it a second time to show that player 0 could win if it had a way to reach the red (color 5) region and play the red strategy."
]
},
{
"cell_type": "code",
"execution_count": 7,
"metadata": {},
"outputs": [
{
"data": {
"image/svg+xml": [
"\n",
"\n",
"\n",
"\n",
"\n"
],
"text/plain": [
" *' at 0x7fcb3c55a900> >"
]
},
"execution_count": 7,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"sol.highlight_strategy(0, 5)"
]
},
{
"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.8.5"
}
},
"nbformat": 4,
"nbformat_minor": 4
}