0

{ "cells": [ { "cell_type": "code", "execution_count": 1, "id": "4f84fa79", "metadata": {}, "outputs": [], "source": [ "import spot\n", "spot.setup()\n", "from spot.jupyter import display_inline" ] }, { "cell_type": "markdown", "id": "4ad017a0", "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 represents 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 controllable, so only job is to decide what output signal to produce.\n", "\n", "# Reactive synthesis in four steps\n", "\n", "A strategy/control circuit can be derived more conveniently from an LTL/PSL specification.\n", "The process is decomposed in three steps:\n", "- Creating the game\n", "- Solving the game\n", "- Simplifying the winning strategy\n", "- Building the circuit from the strategy\n", "\n", "Each of these steps is parameterized 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 controllable 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, "id": "e333be09", "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/html": [ "\n", "\n", "\n", "\n", "\n" ], "text/plain": [ " *' at 0x7f654cfb32a0> >" ] }, "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", "id": "4d030586", "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, "id": "f13ac820", "metadata": {}, "outputs": [ { "name": "stdout", "output_type": "stream", "text": [ "Found a solution: True\n" ] }, { "data": { "text/html": [ "\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", "id": "98aa1402", "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 have the form `(ins)&(outs)` where `ins` and `outs` are Boolean formulas representing possible inputs and outputs (they could be more than just conjunctions of atomic proposition). Mealy machines with this type of labels are called \"separated\" in Spot." ] }, { "cell_type": "code", "execution_count": 4, "id": "4c93add7", "metadata": {}, "outputs": [ { "name": "stdout", "output_type": "stream", "text": [ "simplification lvl 0 : No simplification\n" ] }, { "data": { "image/svg+xml": [ "\n", "\n", "\n", "\n", "\n" ], "text/html": [ "\n", "\n", "\n", "\n", "\n" ], "text/plain": [ " *' at 0x7f654cfb2ca0> >" ] }, "metadata": {}, "output_type": "display_data" }, { "name": "stdout", "output_type": "stream", "text": [ "simplification lvl 1 : bisimulation-based reduction\n" ] }, { "data": { "image/svg+xml": [ "\n", "\n", "\n", "\n", "\n" ], "text/html": [ "\n", "\n", "\n", "\n", "\n" ], "text/plain": [ " *' at 0x7f654cfb3b40> >" ] }, "metadata": {}, "output_type": "display_data" }, { "name": "stdout", "output_type": "stream", "text": [ "simplification lvl 2 : bisimulation-based reduction with output assignement\n" ] }, { "data": { "image/svg+xml": [ "\n", "\n", "\n", "\n", "\n" ], "text/html": [ "\n", "\n", "\n", "\n", "\n" ], "text/plain": [ " *' at 0x7f654cfb3480> >" ] }, "metadata": {}, "output_type": "display_data" }, { "name": "stdout", "output_type": "stream", "text": [ "simplification lvl 3 : SAT-based exact minimization\n" ] }, { "data": { "image/svg+xml": [ "\n", "\n", "\n", "\n", "\n" ], "text/html": [ "\n", "\n", "\n", "\n", "\n" ], "text/plain": [ " *' at 0x7f654cfb2dc0> >" ] }, "metadata": {}, "output_type": "display_data" }, { "name": "stdout", "output_type": "stream", "text": [ "simplification lvl 4 : First 1 then 3 (exact)\n" ] }, { "data": { "image/svg+xml": [ "\n", "\n", "\n", "\n", "\n" ], "text/html": [ "\n", "\n", "\n", "\n", "\n" ], "text/plain": [ " *' at 0x7f654cfb3e40> >" ] }, "metadata": {}, "output_type": "display_data" }, { "name": "stdout", "output_type": "stream", "text": [ "simplification lvl 5 : First 2 then 3 (not exact)\n" ] }, { "data": { "image/svg+xml": [ "\n", "\n", "\n", "\n", "\n" ], "text/html": [ "\n", "\n", "\n", "\n", "\n" ], "text/plain": [ " *' at 0x7f654cfb2ca0> >" ] }, "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 assignement\n", "# 3 : SAT-based exact minimization\n", "# 4 : First 1 then 3 (exact)\n", "# 5 : First 2 then 3 (not exact)\n", "\n", "descr = [\"0 : No simplification\", \n", " \"1 : bisimulation-based reduction\", \n", " \"2 : bisimulation-based reduction with output assignement\",\n", " \"3 : SAT-based exact minimization\",\n", " \"4 : First 1 then 3 (exact)\",\n", " \"5 : First 2 then 3 (not exact)\"]\n", "\n", "\n", "for i in range(6):\n", " print(\"simplification lvl \", descr[i])\n", " si.minimize_lvl = i\n", " mealy = spot.solved_game_to_mealy(game, si)\n", " spot.simplify_mealy_here(mealy, si.minimize_lvl, False)\n", " display(mealy)" ] }, { "cell_type": "markdown", "id": "9d8d52f6", "metadata": {}, "source": [ "If needed, a separated Mealy machine can be turned into game shape using `split_separated_mealy()`, which is more efficient than `split_2step()`." ] }, { "cell_type": "code", "execution_count": 5, "id": "707f4cf6", "metadata": {}, "outputs": [ { "data": { "text/html": [ "

\n", "\n", "\n", "\n", "\n", "

" ], "text/plain": [ "" ] }, "metadata": {}, "output_type": "display_data" } ], "source": [ "display_inline(mealy, spot.split_separated_mealy(mealy), per_row=2)" ] }, { "cell_type": "markdown", "id": "b9e4412e", "metadata": {}, "source": [ "# Converting the separated Mealy machine to AIG\n", "\n", "A separated Mealy machine can be converted to a circuit in the [AIGER format](http://fmv.jku.at/aiger/FORMAT.aiger) using `mealy_machine_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 if `i0` can be ignored." ] }, { "cell_type": "code", "execution_count": 6, "id": "9f344931", "metadata": {}, "outputs": [ { "data": { "image/svg+xml": [ "\n", "\n", "\n", "\n", "\n" ], "text/html": [ "\n", "\n", "\n", "\n", "\n" ], "text/plain": [ " *' at 0x7f654cfb21f0> >" ] }, "metadata": {}, "output_type": "display_data" } ], "source": [ "aig = spot.mealy_machine_to_aig(mealy, \"isop\")\n", "display(aig)" ] }, { "cell_type": "markdown", "id": "92bbe8d0", "metadata": {}, "source": [ "While we are at it, let us mention that you can render those circuits horizontally as follows:" ] }, { "cell_type": "code", "execution_count": 7, "id": "3ae7ce32", "metadata": {}, "outputs": [ { "data": { "text/html": [ "\n", "\n", "\n", "\n", "\n" ], "text/plain": [ "" ] }, "execution_count": 7, "metadata": {}, "output_type": "execute_result" } ], "source": [ "aig.show('h')" ] }, { "cell_type": "markdown", "id": "44fbc0ac", "metadata": {}, "source": [ "To encode the circuit in the AIGER format (ASCII version) use:" ] }, { "cell_type": "code", "execution_count": 8, "id": "566715d5", "metadata": {}, "outputs": [ { "name": "stdout", "output_type": "stream", "text": [ "aag 3 2 1 1 0\n", "2\n", "4\n", "6 3\n", "7\n", "i0 i1\n", "i1 i0\n", "o0 o0\n" ] } ], "source": [ "print(aig.to_str())" ] }, { "cell_type": "markdown", "id": "ef304f36", "metadata": {}, "source": [ "# Adding more inputs and outputs by force" ] }, { "cell_type": "markdown", "id": "5c2b0b78", "metadata": {}, "source": [ "It can happen that propositions declared as output are omitted 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, "id": "874c7df1", "metadata": {}, "outputs": [ { "data": { "image/svg+xml": [ "\n", "\n", "\n", "\n", "\n" ], "text/html": [ "\n", "\n", "\n", "\n", "\n" ], "text/plain": [ " *' at 0x7f654cfc9920> >" ] }, "metadata": {}, "output_type": "display_data" }, { "data": { "image/svg+xml": [ "\n", "\n", "\n", "\n", "\n" ], "text/html": [ "\n", "\n", "\n", "\n", "\n" ], "text/plain": [ " *' at 0x7f654cfb3480> >" ] }, "metadata": {}, "output_type": "display_data" }, { "data": { "text/html": [ "

\n", "\n", "\n", "\n", "\n", "

" ], "text/plain": [ "" ] }, "metadata": {}, "output_type": "display_data" }, { "data": { "image/svg+xml": [ "\n", "\n", "\n", "\n", "\n" ], "text/html": [ "\n", "\n", "\n", "\n", "\n" ], "text/plain": [ " *' at 0x7f654cfb2ca0> >" ] }, "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", "mealy = spot.solved_game_to_mealy(game)\n", "display(mealy)\n", "spot.simplify_mealy_here(mealy, 2, True)\n", "display_inline(mealy, spot.unsplit_mealy(mealy))\n", "aig = spot.mealy_machine_to_aig(mealy, \"isop\")\n", "display(aig)" ] }, { "cell_type": "markdown", "id": "c564dba3", "metadata": {}, "source": [ "To force the presence of extra variables in the circuit, they can be passed to `mealy_machine_to_aig()`." ] }, { "cell_type": "code", "execution_count": 10, "id": "c31a3b38", "metadata": {}, "outputs": [ { "data": { "image/svg+xml": [ "\n", "\n", "\n", "\n", "\n" ], "text/html": [ "\n", "\n", "\n", "\n", "\n" ], "text/plain": [ " *' at 0x7f654cfb3bd0> >" ] }, "metadata": {}, "output_type": "display_data" } ], "source": [ "display(spot.mealy_machine_to_aig(mealy, \"isop\", [\"i0\", \"i1\"], [\"o0\", \"o1\"]))" ] }, { "cell_type": "markdown", "id": "3323fc84", "metadata": {}, "source": [ "# Combining Mealy machines\n", "\n", "It can happen that the complete specification of the controller can be separated into sub-specifications with DISJOINT output propositions, see Finkbeiner et al. Specification Decomposition for Reactive Synthesis.\n", "This results in multiple Mealy machines which have to be converted into one single AIG circuit.\n", "\n", "This can be done in two ways:\n", "\n", "1. Using the function `mealy_machines_to_aig()`, which takes a vector of separated Mealy machines as argument.\n", "2. Combine the mealy machines into one before passing it to `mealy_machine_to aig(). This currently only supports input complete machines of the same type (mealy/separated mealy/split mealy)\n", "\n", "Note that the method version is usually preferable as it is faster.\n", "Also note that in order for this to work, all mealy machines need to share the same `bdd_dict`. This can be ensured by passing a common options structure." ] }, { "cell_type": "code", "execution_count": 11, "id": "5d8e4cdb", "metadata": {}, "outputs": [ { "name": "stdout", "output_type": "stream", "text": [ "Solved games:\n" ] }, { "data": { "text/html": [ "

\n", "\n", "\n", "\n", "\n", "

" ], "text/plain": [ "" ] }, "metadata": {}, "output_type": "display_data" }, { "name": "stdout", "output_type": "stream", "text": [ "Reduced strategies:\n" ] }, { "data": { "text/html": [ "

\n", "\n", "\n", "\n", "\n", "

" ], "text/plain": [ "" ] }, "metadata": {}, "output_type": "display_data" }, { "name": "stdout", "output_type": "stream", "text": [ "Circuit implementing both machines from a vector of machines:\n" ] }, { "data": { "image/svg+xml": [ "\n", "\n", "\n", "\n", "\n" ], "text/html": [ "\n", "\n", "\n", "\n", "\n" ], "text/plain": [ " *' at 0x7f655e8c5200> >" ] }, "metadata": {}, "output_type": "display_data" }, { "name": "stdout", "output_type": "stream", "text": [ "Combining the two machines into one.\n" ] }, { "data": { "image/svg+xml": [ "\n", "\n", "\n", "\n", "\n" ], "text/html": [ "\n", "\n", "\n", "\n", "\n" ], "text/plain": [ " *' at 0x7f654cfb2ca0> >" ] }, "metadata": {}, "output_type": "display_data" }, { "data": { "image/svg+xml": [ "\n", "\n", "\n", "\n", "\n" ], "text/html": [ "\n", "\n", "\n", "\n", "\n" ], "text/plain": [ " *' at 0x7f654cfb2700> >" ] }, "metadata": {}, "output_type": "display_data" } ], "source": [ "g1 = spot.ltl_to_game(\"G((i0 xor i1) <-> o0)\", [\"o0\"], si)\n", "g2 = spot.ltl_to_game(\"G((i0 xor i1) <-> (!o1))\", [\"o1\"], si)\n", "spot.solve_game(g1)\n", "spot.highlight_strategy(g1)\n", "spot.solve_game(g2)\n", "spot.highlight_strategy(g2)\n", "print(\"Solved games:\")\n", "display_inline(g1, g2)\n", "strat1 = spot.solved_game_to_separated_mealy(g1)\n", "strat2 = spot.solved_game_to_separated_mealy(g2)\n", "print(\"Reduced strategies:\")\n", "display_inline(strat1, strat2)\n", "#Method 1\n", "print(\"Circuit implementing both machines from a vector of machines:\")\n", "aig = spot.mealy_machines_to_aig([strat1, strat2], \"isop\")\n", "display(aig)\n", "#Method 2\n", "strat_comb = spot.mealy_product(strat1, strat2)\n", "print(\"Combining the two machines into one.\")\n", "display(strat_comb)\n", "aig_comb = spot.mealy_machine_to_aig(strat_comb, \"isop\")\n", "display(aig_comb)" ] }, { "cell_type": "markdown", "id": "c7a1986f", "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/html": [ "\n", "\n", "\n", "\n", "\n" ], "text/plain": [ " *' at 0x7f654cfc9230> >" ] }, "metadata": {}, "output_type": "display_data" } ], "source": [ "this_aig = spot.aiger_circuit(aag_txt)\n", "display(this_aig)" ] }, { "cell_type": "code", "execution_count": 14, "id": "0ad6c566", "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": 15, "id": "2e1996c1", "metadata": {}, "outputs": [ { "name": "stdout", "output_type": "stream", "text": [ "((2, 4), (3, 5), (7, 9))\n" ] } ], "source": [ "print(this_aig.gates())" ] }, { "cell_type": "markdown", "id": "41a8e042", "metadata": {}, "source": [ "An AIG circuit can be transformed into a monitor/Mealy machine. This can be used for instance to check that it does not intersect the negation of the specification." ] }, { "cell_type": "code", "execution_count": 16, "id": "7399ea38", "metadata": {}, "outputs": [ { "data": { "image/svg+xml": [ "\n", "\n", "\n", "\n", "\n" ], "text/html": [ "\n", "\n", "\n", "\n", "\n" ], "text/plain": [ " *' at 0x7f654cfcb720> >" ] }, "execution_count": 16, "metadata": {}, "output_type": "execute_result" } ], "source": [ "this_aig.as_automaton()" ] }, { "cell_type": "markdown", "id": "7ac06afc", "metadata": {}, "source": [ "Note that the generation of aiger circuits from Mealy machines is flexible and accepts separated Mealy machines\n", "as well as split Mealy machines." ] }, { "cell_type": "code", "execution_count": 17, "id": "bac68923", "metadata": {}, "outputs": [ { "data": { "text/html": [ "

\n", "\n", "\n", "\n", "\n", "

" ], "text/plain": [ "" ] }, "metadata": {}, "output_type": "display_data" }, { "name": "stdout", "output_type": "stream", "text": [ "('o0',)\n", "('o0',)\n" ] } ], "source": [ "strat1_s = spot.split_separated_mealy(strat1)\n", "display_inline(strat1, strat1_s)\n", "print(spot.get_synthesis_output_aps(strat1))\n", "print(spot.get_synthesis_output_aps(strat1_s))" ] }, { "cell_type": "code", "execution_count": 18, "id": "03ceb2a8", "metadata": {}, "outputs": [ { "data": { "text/html": [ "

\n", "\n", "\n", "\n", "\n", "

" ], "text/plain": [ "" ] }, "metadata": {}, "output_type": "display_data" } ], "source": [ "display_inline(spot.mealy_machine_to_aig(strat1, \"isop\"), spot.mealy_machine_to_aig(strat1_s, \"isop\"))" ] } ], "metadata": { "kernelspec": { "display_name": "Python 3 (ipykernel)", "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.11.7" } }, "nbformat": 4, "nbformat_minor": 5 }