9

{ "cells": [ { "cell_type": "code", "execution_count": 1, "metadata": {}, "outputs": [], "source": [ "import spot\n", "spot.setup()" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "This notebook presents functions that can be used to solve the Reactive Synthesis problem using games.\n", "If you are not familiar with how Spot represent games, please read the `games` notebook first.\n", "\n", "In Reactive Synthesis, the goal is to build an electronic circuit that reacts to some input signals by producing some output signals, under some LTL constraints that tie both input and output. Of course the input signals are not controlable, so only job is to decide what output signal to produce.\n", "\n", "# Reactive synthesis in three steps\n", "\n", "A strategy/control circuit can be derived more conveniently from an LTL/PSL specification.\n", "The process is decomposed in to three steps:\n", "- Creating the game\n", "- Solving the game\n", "- Obtaining the strategy\n", "\n", "Each of these steps is parametrized by a structure called `synthesis_info`. This structure stores some additional data needed to pass fine-tuning options or to store statistics.\n", "\n", "The `ltl_to_game` function takes the LTL specification, and the list of controlable atomic propositions (or output signals). It returns a two-player game, where player 0 plays the input variables (and wants to invalidate the acceptance condition), and player 1 plays the output variables (and wants to satisfy the output condition). The conversion from LTL to parity automata can use one of many algorithms, and can be specified in the `synthesis_info` structure (this works like the `--algo=` option of `ltlsynt`)." ] }, { "cell_type": "code", "execution_count": 2, "metadata": {}, "outputs": [ { "name": "stdout", "output_type": "stream", "text": [ "game has 29 states and 55 edges\n", "output propositions are: o0\n" ] }, { "data": { "image/svg+xml": [ "\n", "\n", "\n", "\n", "\n" ], "text/plain": [ " *' at 0x7f4d60cb1540> >" ] }, "metadata": {}, "output_type": "display_data" } ], "source": [ "si = spot.synthesis_info()\n", "si.s = spot.synthesis_info.algo_LAR # Use LAR algorithm\n", "\n", "game = spot.ltl_to_game(\"G((F(i0) && F(i1))->(G(i1<->(X(o0)))))\", [\"o0\"], si)\n", "print(\"game has\", game.num_states(), \"states and\", game.num_edges(), \"edges\")\n", "print(\"output propositions are:\", \", \".join(spot.get_synthesis_output_aps(game)))\n", "display(game)" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "Solving the game, is done with `solve_game()` as with any game. There is also a version that takes a `synthesis_info` as second argument in case the time it takes has to be recorded. Here passing `si` or not makes no difference." ] }, { "cell_type": "code", "execution_count": 3, "metadata": {}, "outputs": [ { "name": "stdout", "output_type": "stream", "text": [ "Found a solution: True\n" ] }, { "data": { "image/svg+xml": [ "\n", "\n", "\n", "\n", "\n" ], "text/plain": [ "" ] }, "execution_count": 3, "metadata": {}, "output_type": "execute_result" } ], "source": [ "print(\"Found a solution:\", spot.solve_game(game, si))\n", "spot.highlight_strategy(game)\n", "game.show('.g')" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "Once a strategy has been found, it can be extracted as an automaton and simplified using 6 different levels (the default is 2). The output should be interpreted as a mealy automaton, where transition are labeled by combination of input assignments and associated output assignments." ] }, { "cell_type": "code", "execution_count": 4, "metadata": {}, "outputs": [ { "name": "stdout", "output_type": "stream", "text": [ "simplification lvl 0\n" ] }, { "data": { "image/svg+xml": [ "\n", "\n", "\n", "\n", "\n" ], "text/plain": [ "" ] }, "metadata": {}, "output_type": "display_data" }, { "name": "stdout", "output_type": "stream", "text": [ "simplification lvl 1\n" ] }, { "data": { "image/svg+xml": [ "\n", "\n", "\n", "\n", "\n" ], "text/plain": [ "" ] }, "metadata": {}, "output_type": "display_data" }, { "name": "stdout", "output_type": "stream", "text": [ "simplification lvl 2\n" ] }, { "data": { "image/svg+xml": [ "\n", "\n", "\n", "\n", "\n" ], "text/plain": [ "" ] }, "metadata": {}, "output_type": "display_data" }, { "name": "stdout", "output_type": "stream", "text": [ "simplification lvl 3\n" ] }, { "data": { "image/svg+xml": [ "\n", "\n", "\n", "\n", "\n" ], "text/plain": [ "" ] }, "metadata": {}, "output_type": "display_data" }, { "name": "stdout", "output_type": "stream", "text": [ "simplification lvl 4\n" ] }, { "data": { "image/svg+xml": [ "\n", "\n", "\n", "\n", "\n" ], "text/plain": [ "" ] }, "metadata": {}, "output_type": "display_data" }, { "name": "stdout", "output_type": "stream", "text": [ "simplification lvl 5\n" ] }, { "data": { "image/svg+xml": [ "\n", "\n", "\n", "\n", "\n" ], "text/plain": [ "" ] }, "metadata": {}, "output_type": "display_data" } ], "source": [ "# We have different levels of simplification:\n", "# 0 : No simplification\n", "# 1 : bisimulation-based reduction\n", "# 2 : bisimulation-based reduction with output output assignement\n", "# 3 : SAT-based exact minimization\n", "# 4 : First 1 then 3 (exact)\n", "# 5 : First 2 then 3 (not exact)\n", "for i in range(6):\n", " print(\"simplification lvl\", i)\n", " si.minimize_lvl = i\n", " strat = spot.create_strategy(game, si)\n", " display(strat.show())" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "Alternatively, the `apply_strategy` is a more low-level function that can be used to restrict the automaton to the part where player 1 is winning, without simplifying it. It's second argument controls whether pairs of transitions corresponding to each player should be fused back into a single transition. The third argument controls whether the game's acceptance condition should be copied." ] }, { "cell_type": "code", "execution_count": 5, "metadata": {}, "outputs": [ { "data": { "image/svg+xml": [ "\n", "\n", "\n", "\n", "\n" ], "text/plain": [ " *' at 0x7f4d61543bd0> >" ] }, "execution_count": 5, "metadata": {}, "output_type": "execute_result" } ], "source": [ "spot.apply_strategy(game, False, False)" ] }, { "cell_type": "code", "execution_count": 6, "metadata": {}, "outputs": [ { "data": { "image/svg+xml": [ "\n", "\n", "\n", "\n", "\n" ], "text/plain": [ " *' at 0x7f4d61524e10> >" ] }, "execution_count": 6, "metadata": {}, "output_type": "execute_result" } ], "source": [ "spot.apply_strategy(game, True, False)" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "# Converting the strategy to AIGER\n", "\n", "A strategy can be converted to a circuit in the [AIGER format](http://fmv.jku.at/aiger/FORMAT.aiger) using `strategy_to_aig()`. This takes a second argument specifying what type of encoding to use (exactly like `ltlsynt`'s `--aiger=...` option). \n", "\n", "In this case, the circuit is quite simple: `o0` should be the negation of previous value of `i1`. This is done by storing the value of `i1` in a latch. And the value of `i0` can be ignored." ] }, { "cell_type": "code", "execution_count": 7, "metadata": {}, "outputs": [ { "data": { "image/svg+xml": [ "\n", "\n", "\n", "\n", "\n" ], "text/plain": [ " >" ] }, "metadata": {}, "output_type": "display_data" } ], "source": [ "aig = spot.strategy_to_aig(strat, \"isop\")\n", "display(aig)" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "While we are at it, let us mention that you can render those circuits horizontally as follows:" ] }, { "cell_type": "code", "execution_count": 8, "metadata": {}, "outputs": [ { "data": { "image/svg+xml": [ "\n", "\n", "\n", "\n", "\n" ], "text/plain": [ "" ] }, "execution_count": 8, "metadata": {}, "output_type": "execute_result" } ], "source": [ "aig.show('h')" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "# Adding more inputs and outputs by force" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "It can happen that propositions declared as output are ommited in the aig circuit (either because they are not part of the specification, or because they do not appear in the winning strategy). In that case those \n", "values can take arbitrary values.\n", "\n", "For instance so following constraint mention `o1` and `i1`, but those atomic proposition are actually unconstrained (`F(... U x)` can be simplified to `Fx`). Without any indication, the circuit built will ignore those variables:" ] }, { "cell_type": "code", "execution_count": 9, "metadata": {}, "outputs": [ { "data": { "image/svg+xml": [ "\n", "\n", "\n", "\n", "\n" ], "text/plain": [ " *' at 0x7f4d60cb1e10> >" ] }, "metadata": {}, "output_type": "display_data" }, { "data": { "image/svg+xml": [ "\n", "\n", "\n", "\n", "\n" ], "text/plain": [ " >" ] }, "metadata": {}, "output_type": "display_data" } ], "source": [ "game = spot.ltl_to_game(\"i0 <-> F((Go1 -> Fi1) U o0)\", [\"o0\", \"o1\"])\n", "spot.solve_game(game)\n", "spot.highlight_strategy(game)\n", "display(game)\n", "strat = spot.create_strategy(game)\n", "aig = spot.strategy_to_aig(strat, \"isop\")\n", "display(aig)" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "To force the presence of extra variables in the circuit, they can be passed to `strategy_to_aig()`." ] }, { "cell_type": "code", "execution_count": 10, "metadata": {}, "outputs": [ { "data": { "image/svg+xml": [ "\n", "\n", "\n", "\n", "\n" ], "text/plain": [ " >" ] }, "metadata": {}, "output_type": "display_data" } ], "source": [ "display(spot.strategy_to_aig(strat, \"isop\", [\"i0\", \"i1\"], [\"o0\", \"o1\"]))" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "# Reading an AIGER-file\n", "\n", "Note that we do not support the full [AIGER syntax](http://fmv.jku.at/aiger/FORMAT.aiger). Our restrictions corresponds to the conventions used in the type of AIGER file we output:\n", "- Input variables start at index 2 and are consecutively numbered.\n", "- Latch variables start at index (1 + #inputs) * 2 and are consecutively numbered.\n", "- If some inputs or outputs are named in comments, all of them have to be named.\n", "- Gate number $n$ can only connect to latches, inputs, or previously defined gates ($\n", "\n", "\n", "\n", "\n" ], "text/plain": [ " >" ] }, "metadata": {}, "output_type": "display_data" } ], "source": [ "this_aig = spot.aiger_circuit(aag_txt)\n", "display(this_aig)" ] }, { "cell_type": "code", "execution_count": 13, "metadata": {}, "outputs": [ { "name": "stdout", "output_type": "stream", "text": [ "aag 5 2 0 2 3\n", "2\n", "4\n", "10\n", "6\n", "6 2 4\n", "8 3 5\n", "10 7 9\n", "i0 a\n", "i1 b\n", "o0 c\n", "o1 d\n" ] } ], "source": [ "print(this_aig.to_str())" ] }, { "cell_type": "code", "execution_count": 14, "metadata": {}, "outputs": [ { "name": "stdout", "output_type": "stream", "text": [ "((2, 4), (3, 5), (7, 9))\n" ] } ], "source": [ "print(this_aig.gates())" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "An aiger circuit can be transformed into a monitor. This can help for instance to verify that it does not intersect the negation of the specification." ] }, { "cell_type": "code", "execution_count": 15, "metadata": {}, "outputs": [ { "data": { "image/svg+xml": [ "\n", "\n", "\n", "\n", "\n" ], "text/plain": [ " *' at 0x7f4d61543b70> >" ] }, "execution_count": 15, "metadata": {}, "output_type": "execute_result" } ], "source": [ "this_aig.as_automaton()" ] } ], "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.7.3" } }, "nbformat": 4, "nbformat_minor": 5 }