alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

python: fix support for std::vector<const_twa_graph_ptr>

Browse source 
* spot/twaalgos/aiger.hh, spot/twaalgos/aiger.cc: Fix prototypes, as
well as several error messages.
* python/spot/impl.i: Implement an ad-hoc conversion for
std::vector<const_twa_graph_ptr>.
* tests/python/synthesis.ipynb: Use it to simplify the example.
Adjust some comments.
This commit is contained in:
Alexandre Duret-Lutz 2021-11-12 22:38:37 +01:00
parent 98ebbea17e
commit 6555af1f44
4 changed files with 112 additions and 235 deletions
Download patch file Download diff file Expand all files Collapse all files

274
tests/python/synthesis.ipynb
View file

@ -3,6 +3,7 @@
{
"cell_type": "code",
"execution_count": 1,
"id": "452c00ae",
"metadata": {},
"outputs": [],
"source": [
@ -13,6 +14,7 @@
},
{
"cell_type": "markdown",
"id": "7545ab74",
"metadata": {},
"source": [
"This notebook presents functions that can be used to solve the Reactive Synthesis problem using games.\n",
@ -20,13 +22,14 @@
"\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",
"# 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 to three steps:\n",
"The process is decomposed in three steps:\n",
"- Creating the game\n",
"- Solving the game\n",
"- Obtaining the strategy\n",
"- Simplifying the winnning strategy\n",
"- Building the circuit from 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",
@ -36,6 +39,7 @@
{
"cell_type": "code",
"execution_count": 2,
"id": "fb49e681",
"metadata": {},
"outputs": [
{
@ -694,7 +698,7 @@
"</svg>\n"
],
"text/plain": [
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f494811f630> >"
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fe9bc79b6f0> >"
]
},
"metadata": {},
@ -713,6 +717,7 @@
},
{
"cell_type": "markdown",
"id": "3797307f",
"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."
@ -721,6 +726,7 @@
{
"cell_type": "code",
"execution_count": 3,
"id": "62fb169f",
"metadata": {},
"outputs": [
{
@ -1339,14 +1345,16 @@
},
{
"cell_type": "markdown",
"id": "d5a53d3f",
"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."
"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 possibles 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": "cdf8f5f1",
"metadata": {},
"outputs": [
{
@ -2344,22 +2352,22 @@
},
{
"cell_type": "markdown",
"id": "511093c3",
"metadata": {},
"source": [
"The machines returned by 'solved_game_to_separated_mealy' are (obviously) separated.\n",
"If we need a split mealy machine, we can call the dedicated function, which is more efficient\n",
"than the general 'split_2step'."
"If needed, a separated Mealy machine can be turned into game shape using `split_sepearated_mealy()`, which is more efficient than `split_2step()`."
]
},
{
"cell_type": "code",
"execution_count": 5,
"id": "cc977286",
"metadata": {},
"outputs": [
{
"data": {
"text/html": [
"<div style='vertical-align:text-top;display:inline-block;'><?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n",
"<div style='vertical-align:text-top;display:inline-block;width:50%;'><?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n",
"<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n",
" \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n",
"<!-- Generated by graphviz version 2.43.0 (0)\n",
@ -2478,7 +2486,7 @@
"</g>\n",
"</g>\n",
"</svg>\n",
"</div><div style='vertical-align:text-top;display:inline-block;'><?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n",
"</div><div style='vertical-align:text-top;display:inline-block;width:50%;'><?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n",
"<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n",
" \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n",
"<!-- Generated by graphviz version 2.43.0 (0)\n",
@ -2630,16 +2638,17 @@
}
],
"source": [
"display_inline(mealy.show(), spot.split_separated_mealy(mealy).show())"
"display_inline(mealy, spot.split_separated_mealy(mealy), per_row=2)"
]
},
{
"cell_type": "markdown",
"id": "aa6fe484",
"metadata": {},
"source": [
"# Converting the separated mealy machine to AIGER\n",
"\n",
"A separated mealy machine 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",
"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."
]
@ -2647,6 +2656,7 @@
{
"cell_type": "code",
"execution_count": 6,
"id": "78261ec4",
"metadata": {},
"outputs": [
{
@ -2708,7 +2718,7 @@
"</svg>\n"
],
"text/plain": [
"<spot.aig; proxy of <Swig Object of type 'spot::aig_ptr *' at 0x7f494811f9f0> >"
"<spot.aig; proxy of <Swig Object of type 'spot::aig_ptr *' at 0x7fe9bc79ba50> >"
]
},
"metadata": {},
@ -2722,6 +2732,7 @@
},
{
"cell_type": "markdown",
"id": "f95dc6b7",
"metadata": {},
"source": [
"While we are at it, let us mention that you can render those circuits horizontally as follows:"
@ -2730,6 +2741,7 @@
{
"cell_type": "code",
"execution_count": 7,
"id": "14410565",
"metadata": {},
"outputs": [
{
@ -2805,6 +2817,7 @@
},
{
"cell_type": "markdown",
"id": "9ccbc2e2",
"metadata": {},
"source": [
"To encode the circuit in the aig format (ASCII version) use:"
@ -2813,6 +2826,7 @@
{
"cell_type": "code",
"execution_count": 8,
"id": "06e485d0",
"metadata": {},
"outputs": [
{
@ -2836,6 +2850,7 @@
},
{
"cell_type": "markdown",
"id": "5f006648",
"metadata": {},
"source": [
"# Adding more inputs and outputs by force"
@ -2843,6 +2858,7 @@
},
{
"cell_type": "markdown",
"id": "9905208f",
"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",
@ -2854,6 +2870,7 @@
{
"cell_type": "code",
"execution_count": 9,
"id": "560a7e46",
"metadata": {},
"outputs": [
{
@ -3022,7 +3039,7 @@
"</svg>\n"
],
"text/plain": [
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f4948141cc0> >"
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fe9bc6a8360> >"
]
},
"metadata": {},
@ -3097,7 +3114,7 @@
"</svg>\n"
],
"text/plain": [
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f4948141de0> >"
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fe9bd884390> >"
]
},
"metadata": {},
@ -3174,7 +3191,7 @@
"</svg>\n"
],
"text/plain": [
"<spot.aig; proxy of <Swig Object of type 'spot::aig_ptr *' at 0x7f49482d5c90> >"
"<spot.aig; proxy of <Swig Object of type 'spot::aig_ptr *' at 0x7fe9bc6a8660> >"
]
},
"metadata": {},
@ -3194,6 +3211,7 @@
},
{
"cell_type": "markdown",
"id": "06d42ec3",
"metadata": {},
"source": [
"To force the presence of extra variables in the circuit, they can be passed to `mealy_machine_to_aig()`."
@ -3202,6 +3220,7 @@
{
"cell_type": "code",
"execution_count": 10,
"id": "6ea759ea",
"metadata": {},
"outputs": [
{
@ -3299,7 +3318,7 @@
"</svg>\n"
],
"text/plain": [
"<spot.aig; proxy of <Swig Object of type 'spot::aig_ptr *' at 0x7f494811f750> >"
"<spot.aig; proxy of <Swig Object of type 'spot::aig_ptr *' at 0x7fe9bc6a8900> >"
]
},
"metadata": {},
@ -3312,6 +3331,7 @@
},
{
"cell_type": "markdown",
"id": "4135f43e",
"metadata": {},
"source": [
"# Combining mealy machines\n",
@ -3325,191 +3345,15 @@
},
{
"cell_type": "code",
"execution_count": 11,
"execution_count": 17,
"id": "4f9be142",
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"initial games\n"
]
},
{
"data": {
"text/html": [
"<div style='vertical-align:text-top;display:inline-block;'><?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n",
"<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n",
" \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n",
"<!-- Generated by graphviz version 2.43.0 (0)\n",
" -->\n",
"<!-- Pages: 1 -->\n",
"<svg width=\"286pt\" height=\"236pt\"\n",
" viewBox=\"0.00 0.00 286.00 236.28\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
"<g id=\"graph0\" class=\"graph\" transform=\"scale(1.0 1.0) rotate(0) translate(4 232.28)\">\n",
"<polygon fill=\"white\" stroke=\"transparent\" points=\"-4,4 -4,-232.28 282,-232.28 282,4 -4,4\"/>\n",
"<text text-anchor=\"start\" x=\"27.5\" y=\"-214.08\" font-family=\"Lato\" font-size=\"14.00\">Inf(</text>\n",
"<text text-anchor=\"start\" x=\"48.5\" y=\"-214.08\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#6a3d9a\">❸</text>\n",
"<text text-anchor=\"start\" x=\"64.5\" y=\"-214.08\" font-family=\"Lato\" font-size=\"14.00\">) | (Fin(</text>\n",
"<text text-anchor=\"start\" x=\"106.5\" y=\"-214.08\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#ff7f00\">❷</text>\n",
"<text text-anchor=\"start\" x=\"122.5\" y=\"-214.08\" font-family=\"Lato\" font-size=\"14.00\">) &amp; (Inf(</text>\n",
"<text text-anchor=\"start\" x=\"168.5\" y=\"-214.08\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#ff4da0\">❶</text>\n",
"<text text-anchor=\"start\" x=\"184.5\" y=\"-214.08\" font-family=\"Lato\" font-size=\"14.00\">) | Fin(</text>\n",
"<text text-anchor=\"start\" x=\"222.5\" y=\"-214.08\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">⓿</text>\n",
"<text text-anchor=\"start\" x=\"238.5\" y=\"-214.08\" font-family=\"Lato\" font-size=\"14.00\">)))</text>\n",
"<text text-anchor=\"start\" x=\"83.5\" y=\"-200.08\" font-family=\"Lato\" font-size=\"14.00\">[parity max odd 4]</text>\n",
"<!-- I -->\n",
"<!-- 0 -->\n",
"<g id=\"node2\" class=\"node\">\n",
"<title>0</title>\n",
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"56\" cy=\"-93.28\" rx=\"18\" ry=\"18\"/>\n",
"<text text-anchor=\"middle\" x=\"56\" y=\"-89.58\" font-family=\"Lato\" font-size=\"14.00\">0</text>\n",
"</g>\n",
"<!-- I&#45;&gt;0 -->\n",
"<g id=\"edge1\" class=\"edge\">\n",
"<title>I&#45;&gt;0</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M1.15,-93.28C2.79,-93.28 17.15,-93.28 30.63,-93.28\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"37.94,-93.28 30.94,-96.43 34.44,-93.28 30.94,-93.28 30.94,-93.28 30.94,-93.28 34.44,-93.28 30.94,-90.13 37.94,-93.28 37.94,-93.28\"/>\n",
"</g>\n",
"<!-- 1 -->\n",
"<g id=\"node3\" class=\"node\">\n",
"<title>1</title>\n",
"<polygon fill=\"#ffffaa\" stroke=\"black\" points=\"251,-151.28 224,-133.28 251,-115.28 278,-133.28 251,-151.28\"/>\n",
"<text text-anchor=\"middle\" x=\"251\" y=\"-129.58\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
"</g>\n",
"<!-- 0&#45;&gt;1 -->\n",
"<g id=\"edge2\" class=\"edge\">\n",
"<title>0&#45;&gt;1</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M62.13,-110.41C67.26,-124.18 76.64,-142.61 92,-151.28 135.36,-175.76 196.05,-156.81 228.13,-143.47\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"234.89,-140.57 229.71,-146.22 231.68,-141.95 228.46,-143.33 228.46,-143.33 228.46,-143.33 231.68,-141.95 227.22,-140.44 234.89,-140.57 234.89,-140.57\"/>\n",
"<text text-anchor=\"start\" x=\"92\" y=\"-181.08\" font-family=\"Lato\" font-size=\"14.00\">(!i0 &amp; !i1) | (i0 &amp; i1)</text>\n",
"<text text-anchor=\"start\" x=\"141\" y=\"-166.08\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#ff4da0\">❶</text>\n",
"</g>\n",
"<!-- 2 -->\n",
"<g id=\"node4\" class=\"node\">\n",
"<title>2</title>\n",
"<polygon fill=\"#ffffaa\" stroke=\"black\" points=\"251,-71.28 224,-53.28 251,-35.28 278,-53.28 251,-71.28\"/>\n",
"<text text-anchor=\"middle\" x=\"251\" y=\"-49.58\" font-family=\"Lato\" font-size=\"14.00\">2</text>\n",
"</g>\n",
"<!-- 0&#45;&gt;2 -->\n",
"<g id=\"edge3\" class=\"edge\">\n",
"<title>0&#45;&gt;2</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M70,-81.48C76.21,-76.54 84.03,-71.26 92,-68.28 134,-52.59 186.43,-50.79 219.07,-51.55\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"226.12,-51.77 219.03,-54.7 222.62,-51.66 219.13,-51.55 219.13,-51.55 219.13,-51.55 222.62,-51.66 219.22,-48.41 226.12,-51.77 226.12,-51.77\"/>\n",
"<text text-anchor=\"start\" x=\"92\" y=\"-87.08\" font-family=\"Lato\" font-size=\"14.00\">(!i0 &amp; i1) | (i0 &amp; !i1)</text>\n",
"<text text-anchor=\"start\" x=\"141\" y=\"-72.08\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#ff4da0\">❶</text>\n",
"</g>\n",
"<!-- 1&#45;&gt;0 -->\n",
"<g id=\"edge4\" class=\"edge\">\n",
"<title>1&#45;&gt;0</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M233.93,-126.61C225.7,-123.4 215.44,-119.73 206,-117.28 194.17,-114.2 120.45,-102.86 81.33,-96.94\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"73.99,-95.83 81.39,-93.76 77.46,-96.35 80.92,-96.88 80.92,-96.88 80.92,-96.88 77.46,-96.35 80.45,-99.99 73.99,-95.83 73.99,-95.83\"/>\n",
"<text text-anchor=\"start\" x=\"138.5\" y=\"-136.08\" font-family=\"Lato\" font-size=\"14.00\">!o0</text>\n",
"<text text-anchor=\"start\" x=\"141\" y=\"-121.08\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#6a3d9a\">❸</text>\n",
"</g>\n",
"<!-- 2&#45;&gt;0 -->\n",
"<g id=\"edge5\" class=\"edge\">\n",
"<title>2&#45;&gt;0</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M240.46,-42.08C232.31,-33.45 219.76,-22.19 206,-17.28 158.28,-0.24 134.67,10.05 92,-17.28 74.55,-28.45 65.68,-50.76 61.25,-68.34\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"59.61,-75.53 58.09,-68.01 60.39,-72.12 61.16,-68.71 61.16,-68.71 61.16,-68.71 60.39,-72.12 64.23,-69.41 59.61,-75.53 59.61,-75.53\"/>\n",
"<text text-anchor=\"start\" x=\"140.5\" y=\"-36.08\" font-family=\"Lato\" font-size=\"14.00\">o0</text>\n",
"<text text-anchor=\"start\" x=\"141\" y=\"-21.08\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#6a3d9a\">❸</text>\n",
"</g>\n",
"</g>\n",
"</svg>\n",
"</div><div style='vertical-align:text-top;display:inline-block;'><?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n",
"<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n",
" \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n",
"<!-- Generated by graphviz version 2.43.0 (0)\n",
" -->\n",
"<!-- Pages: 1 -->\n",
"<svg width=\"286pt\" height=\"236pt\"\n",
" viewBox=\"0.00 0.00 286.00 236.28\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
"<g id=\"graph0\" class=\"graph\" transform=\"scale(1.0 1.0) rotate(0) translate(4 232.28)\">\n",
"<polygon fill=\"white\" stroke=\"transparent\" points=\"-4,4 -4,-232.28 282,-232.28 282,4 -4,4\"/>\n",
"<text text-anchor=\"start\" x=\"27.5\" y=\"-214.08\" font-family=\"Lato\" font-size=\"14.00\">Inf(</text>\n",
"<text text-anchor=\"start\" x=\"48.5\" y=\"-214.08\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#6a3d9a\">❸</text>\n",
"<text text-anchor=\"start\" x=\"64.5\" y=\"-214.08\" font-family=\"Lato\" font-size=\"14.00\">) | (Fin(</text>\n",
"<text text-anchor=\"start\" x=\"106.5\" y=\"-214.08\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#ff7f00\">❷</text>\n",
"<text text-anchor=\"start\" x=\"122.5\" y=\"-214.08\" font-family=\"Lato\" font-size=\"14.00\">) &amp; (Inf(</text>\n",
"<text text-anchor=\"start\" x=\"168.5\" y=\"-214.08\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#ff4da0\">❶</text>\n",
"<text text-anchor=\"start\" x=\"184.5\" y=\"-214.08\" font-family=\"Lato\" font-size=\"14.00\">) | Fin(</text>\n",
"<text text-anchor=\"start\" x=\"222.5\" y=\"-214.08\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">⓿</text>\n",
"<text text-anchor=\"start\" x=\"238.5\" y=\"-214.08\" font-family=\"Lato\" font-size=\"14.00\">)))</text>\n",
"<text text-anchor=\"start\" x=\"83.5\" y=\"-200.08\" font-family=\"Lato\" font-size=\"14.00\">[parity max odd 4]</text>\n",
"<!-- I -->\n",
"<!-- 0 -->\n",
"<g id=\"node2\" class=\"node\">\n",
"<title>0</title>\n",
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"56\" cy=\"-93.28\" rx=\"18\" ry=\"18\"/>\n",
"<text text-anchor=\"middle\" x=\"56\" y=\"-89.58\" font-family=\"Lato\" font-size=\"14.00\">0</text>\n",
"</g>\n",
"<!-- I&#45;&gt;0 -->\n",
"<g id=\"edge1\" class=\"edge\">\n",
"<title>I&#45;&gt;0</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M1.15,-93.28C2.79,-93.28 17.15,-93.28 30.63,-93.28\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"37.94,-93.28 30.94,-96.43 34.44,-93.28 30.94,-93.28 30.94,-93.28 30.94,-93.28 34.44,-93.28 30.94,-90.13 37.94,-93.28 37.94,-93.28\"/>\n",
"</g>\n",
"<!-- 1 -->\n",
"<g id=\"node3\" class=\"node\">\n",
"<title>1</title>\n",
"<polygon fill=\"#ffffaa\" stroke=\"black\" points=\"251,-151.28 224,-133.28 251,-115.28 278,-133.28 251,-151.28\"/>\n",
"<text text-anchor=\"middle\" x=\"251\" y=\"-129.58\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
"</g>\n",
"<!-- 0&#45;&gt;1 -->\n",
"<g id=\"edge2\" class=\"edge\">\n",
"<title>0&#45;&gt;1</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M62.13,-110.41C67.26,-124.18 76.64,-142.61 92,-151.28 135.36,-175.76 196.05,-156.81 228.13,-143.47\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"234.89,-140.57 229.71,-146.22 231.68,-141.95 228.46,-143.33 228.46,-143.33 228.46,-143.33 231.68,-141.95 227.22,-140.44 234.89,-140.57 234.89,-140.57\"/>\n",
"<text text-anchor=\"start\" x=\"92\" y=\"-181.08\" font-family=\"Lato\" font-size=\"14.00\">(!i0 &amp; !i1) | (i0 &amp; i1)</text>\n",
"<text text-anchor=\"start\" x=\"141\" y=\"-166.08\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#ff4da0\">❶</text>\n",
"</g>\n",
"<!-- 2 -->\n",
"<g id=\"node4\" class=\"node\">\n",
"<title>2</title>\n",
"<polygon fill=\"#ffffaa\" stroke=\"black\" points=\"251,-71.28 224,-53.28 251,-35.28 278,-53.28 251,-71.28\"/>\n",
"<text text-anchor=\"middle\" x=\"251\" y=\"-49.58\" font-family=\"Lato\" font-size=\"14.00\">2</text>\n",
"</g>\n",
"<!-- 0&#45;&gt;2 -->\n",
"<g id=\"edge3\" class=\"edge\">\n",
"<title>0&#45;&gt;2</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M70,-81.48C76.21,-76.54 84.03,-71.26 92,-68.28 134,-52.59 186.43,-50.79 219.07,-51.55\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"226.12,-51.77 219.03,-54.7 222.62,-51.66 219.13,-51.55 219.13,-51.55 219.13,-51.55 222.62,-51.66 219.22,-48.41 226.12,-51.77 226.12,-51.77\"/>\n",
"<text text-anchor=\"start\" x=\"92\" y=\"-87.08\" font-family=\"Lato\" font-size=\"14.00\">(!i0 &amp; i1) | (i0 &amp; !i1)</text>\n",
"<text text-anchor=\"start\" x=\"141\" y=\"-72.08\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#ff4da0\">❶</text>\n",
"</g>\n",
"<!-- 1&#45;&gt;0 -->\n",
"<g id=\"edge4\" class=\"edge\">\n",
"<title>1&#45;&gt;0</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M233.93,-126.61C225.7,-123.4 215.44,-119.73 206,-117.28 194.17,-114.2 120.45,-102.86 81.33,-96.94\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"73.99,-95.83 81.39,-93.76 77.46,-96.35 80.92,-96.88 80.92,-96.88 80.92,-96.88 77.46,-96.35 80.45,-99.99 73.99,-95.83 73.99,-95.83\"/>\n",
"<text text-anchor=\"start\" x=\"140.5\" y=\"-136.08\" font-family=\"Lato\" font-size=\"14.00\">o1</text>\n",
"<text text-anchor=\"start\" x=\"141\" y=\"-121.08\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#6a3d9a\">❸</text>\n",
"</g>\n",
"<!-- 2&#45;&gt;0 -->\n",
"<g id=\"edge5\" class=\"edge\">\n",
"<title>2&#45;&gt;0</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M240.46,-42.08C232.31,-33.45 219.76,-22.19 206,-17.28 158.28,-0.24 134.67,10.05 92,-17.28 74.55,-28.45 65.68,-50.76 61.25,-68.34\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"59.61,-75.53 58.09,-68.01 60.39,-72.12 61.16,-68.71 61.16,-68.71 61.16,-68.71 60.39,-72.12 64.23,-69.41 59.61,-75.53 59.61,-75.53\"/>\n",
"<text text-anchor=\"start\" x=\"138.5\" y=\"-36.08\" font-family=\"Lato\" font-size=\"14.00\">!o1</text>\n",
"<text text-anchor=\"start\" x=\"141\" y=\"-21.08\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#6a3d9a\">❸</text>\n",
"</g>\n",
"</g>\n",
"</svg>\n",
"</div>"
],
"text/plain": [
"<IPython.core.display.HTML object>"
]
},
"metadata": {},
"output_type": "display_data"
},
{
"name": "stdout",
"output_type": "stream",
"text": [
"solved games\n"
"Solved games:\n"
]
},
{
@ -3686,7 +3530,7 @@
"name": "stdout",
"output_type": "stream",
"text": [
"reduced strategies\n"
"Reduced strategies:\n"
]
},
{
@ -3799,7 +3643,7 @@
"name": "stdout",
"output_type": "stream",
"text": [
"Circuit implementing both machines\n"
"Circuit implementing both machines:\n"
]
},
{
@ -3909,7 +3753,7 @@
"</svg>\n"
],
"text/plain": [
"<spot.aig; proxy of <Swig Object of type 'spot::aig_ptr *' at 0x7f49480dd900> >"
"<spot.aig; proxy of <Swig Object of type 'spot::aig_ptr *' at 0x7fe9bc6ae030> >"
]
},
"metadata": {},
@ -3918,36 +3762,32 @@
],
"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",
"print(\"initial games\")\n",
"display_inline(g1, g2)\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",
"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",
"print(\"Reduced strategies:\")\n",
"display_inline(strat1, strat2)\n",
"print(\"Circuit implementing both machines\")\n",
"m_vec = spot.vector_const_twa_graph()\n",
"m_vec.push_back(strat1)\n",
"m_vec.push_back(strat2)\n",
"aig = spot.mealy_machines_to_aig(m_vec, \"isop\")\n",
"print(\"Circuit implementing both machines:\")\n",
"aig = spot.mealy_machines_to_aig([strat1, strat2], \"isop\")\n",
"display(aig)"
]
},
{
"cell_type": "markdown",
"id": "b3985f04",
"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",
"- 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$)."
]
@ -3955,6 +3795,7 @@
{
"cell_type": "code",
"execution_count": 12,
"id": "3bc0b1f2",
"metadata": {},
"outputs": [],
"source": [
@ -3975,6 +3816,7 @@
{
"cell_type": "code",
"execution_count": 13,
"id": "1455e6ab",
"metadata": {},
"outputs": [
{
@ -4084,7 +3926,7 @@
"</svg>\n"
],
"text/plain": [
"<spot.aig; proxy of <Swig Object of type 'spot::aig_ptr *' at 0x7f49481417e0> >"
"<spot.aig; proxy of <Swig Object of type 'spot::aig_ptr *' at 0x7fe9bc6a8d50> >"
]
},
"metadata": {},
@ -4099,6 +3941,7 @@
{
"cell_type": "code",
"execution_count": 14,
"id": "0c418256",
"metadata": {},
"outputs": [
{
@ -4127,6 +3970,7 @@
{
"cell_type": "code",
"execution_count": 15,
"id": "bd4b6aa2",
"metadata": {},
"outputs": [
{
@ -4143,14 +3987,16 @@
},
{
"cell_type": "markdown",
"id": "94fd22a1",
"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."
"An aiger 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": "b157ec16",
"metadata": {},
"outputs": [
{
@ -4204,7 +4050,7 @@
"</svg>\n"
],
"text/plain": [
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f49481417b0> >"
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fe9bc6a8330> >"
]
},
"execution_count": 16,
@ -4233,7 +4079,7 @@
"name": "python",
"nbconvert_exporter": "python",
"pygments_lexer": "ipython3",
"version": "3.8.10"
"version": "3.9.2"
}
},
"nbformat": 4,