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\">) & (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->0 -->\n", 85 "<g id=\"edge1\" class=\"edge\">\n", 86 "<title>I->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->1 -->\n", 97 "<g id=\"edge2\" class=\"edge\">\n", 98 "<title>0->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 & !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->2 -->\n", 111 "<g id=\"edge3\" class=\"edge\">\n", 112 "<title>0->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->0 -->\n", 119 "<g id=\"edge4\" class=\"edge\">\n", 120 "<title>1->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 & !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->0 -->\n", 127 "<g id=\"edge5\" class=\"edge\">\n", 128 "<title>2->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->0 -->\n", 185 "<g id=\"edge1\" class=\"edge\">\n", 186 "<title>I->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->0 -->\n", 191 "<g id=\"edge2\" class=\"edge\">\n", 192 "<title>0->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 & !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 & !d</text>\n", 200 "</g>\n", 201 "<!-- 0->0 -->\n", 202 "<g id=\"edge3\" class=\"edge\">\n", 203 "<title>0->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->0 -->\n", 263 "<g id=\"edge1\" class=\"edge\">\n", 264 "<title>I->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->0 -->\n", 269 "<g id=\"edge2\" class=\"edge\">\n", 270 "<title>0->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 & !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 & !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