{
"cells": [
{
"cell_type": "markdown",
"id": "4d225dd2-8b41-4bb4-9cae-136c314bbcc9",
"metadata": {},
"source": [
"This notebook reproduces the examples shown in our CAV'22 paper, as well as a few more. It was part of the CAV'22 artifact, but has been updated to keep up with recent version of Spot."
]
},
{
"cell_type": "code",
"execution_count": 1,
"id": "a1948c94-e737-4b8b-88b8-00d896c5c928",
"metadata": {},
"outputs": [],
"source": [
"import spot\n",
"from spot.jupyter import display_inline\n",
"from buddy import bdd_ithvar\n",
"spot.setup()"
]
},
{
"cell_type": "markdown",
"id": "c03f8776-c657-4f87-99b5-a56ed1fdcbe3",
"metadata": {},
"source": [
"# Figure 1\n",
"\n",
"Fig. 1 of the paper shows (1) how to convert an LTL formula to an automaton with arbitrary acceptance condition, and (2) how to display the internal representation of the automaton."
]
},
{
"cell_type": "code",
"execution_count": 2,
"id": "d7b6e2d6-7472-4136-8114-ecb03dde1edd",
"metadata": {},
"outputs": [
{
"data": {
"image/svg+xml": [
"\n",
"\n",
"\n",
"\n",
"\n"
],
"text/plain": [
" *' at 0x7fb6a430f5a0> >"
]
},
"execution_count": 2,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"aut = spot.translate('GF(a <-> Xa) & FGb', 'det', 'gen')\n",
"aut"
]
},
{
"cell_type": "code",
"execution_count": 3,
"id": "18248bd4-8d80-4ae7-a466-c347e1ea5ad4",
"metadata": {},
"outputs": [
{
"data": {
"image/svg+xml": [
"\n",
"\n",
"\n",
"\n",
"\n"
],
"text/plain": [
""
]
},
"execution_count": 3,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"aut.show_storage()"
]
},
{
"cell_type": "markdown",
"id": "ef2e2a61-046c-42f0-b0a1-8dc7f1f2b37a",
"metadata": {},
"source": [
"# Figure 2\n",
"\n",
"Fig.2 shows an example of alternating automaton, represented in two different ways, along with its internal representation."
]
},
{
"cell_type": "code",
"execution_count": 4,
"id": "5d2dd179-470c-47c1-b9f2-c5df9f76b2b8",
"metadata": {},
"outputs": [],
"source": [
"# We enter the automaton using the HOA format.\n",
"aut2 = spot.automaton(\"\"\"\n",
"HOA: v1\n",
"States: 5\n",
"Start: 3\n",
"acc-name: co-Buchi\n",
"Acceptance: 1 Fin(0)\n",
"AP: 2 \"a\" \"b\"\n",
"--BODY--\n",
"State: 0 {0} \n",
"[0] 1\n",
"[!0] 2\n",
"State: 1 {0} \n",
"[0&1] 0&1\n",
"State: 2 \n",
"[t] 2 \n",
"State: 3 \n",
"[0] 4&0\n",
"State: 4 \n",
"[t] 3 \n",
"--END--\n",
"\"\"\")"
]
},
{
"cell_type": "code",
"execution_count": 5,
"id": "e1517479-6947-43fd-8369-c4fcdca72e1d",
"metadata": {},
"outputs": [
{
"data": {
"text/html": [
"
\n",
"\n",
"\n",
"\n",
"\n",
"
\n",
"\n",
"\n",
"\n",
"\n",
"
"
],
"text/plain": [
""
]
},
"metadata": {},
"output_type": "display_data"
}
],
"source": [
"display_inline(aut2, aut2.show('.u'), per_row=2)"
]
},
{
"cell_type": "code",
"execution_count": 6,
"id": "ef26e6e8-3206-4e51-9858-33f8d27f915c",
"metadata": {},
"outputs": [
{
"data": {
"image/svg+xml": [
"\n",
"\n",
"\n",
"\n",
"\n"
],
"text/plain": [
""
]
},
"execution_count": 6,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"aut2.show_storage()"
]
},
{
"cell_type": "markdown",
"id": "f4f651b6-974e-4783-a54a-17a280d30782",
"metadata": {},
"source": [
"# Figure 3\n",
"\n",
"Fig. 3 shows an example of game generated by `ltlsynt` from the LTL specification of a reactive controller, and then how this game can be encoded into an And-Inverter-Graph.\n",
"First we retrieve the game generated by `ltlsynt` (any argument passed to `spot.automaton` is interpreted as a command if it ends with a pipe), then we solve it to compute a possible winning strategy. \n",
"\n",
"Player 0 plays from round states and tries to violate the acceptance condition; Player 1 plays from diamond states and tries to satisfy the acceptance condition. Once a game has been solved, the `highlight_strategy` function will decorate the automaton with winning region and computed strategies for player 0 and 1 in red and green respectively. Therefore this game is winning for player 1 from the initial state.\n",
"\n",
"Compared to the paper, the production of parity automata in `ltlsynt` has been improved, and it generates a Büchi game instead (but Büchi can be seen one case of parity)."
]
},
{
"cell_type": "code",
"execution_count": 7,
"id": "ac90284d-2493-428b-9db7-cc7aa63384cb",
"metadata": {},
"outputs": [
{
"data": {
"image/svg+xml": [
"\n",
"\n",
"\n",
"\n",
"\n"
],
"text/plain": [
" *' at 0x7fb6a430f300> >"
]
},
"execution_count": 7,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"game = spot.automaton(\"ltlsynt --outs=b -f 'F(a & Xa) <-> Fb' --print-game-hoa |\")\n",
"spot.solve_game(game)\n",
"spot.highlight_strategy(game)\n",
"game"
]
},
{
"cell_type": "markdown",
"id": "d8b3ad5a-fef2-498b-8fd3-2d3940dacbf5",
"metadata": {},
"source": [
"The `solved_game_to_mealy()` shown in the paper does not always produce the same type of output, so it is\n",
"better to explicitly call `solved_game_to_split_mealy()` or `solved_game_to_separated_mealy()` depending on the type of output one need. We also show how to use the `reduce_mealy()` method to simplify one."
]
},
{
"cell_type": "code",
"execution_count": 8,
"id": "39156f1a-945c-46db-bac2-01565d17b82e",
"metadata": {},
"outputs": [
{
"data": {
"text/html": [
"