1{
2 "cells": [
3  {
4   "cell_type": "code",
5   "execution_count": 1,
6   "metadata": {},
7   "outputs": [],
8   "source": [
9    "import spot\n",
10    "spot.setup()"
11   ]
12  },
13  {
14   "cell_type": "markdown",
15   "metadata": {},
16   "source": [
17    "Test the Mealy printer."
18   ]
19  },
20  {
21   "cell_type": "code",
22   "execution_count": 2,
23   "metadata": {},
24   "outputs": [],
25   "source": [
26    "g = spot.ltl_to_game('G((a|c) <-> (b|d))', [\"b\", \"d\"])"
27   ]
28  },
29  {
30   "cell_type": "code",
31   "execution_count": 3,
32   "metadata": {},
33   "outputs": [
34    {
35     "data": {
36      "text/plain": [
37       "True"
38      ]
39     },
40     "execution_count": 3,
41     "metadata": {},
42     "output_type": "execute_result"
43    }
44   ],
45   "source": [
46    "spot.solve_game(g)"
47   ]
48  },
49  {
50   "cell_type": "code",
51   "execution_count": 4,
52   "metadata": {},
53   "outputs": [
54    {
55     "data": {
56      "image/svg+xml": [
57       "<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n",
58       "<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n",
59       " \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n",
60       "<!-- Generated by graphviz version 2.43.0 (0)\n",
61       " -->\n",
62       "<!-- Pages: 1 -->\n",
63       "<svg width=\"247pt\" height=\"212pt\"\n",
64       " viewBox=\"0.00 0.00 247.00 212.07\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
65       "<g id=\"graph0\" class=\"graph\" transform=\"scale(1.0 1.0) rotate(0) translate(4 208.07)\">\n",
66       "<polygon fill=\"white\" stroke=\"transparent\" points=\"-4,4 -4,-208.07 243,-208.07 243,4 -4,4\"/>\n",
67       "<text text-anchor=\"start\" x=\"8\" y=\"-189.87\" font-family=\"Lato\" font-size=\"14.00\">Inf(</text>\n",
68       "<text text-anchor=\"start\" x=\"29\" y=\"-189.87\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#6a3d9a\">❸</text>\n",
69       "<text text-anchor=\"start\" x=\"45\" y=\"-189.87\" font-family=\"Lato\" font-size=\"14.00\">) | (Fin(</text>\n",
70       "<text text-anchor=\"start\" x=\"87\" y=\"-189.87\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#ff7f00\">❷</text>\n",
71       "<text text-anchor=\"start\" x=\"103\" y=\"-189.87\" font-family=\"Lato\" font-size=\"14.00\">) &amp; (Inf(</text>\n",
72       "<text text-anchor=\"start\" x=\"149\" y=\"-189.87\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#ff4da0\">❶</text>\n",
73       "<text text-anchor=\"start\" x=\"165\" y=\"-189.87\" font-family=\"Lato\" font-size=\"14.00\">) | Fin(</text>\n",
74       "<text text-anchor=\"start\" x=\"203\" y=\"-189.87\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">⓿</text>\n",
75       "<text text-anchor=\"start\" x=\"219\" y=\"-189.87\" font-family=\"Lato\" font-size=\"14.00\">)))</text>\n",
76       "<text text-anchor=\"start\" x=\"64\" y=\"-175.87\" font-family=\"Lato\" font-size=\"14.00\">[parity max odd 4]</text>\n",
77       "<!-- I -->\n",
78       "<!-- 0 -->\n",
79       "<g id=\"node2\" class=\"node\">\n",
80       "<title>0</title>\n",
81       "<ellipse fill=\"#ffffaa\" stroke=\"#33a02c\" stroke-width=\"2\" cx=\"73.5\" cy=\"-75.07\" rx=\"18\" ry=\"18\"/>\n",
82       "<text text-anchor=\"middle\" x=\"73.5\" y=\"-71.37\" font-family=\"Lato\" font-size=\"14.00\">0</text>\n",
83       "</g>\n",
84       "<!-- I&#45;&gt;0 -->\n",
85       "<g id=\"edge1\" class=\"edge\">\n",
86       "<title>I&#45;&gt;0</title>\n",
87       "<path fill=\"none\" stroke=\"black\" d=\"M18.65,-75.07C20.29,-75.07 34.65,-75.07 48.13,-75.07\"/>\n",
88       "<polygon fill=\"black\" stroke=\"black\" points=\"55.44,-75.07 48.44,-78.22 51.94,-75.07 48.44,-75.07 48.44,-75.07 48.44,-75.07 51.94,-75.07 48.44,-71.92 55.44,-75.07 55.44,-75.07\"/>\n",
89       "</g>\n",
90       "<!-- 1 -->\n",
91       "<g id=\"node3\" class=\"node\">\n",
92       "<title>1</title>\n",
93       "<polygon fill=\"#ffffaa\" stroke=\"#33a02c\" stroke-width=\"2\" points=\"194.5,-133.07 167.5,-115.07 194.5,-97.07 221.5,-115.07 194.5,-133.07\"/>\n",
94       "<text text-anchor=\"middle\" x=\"194.5\" y=\"-111.37\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
95       "</g>\n",
96       "<!-- 0&#45;&gt;1 -->\n",
97       "<g id=\"edge2\" class=\"edge\">\n",
98       "<title>0&#45;&gt;1</title>\n",
99       "<path fill=\"none\" stroke=\"black\" d=\"M79.63,-92.21C84.76,-105.97 94.14,-124.4 109.5,-133.07 129.34,-144.27 155.4,-135.7 173.2,-126.96\"/>\n",
100       "<polygon fill=\"black\" stroke=\"black\" points=\"179.82,-123.52 175.06,-129.54 176.72,-125.13 173.61,-126.75 173.61,-126.75 173.61,-126.75 176.72,-125.13 172.16,-123.95 179.82,-123.52 179.82,-123.52\"/>\n",
101       "<text text-anchor=\"start\" x=\"110\" y=\"-156.87\" font-family=\"Lato\" font-size=\"14.00\">!a &amp; !c</text>\n",
102       "<text text-anchor=\"start\" x=\"121.5\" y=\"-141.87\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#ff4da0\">❶</text>\n",
103       "</g>\n",
104       "<!-- 2 -->\n",
105       "<g id=\"node4\" class=\"node\">\n",
106       "<title>2</title>\n",
107       "<polygon fill=\"#ffffaa\" stroke=\"#33a02c\" stroke-width=\"2\" points=\"194.5,-53.07 167.5,-35.07 194.5,-17.07 221.5,-35.07 194.5,-53.07\"/>\n",
108       "<text text-anchor=\"middle\" x=\"194.5\" y=\"-31.37\" font-family=\"Lato\" font-size=\"14.00\">2</text>\n",
109       "</g>\n",
110       "<!-- 0&#45;&gt;2 -->\n",
111       "<g id=\"edge3\" class=\"edge\">\n",
112       "<title>0&#45;&gt;2</title>\n",
113       "<path fill=\"none\" stroke=\"black\" d=\"M87.62,-63.58C93.86,-58.69 101.65,-53.37 109.5,-50.07 126.19,-43.04 146.1,-39.3 162.35,-37.32\"/>\n",
114       "<polygon fill=\"black\" stroke=\"black\" points=\"169.53,-36.52 162.92,-40.42 166.05,-36.91 162.57,-37.29 162.57,-37.29 162.57,-37.29 166.05,-36.91 162.23,-34.16 169.53,-36.52 169.53,-36.52\"/>\n",
115       "<text text-anchor=\"start\" x=\"117\" y=\"-68.87\" font-family=\"Lato\" font-size=\"14.00\">a | c</text>\n",
116       "<text text-anchor=\"start\" x=\"121.5\" y=\"-53.87\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#ff4da0\">❶</text>\n",
117       "</g>\n",
118       "<!-- 1&#45;&gt;0 -->\n",
119       "<g id=\"edge4\" class=\"edge\">\n",
120       "<title>1&#45;&gt;0</title>\n",
121       "<path fill=\"none\" stroke=\"#33a02c\" stroke-width=\"2\" d=\"M176.84,-108.84C168.63,-105.81 158.58,-102.17 149.5,-99.07 132.27,-93.18 112.66,-86.92 97.82,-82.27\"/>\n",
122       "<polygon fill=\"#33a02c\" stroke=\"#33a02c\" stroke-width=\"2\" points=\"90.95,-80.13 98.57,-79.21 94.44,-80.69 97.78,-81.74 97.63,-82.21 97.48,-82.69 94.14,-81.65 96.69,-85.22 90.95,-80.13 90.95,-80.13\"/>\n",
123       "<text text-anchor=\"start\" x=\"109.5\" y=\"-117.87\" font-family=\"Lato\" font-size=\"14.00\">!b &amp; !d</text>\n",
124       "<text text-anchor=\"start\" x=\"121.5\" y=\"-102.87\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#6a3d9a\">❸</text>\n",
125       "</g>\n",
126       "<!-- 2&#45;&gt;0 -->\n",
127       "<g id=\"edge5\" class=\"edge\">\n",
128       "<title>2&#45;&gt;0</title>\n",
129       "<path fill=\"none\" stroke=\"#33a02c\" stroke-width=\"2\" d=\"M182.23,-25.06C165.46,-11.43 133.34,9.67 109.5,-5.07 93.56,-14.92 84.64,-34.46 79.8,-50.4\"/>\n",
130       "<polygon fill=\"#33a02c\" stroke=\"#33a02c\" stroke-width=\"2\" points=\"77.85,-57.43 76.69,-49.84 78.31,-53.92 79.24,-50.55 79.72,-50.68 80.2,-50.82 79.27,-54.19 82.76,-51.52 77.85,-57.43 77.85,-57.43\"/>\n",
131       "<text text-anchor=\"start\" x=\"116\" y=\"-23.87\" font-family=\"Lato\" font-size=\"14.00\">b | d</text>\n",
132       "<text text-anchor=\"start\" x=\"121.5\" y=\"-8.87\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#6a3d9a\">❸</text>\n",
133       "</g>\n",
134       "</g>\n",
135       "</svg>\n"
136      ],
137      "text/plain": [
138       "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f300caabba0> >"
139      ]
140     },
141     "execution_count": 4,
142     "metadata": {},
143     "output_type": "execute_result"
144    }
145   ],
146   "source": [
147    "spot.highlight_strategy(g)"
148   ]
149  },
150  {
151   "cell_type": "code",
152   "execution_count": 5,
153   "metadata": {},
154   "outputs": [],
155   "source": [
156    "x = spot.solved_game_to_separated_mealy(g)"
157   ]
158  },
159  {
160   "cell_type": "code",
161   "execution_count": 6,
162   "metadata": {},
163   "outputs": [
164    {
165     "data": {
166      "image/svg+xml": [
167       "<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n",
168       "<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n",
169       " \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n",
170       "<!-- Generated by graphviz version 2.43.0 (0)\n",
171       " -->\n",
172       "<!-- Pages: 1 -->\n",
173       "<svg width=\"117pt\" height=\"126pt\"\n",
174       " viewBox=\"0.00 0.00 117.00 126.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
175       "<g id=\"graph0\" class=\"graph\" transform=\"scale(1.0 1.0) rotate(0) translate(4 122)\">\n",
176       "<polygon fill=\"white\" stroke=\"transparent\" points=\"-4,4 -4,-122 113,-122 113,4 -4,4\"/>\n",
177       "<!-- I -->\n",
178       "<!-- 0 -->\n",
179       "<g id=\"node2\" class=\"node\">\n",
180       "<title>0</title>\n",
181       "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"56\" cy=\"-18\" rx=\"18\" ry=\"18\"/>\n",
182       "<text text-anchor=\"middle\" x=\"56\" y=\"-14.3\" font-family=\"Lato\" font-size=\"14.00\">0</text>\n",
183       "</g>\n",
184       "<!-- I&#45;&gt;0 -->\n",
185       "<g id=\"edge1\" class=\"edge\">\n",
186       "<title>I&#45;&gt;0</title>\n",
187       "<path fill=\"none\" stroke=\"black\" d=\"M1.15,-18C2.79,-18 17.15,-18 30.63,-18\"/>\n",
188       "<polygon fill=\"black\" stroke=\"black\" points=\"37.94,-18 30.94,-21.15 34.44,-18 30.94,-18 30.94,-18 30.94,-18 34.44,-18 30.94,-14.85 37.94,-18 37.94,-18\"/>\n",
189       "</g>\n",
190       "<!-- 0&#45;&gt;0 -->\n",
191       "<g id=\"edge2\" class=\"edge\">\n",
192       "<title>0&#45;&gt;0</title>\n",
193       "<path fill=\"none\" stroke=\"black\" d=\"M52.76,-35.78C52.21,-45.31 53.29,-54 56,-54 57.99,-54 59.1,-49.32 59.33,-43.05\"/>\n",
194       "<polygon fill=\"black\" stroke=\"black\" points=\"59.24,-35.78 62.48,-42.74 59.28,-39.28 59.33,-42.78 59.33,-42.78 59.33,-42.78 59.28,-39.28 56.18,-42.82 59.24,-35.78 59.24,-35.78\"/>\n",
195       "<polygon fill=\"#e9f4fb\" stroke=\"transparent\" points=\"5,-55.5 5,-74.5 48,-74.5 48,-55.5 5,-55.5\"/>\n",
196       "<text text-anchor=\"start\" x=\"7\" y=\"-61.3\" font-family=\"Lato\" font-size=\"14.00\">!a &amp; !c</text>\n",
197       "<text text-anchor=\"start\" x=\"52\" y=\"-61.3\" font-family=\"Lato\" font-size=\"14.00\">/</text>\n",
198       "<polygon fill=\"#ffe5f1\" stroke=\"transparent\" points=\"63,-55.5 63,-74.5 107,-74.5 107,-55.5 63,-55.5\"/>\n",
199       "<text text-anchor=\"start\" x=\"65\" y=\"-61.3\" font-family=\"Lato\" font-size=\"14.00\">!b &amp; !d</text>\n",
200       "</g>\n",
201       "<!-- 0&#45;&gt;0 -->\n",
202       "<g id=\"edge3\" class=\"edge\">\n",
203       "<title>0&#45;&gt;0</title>\n",
204       "<path fill=\"none\" stroke=\"black\" d=\"M50.83,-35.41C47.6,-54.42 49.32,-77 56,-77 61.84,-77 63.89,-59.71 62.15,-42.65\"/>\n",
205       "<polygon fill=\"black\" stroke=\"black\" points=\"61.17,-35.41 65.23,-41.93 61.64,-38.88 62.11,-42.35 62.11,-42.35 62.11,-42.35 61.64,-38.88 58.98,-42.77 61.17,-35.41 61.17,-35.41\"/>\n",
206       "<polygon fill=\"#e9f4fb\" stroke=\"transparent\" points=\"19,-78.5 19,-97.5 48,-97.5 48,-78.5 19,-78.5\"/>\n",
207       "<text text-anchor=\"start\" x=\"21\" y=\"-84.3\" font-family=\"Lato\" font-size=\"14.00\">a | c</text>\n",
208       "<text text-anchor=\"start\" x=\"52\" y=\"-84.3\" font-family=\"Lato\" font-size=\"14.00\">/</text>\n",
209       "<polygon fill=\"#ffe5f1\" stroke=\"transparent\" points=\"63,-78.5 63,-97.5 94,-97.5 94,-78.5 63,-78.5\"/>\n",
210       "<text text-anchor=\"start\" x=\"65\" y=\"-84.3\" font-family=\"Lato\" font-size=\"14.00\">b | d</text>\n",
211       "</g>\n",
212       "</g>\n",
213       "</svg>\n"
214      ],
215      "text/plain": [
216       "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f300c179300> >"
217      ]
218     },
219     "execution_count": 6,
220     "metadata": {},
221     "output_type": "execute_result"
222    }
223   ],
224   "source": [
225    "x"
226   ]
227  },
228  {
229   "cell_type": "code",
230   "execution_count": 7,
231   "metadata": {},
232   "outputs": [],
233   "source": [
234    "x.merge_edges()"
235   ]
236  },
237  {
238   "cell_type": "code",
239   "execution_count": 8,
240   "metadata": {},
241   "outputs": [
242    {
243     "data": {
244      "image/svg+xml": [
245       "<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n",
246       "<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n",
247       " \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n",
248       "<!-- Generated by graphviz version 2.43.0 (0)\n",
249       " -->\n",
250       "<!-- Pages: 1 -->\n",
251       "<svg width=\"121pt\" height=\"106pt\"\n",
252       " viewBox=\"0.00 0.00 121.00 106.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
253       "<g id=\"graph0\" class=\"graph\" transform=\"scale(1.0 1.0) rotate(0) translate(4 102)\">\n",
254       "<polygon fill=\"white\" stroke=\"transparent\" points=\"-4,4 -4,-102 117,-102 117,4 -4,4\"/>\n",
255       "<!-- I -->\n",
256       "<!-- 0 -->\n",
257       "<g id=\"node2\" class=\"node\">\n",
258       "<title>0</title>\n",
259       "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"60\" cy=\"-18\" rx=\"18\" ry=\"18\"/>\n",
260       "<text text-anchor=\"middle\" x=\"60\" y=\"-14.3\" font-family=\"Lato\" font-size=\"14.00\">0</text>\n",
261       "</g>\n",
262       "<!-- I&#45;&gt;0 -->\n",
263       "<g id=\"edge1\" class=\"edge\">\n",
264       "<title>I&#45;&gt;0</title>\n",
265       "<path fill=\"none\" stroke=\"black\" d=\"M1.17,-18C3.01,-18 19.75,-18 34.75,-18\"/>\n",
266       "<polygon fill=\"black\" stroke=\"black\" points=\"41.9,-18 34.9,-21.15 38.4,-18 34.9,-18 34.9,-18 34.9,-18 38.4,-18 34.9,-14.85 41.9,-18 41.9,-18\"/>\n",
267       "</g>\n",
268       "<!-- 0&#45;&gt;0 -->\n",
269       "<g id=\"edge2\" class=\"edge\">\n",
270       "<title>0&#45;&gt;0</title>\n",
271       "<path fill=\"none\" stroke=\"black\" d=\"M52.97,-34.66C51.41,-44.62 53.75,-54 60,-54 64.69,-54 67.18,-48.73 67.47,-41.89\"/>\n",
272       "<polygon fill=\"black\" stroke=\"black\" points=\"67.03,-34.66 70.6,-41.46 67.24,-38.16 67.46,-41.65 67.46,-41.65 67.46,-41.65 67.24,-38.16 64.31,-41.84 67.03,-34.66 67.03,-34.66\"/>\n",
273       "<polygon fill=\"#e9f4fb\" stroke=\"transparent\" points=\"9,-77 9,-96 52,-96 52,-77 9,-77\"/>\n",
274       "<text text-anchor=\"start\" x=\"11\" y=\"-82.8\" font-family=\"Lato\" font-size=\"14.00\">!a &amp; !c</text>\n",
275       "<text text-anchor=\"start\" x=\"56\" y=\"-82.8\" font-family=\"Lato\" font-size=\"14.00\">/</text>\n",
276       "<polygon fill=\"#ffe5f1\" stroke=\"transparent\" points=\"67,-77 67,-96 111,-96 111,-77 67,-77\"/>\n",
277       "<text text-anchor=\"start\" x=\"69\" y=\"-82.8\" font-family=\"Lato\" font-size=\"14.00\">!b &amp; !d</text>\n",
278       "<polygon fill=\"#e9f4fb\" stroke=\"transparent\" points=\"9,-56 9,-75 52,-75 52,-56 9,-56\"/>\n",
279       "<text text-anchor=\"start\" x=\"25\" y=\"-61.8\" font-family=\"Lato\" font-size=\"14.00\">a | c</text>\n",
280       "<text text-anchor=\"start\" x=\"56\" y=\"-61.8\" font-family=\"Lato\" font-size=\"14.00\">/</text>\n",
281       "<polygon fill=\"#ffe5f1\" stroke=\"transparent\" points=\"67,-56 67,-75 111,-75 111,-56 67,-56\"/>\n",
282       "<text text-anchor=\"start\" x=\"69\" y=\"-61.8\" font-family=\"Lato\" font-size=\"14.00\">b | d</text>\n",
283       "</g>\n",
284       "</g>\n",
285       "</svg>\n"
286      ],
287      "text/plain": [
288       "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f300c179300> >"
289      ]
290     },
291     "execution_count": 8,
292     "metadata": {},
293     "output_type": "execute_result"
294    }
295   ],
296   "source": [
297    "x"
298   ]
299  }
300 ],
301 "metadata": {
302  "kernelspec": {
303   "display_name": "Python 3",
304   "language": "python",
305   "name": "python3"
306  },
307  "language_info": {
308   "codemirror_mode": {
309    "name": "ipython",
310    "version": 3
311   },
312   "file_extension": ".py",
313   "mimetype": "text/x-python",
314   "name": "python",
315   "nbconvert_exporter": "python",
316   "pygments_lexer": "ipython3",
317   "version": "3.8.10"
318  }
319 },
320 "nbformat": 4,
321 "nbformat_minor": 5
322}
323