19348c8938
* python/spot/impl.i (get_product_states, set_product_states): New. * tests/python/product.ipynb: Use it. * NEWS: Mention it.
2313 lines
194 KiB
Text
2313 lines
194 KiB
Text
{
|
|
"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.6.4"
|
|
},
|
|
"name": ""
|
|
},
|
|
"nbformat": 3,
|
|
"nbformat_minor": 0,
|
|
"worksheets": [
|
|
{
|
|
"cells": [
|
|
{
|
|
"cell_type": "code",
|
|
"collapsed": false,
|
|
"input": [
|
|
"from IPython.display import display, HTML\n",
|
|
"import spot\n",
|
|
"import buddy\n",
|
|
"spot.setup(show_default='.tavb')\n",
|
|
"\n",
|
|
"def horiz(*args):\n",
|
|
" \"\"\"Display multiple arguments side by side in a table.\"\"\"\n",
|
|
" s = '<table><tr>'\n",
|
|
" for arg in args:\n",
|
|
" s += '<td style=\\\"vertical-align: top;\\\">' + arg.data + '</td>'\n",
|
|
" return HTML(s + '</tr></table>')"
|
|
],
|
|
"language": "python",
|
|
"metadata": {},
|
|
"outputs": [],
|
|
"prompt_number": 1
|
|
},
|
|
{
|
|
"cell_type": "markdown",
|
|
"metadata": {},
|
|
"source": [
|
|
"# Anatomy of a product\n",
|
|
"\n",
|
|
"In this notebook, we write a Python function that constructs the product of two automata.\n",
|
|
"\n",
|
|
"This is obviously not a new feature: Spot can already make a product of two automata using its `product()` function. \n",
|
|
"For instance:"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"collapsed": false,
|
|
"input": [
|
|
"a1 = spot.translate('X(a W b)')\n",
|
|
"a2 = spot.translate('G(Fc U b)')\n",
|
|
"prod = spot.product(a1, a2)\n",
|
|
"horiz(a1.show(), a2.show(), prod.show())"
|
|
],
|
|
"language": "python",
|
|
"metadata": {},
|
|
"outputs": [
|
|
{
|
|
"html": [
|
|
"<table><tr><td style=\"vertical-align: top;\"><svg height=\"307pt\" viewBox=\"0.00 0.00 99.00 307.00\" width=\"99pt\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
|
|
"<g class=\"graph\" id=\"graph0\" transform=\"scale(1 1) rotate(0) translate(4 303)\">\n",
|
|
"<title>G</title>\n",
|
|
"<polygon fill=\"white\" points=\"-4,4 -4,-303 95,-303 95,4 -4,4\" stroke=\"none\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"24.5\" y=\"-284.8\">Inf(</text>\n",
|
|
"<text fill=\"#1f78b4\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"46.5\" y=\"-284.8\">\u24ff</text>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"62.5\" y=\"-284.8\">)</text>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"22.5\" y=\"-270.8\">[B\u00fcchi]</text>\n",
|
|
"<!-- I -->\n",
|
|
"<!-- 1 -->\n",
|
|
"<g class=\"node\" id=\"node2\"><title>1</title>\n",
|
|
"<ellipse cx=\"18\" cy=\"-207\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"18\" y=\"-203.3\">1</text>\n",
|
|
"</g>\n",
|
|
"<!-- I->1 -->\n",
|
|
"<g class=\"edge\" id=\"edge1\"><title>I->1</title>\n",
|
|
"<path d=\"M18,-261.845C18,-260.206 18,-245.846 18,-232.368\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"18,-225.058 21.1501,-232.058 18,-228.558 18.0001,-232.058 18.0001,-232.058 18.0001,-232.058 18,-228.558 14.8501,-232.058 18,-225.058 18,-225.058\" stroke=\"black\"/>\n",
|
|
"</g>\n",
|
|
"<!-- 0 -->\n",
|
|
"<g class=\"node\" id=\"node3\"><title>0</title>\n",
|
|
"<ellipse cx=\"18\" cy=\"-120\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"18\" y=\"-116.3\">0</text>\n",
|
|
"</g>\n",
|
|
"<!-- 1->0 -->\n",
|
|
"<g class=\"edge\" id=\"edge4\"><title>1->0</title>\n",
|
|
"<path d=\"M18,-188.799C18,-176.356 18,-159.364 18,-145.504\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"18,-138.175 21.1501,-145.175 18,-141.675 18.0001,-145.175 18.0001,-145.175 18.0001,-145.175 18,-141.675 14.8501,-145.175 18,-138.175 18,-138.175\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"22.5\" y=\"-159.8\">1</text>\n",
|
|
"</g>\n",
|
|
"<!-- 0->0 -->\n",
|
|
"<g class=\"edge\" id=\"edge2\"><title>0->0</title>\n",
|
|
"<path d=\"M34.6641,-127.383C44.625,-129.023 54,-126.562 54,-120 54,-115.078 48.7266,-112.463 41.8876,-112.156\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"34.6641,-112.617 41.449,-109.027 38.1569,-112.394 41.6498,-112.171 41.6498,-112.171 41.6498,-112.171 38.1569,-112.394 41.8507,-115.314 34.6641,-112.617 34.6641,-112.617\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"54\" y=\"-123.8\">a & !b</text>\n",
|
|
"<text fill=\"#1f78b4\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"64.5\" y=\"-108.8\">\u24ff</text>\n",
|
|
"</g>\n",
|
|
"<!-- 2 -->\n",
|
|
"<g class=\"node\" id=\"node4\"><title>2</title>\n",
|
|
"<ellipse cx=\"18\" cy=\"-18\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"18\" y=\"-14.3\">2</text>\n",
|
|
"</g>\n",
|
|
"<!-- 0->2 -->\n",
|
|
"<g class=\"edge\" id=\"edge3\"><title>0->2</title>\n",
|
|
"<path d=\"M18,-101.581C18,-85.5213 18,-61.5179 18,-43.5228\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"18,-36.2191 21.1501,-43.219 18,-39.7191 18.0001,-43.2191 18.0001,-43.2191 18.0001,-43.2191 18,-39.7191 14.8501,-43.2191 18,-36.2191 18,-36.2191\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"21.5\" y=\"-72.8\">b</text>\n",
|
|
"<text fill=\"#1f78b4\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"18\" y=\"-57.8\">\u24ff</text>\n",
|
|
"</g>\n",
|
|
"<!-- 2->2 -->\n",
|
|
"<g class=\"edge\" id=\"edge5\"><title>2->2</title>\n",
|
|
"<path d=\"M33.916,-26.6334C44.1504,-28.8856 54,-26.0078 54,-18 54,-11.869 48.2263,-8.74515 40.9268,-8.6284\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"33.916,-9.36658 40.5477,-5.50081 37.3968,-9.00004 40.8775,-8.6335 40.8775,-8.6335 40.8775,-8.6335 37.3968,-9.00004 41.2074,-11.7662 33.916,-9.36658 33.916,-9.36658\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"57.5\" y=\"-21.8\">1</text>\n",
|
|
"<text fill=\"#1f78b4\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"54\" y=\"-6.8\">\u24ff</text>\n",
|
|
"</g>\n",
|
|
"</g>\n",
|
|
"</svg></td><td style=\"vertical-align: top;\"><svg height=\"220pt\" viewBox=\"0.00 0.00 208.07 220.00\" width=\"208pt\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
|
|
"<g class=\"graph\" id=\"graph0\" transform=\"scale(1 1) rotate(0) translate(4 216)\">\n",
|
|
"<title>G</title>\n",
|
|
"<polygon fill=\"white\" points=\"-4,4 -4,-216 204.071,-216 204.071,4 -4,4\" stroke=\"none\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"53.0356\" y=\"-197.8\">Inf(</text>\n",
|
|
"<text fill=\"#1f78b4\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"75.0356\" y=\"-197.8\">\u24ff</text>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"91.0356\" y=\"-197.8\">)&Inf(</text>\n",
|
|
"<text fill=\"#ff4da0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"127.036\" y=\"-197.8\">\u2776</text>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"143.036\" y=\"-197.8\">)</text>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"56.0356\" y=\"-183.8\">[gen. B\u00fcchi 2]</text>\n",
|
|
"<!-- I -->\n",
|
|
"<!-- 0 -->\n",
|
|
"<g class=\"node\" id=\"node2\"><title>0</title>\n",
|
|
"<ellipse cx=\"68.0713\" cy=\"-120\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"68.0713\" y=\"-116.3\">0</text>\n",
|
|
"</g>\n",
|
|
"<!-- I->0 -->\n",
|
|
"<g class=\"edge\" id=\"edge1\"><title>I->0</title>\n",
|
|
"<path d=\"M68.0713,-174.845C68.0713,-173.206 68.0713,-158.846 68.0713,-145.368\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"68.0713,-138.058 71.2214,-145.058 68.0713,-141.558 68.0714,-145.058 68.0714,-145.058 68.0714,-145.058 68.0713,-141.558 64.9214,-145.058 68.0713,-138.058 68.0713,-138.058\" stroke=\"black\"/>\n",
|
|
"</g>\n",
|
|
"<!-- 0->0 -->\n",
|
|
"<g class=\"edge\" id=\"edge2\"><title>0->0</title>\n",
|
|
"<path d=\"M85.853,-123.236C95.3862,-123.786 104.071,-122.707 104.071,-120 104.071,-118.012 99.3874,-116.902 93.1234,-116.671\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"85.853,-116.764 92.8119,-113.524 89.3527,-116.719 92.8524,-116.674 92.8524,-116.674 92.8524,-116.674 89.3527,-116.719 92.893,-119.824 85.853,-116.764 85.853,-116.764\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"104.071\" y=\"-123.8\">!b & c</text>\n",
|
|
"<text fill=\"#1f78b4\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"114.571\" y=\"-108.8\">\u24ff</text>\n",
|
|
"</g>\n",
|
|
"<!-- 0->0 -->\n",
|
|
"<g class=\"edge\" id=\"edge3\"><title>0->0</title>\n",
|
|
"<path d=\"M85.6405,-124.845C108.831,-128.506 141.071,-126.891 141.071,-120 141.071,-113.782 114.821,-111.86 92.6551,-114.234\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"85.6405,-115.155 92.1705,-111.12 89.1107,-114.699 92.5808,-114.243 92.5808,-114.243 92.5808,-114.243 89.1107,-114.699 92.9912,-117.366 85.6405,-115.155 85.6405,-115.155\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"152.571\" y=\"-123.8\">b</text>\n",
|
|
"<text fill=\"#1f78b4\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"141.071\" y=\"-109.8\">\u24ff</text>\n",
|
|
"<text fill=\"#ff4da0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"157.071\" y=\"-109.8\">\u2776</text>\n",
|
|
"</g>\n",
|
|
"<!-- 1 -->\n",
|
|
"<g class=\"node\" id=\"node3\"><title>1</title>\n",
|
|
"<ellipse cx=\"68.0713\" cy=\"-18\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"68.0713\" y=\"-14.3\">1</text>\n",
|
|
"</g>\n",
|
|
"<!-- 0->1 -->\n",
|
|
"<g class=\"edge\" id=\"edge4\"><title>0->1</title>\n",
|
|
"<path d=\"M50.6907,-114.668C35.6563,-109.899 14.8429,-100.607 5.07128,-84 -1.69043,-72.5084 -1.69043,-65.4916 5.07128,-54 13.4688,-39.7284 30.0209,-30.8587 44.052,-25.6199\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"50.6907,-23.3321 45.0991,-28.591 47.3817,-24.4725 44.0727,-25.6129 44.0727,-25.6129 44.0727,-25.6129 47.3817,-24.4725 43.0464,-22.6348 50.6907,-23.3321 50.6907,-23.3321\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"5.07128\" y=\"-65.3\">!b & !c</text>\n",
|
|
"</g>\n",
|
|
"<!-- 1->0 -->\n",
|
|
"<g class=\"edge\" id=\"edge5\"><title>1->0</title>\n",
|
|
"<path d=\"M68.0713,-36.2191C68.0713,-52.2129 68.0713,-76.208 68.0713,-94.2528\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"68.0713,-101.581 64.9214,-94.5813 68.0713,-98.0813 68.0714,-94.5813 68.0714,-94.5813 68.0714,-94.5813 68.0713,-98.0813 71.2214,-94.5814 68.0713,-101.581 68.0713,-101.581\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"68.0713\" y=\"-72.8\">!b & c</text>\n",
|
|
"<text fill=\"#1f78b4\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"78.5713\" y=\"-57.8\">\u24ff</text>\n",
|
|
"</g>\n",
|
|
"<!-- 1->0 -->\n",
|
|
"<g class=\"edge\" id=\"edge6\"><title>1->0</title>\n",
|
|
"<path d=\"M83.2231,-28.3294C91.6629,-34.4628 101.389,-43.3215 106.071,-54 111.426,-66.211 111.426,-71.789 106.071,-84 102.413,-92.3425 95.6767,-99.5744 88.8801,-105.264\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"83.2231,-109.671 86.8095,-102.884 85.9842,-107.52 88.7453,-105.369 88.7453,-105.369 88.7453,-105.369 85.9842,-107.52 90.6812,-107.854 83.2231,-109.671 83.2231,-109.671\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"110.071\" y=\"-72.8\">b & c</text>\n",
|
|
"<text fill=\"#1f78b4\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"111.071\" y=\"-58.8\">\u24ff</text>\n",
|
|
"<text fill=\"#ff4da0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"127.071\" y=\"-58.8\">\u2776</text>\n",
|
|
"</g>\n",
|
|
"<!-- 1->1 -->\n",
|
|
"<g class=\"edge\" id=\"edge7\"><title>1->1</title>\n",
|
|
"<path d=\"M85.853,-22.4941C95.3862,-23.2578 104.071,-21.7598 104.071,-18 104.071,-15.2389 99.3874,-13.6976 93.1234,-13.3761\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"85.853,-13.5059 92.7956,-10.2313 89.3525,-13.4434 92.8519,-13.3808 92.8519,-13.3808 92.8519,-13.3808 89.3525,-13.4434 92.9082,-16.5303 85.853,-13.5059 85.853,-13.5059\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"104.071\" y=\"-14.3\">!b & !c</text>\n",
|
|
"</g>\n",
|
|
"<!-- 1->1 -->\n",
|
|
"<g class=\"edge\" id=\"edge8\"><title>1->1</title>\n",
|
|
"<path d=\"M85.0887,-24.4905C109.42,-29.8803 145.071,-27.7168 145.071,-18 145.071,-9.19415 115.791,-6.59174 92.1916,-10.1928\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"85.0887,-11.5095 91.3972,-7.13627 88.5301,-10.8715 91.9714,-10.2335 91.9714,-10.2335 91.9714,-10.2335 88.5301,-10.8715 92.5456,-13.3307 85.0887,-11.5095 85.0887,-11.5095\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"145.071\" y=\"-21.8\">b & !c</text>\n",
|
|
"<text fill=\"#ff4da0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"155.571\" y=\"-6.8\">\u2776</text>\n",
|
|
"</g>\n",
|
|
"</g>\n",
|
|
"</svg></td><td style=\"vertical-align: top;\"><svg height=\"360pt\" viewBox=\"0.00 0.00 193.38 360.00\" width=\"193pt\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
|
|
"<g class=\"graph\" id=\"graph0\" transform=\"scale(0.687023 0.687023) rotate(0) translate(4 520)\">\n",
|
|
"<title>G</title>\n",
|
|
"<polygon fill=\"white\" points=\"-4,4 -4,-520 277.475,-520 277.475,4 -4,4\" stroke=\"none\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"63.7375\" y=\"-501.8\">Inf(</text>\n",
|
|
"<text fill=\"#1f78b4\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"85.7375\" y=\"-501.8\">\u24ff</text>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"101.738\" y=\"-501.8\">)&Inf(</text>\n",
|
|
"<text fill=\"#ff4da0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"137.738\" y=\"-501.8\">\u2776</text>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"153.738\" y=\"-501.8\">)&Inf(</text>\n",
|
|
"<text fill=\"#ff7f00\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"189.738\" y=\"-501.8\">\u2777</text>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"205.738\" y=\"-501.8\">)</text>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"92.7375\" y=\"-487.8\">[gen. B\u00fcchi 3]</text>\n",
|
|
"<!-- I -->\n",
|
|
"<!-- 0 -->\n",
|
|
"<g class=\"node\" id=\"node2\"><title>0</title>\n",
|
|
"<ellipse cx=\"100.475\" cy=\"-424\" fill=\"#ffffaa\" rx=\"27\" ry=\"18\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"90.475\" y=\"-420.3\">1,0</text>\n",
|
|
"</g>\n",
|
|
"<!-- I->0 -->\n",
|
|
"<g class=\"edge\" id=\"edge1\"><title>I->0</title>\n",
|
|
"<path d=\"M100.475,-478.845C100.475,-477.206 100.475,-462.846 100.475,-449.368\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"100.475,-442.058 103.625,-449.058 100.475,-445.558 100.475,-449.058 100.475,-449.058 100.475,-449.058 100.475,-445.558 97.3251,-449.058 100.475,-442.058 100.475,-442.058\" stroke=\"black\"/>\n",
|
|
"</g>\n",
|
|
"<!-- 1 -->\n",
|
|
"<g class=\"node\" id=\"node3\"><title>1</title>\n",
|
|
"<ellipse cx=\"40.475\" cy=\"-322\" fill=\"#ffffaa\" rx=\"27\" ry=\"18\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"30.475\" y=\"-318.3\">0,0</text>\n",
|
|
"</g>\n",
|
|
"<!-- 0->1 -->\n",
|
|
"<g class=\"edge\" id=\"edge2\"><title>0->1</title>\n",
|
|
"<path d=\"M76.7094,-415.391C63.8708,-409.939 49.1208,-401.189 41.475,-388 34.4247,-375.839 33.9982,-360.124 35.419,-347.193\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"36.4329,-339.949 38.5821,-347.318 35.9477,-343.415 35.4625,-346.881 35.4625,-346.881 35.4625,-346.881 35.9477,-343.415 32.3429,-346.445 36.4329,-339.949 36.4329,-339.949\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"41.475\" y=\"-376.8\">!b & c</text>\n",
|
|
"<text fill=\"#ff4da0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"51.975\" y=\"-361.8\">\u2776</text>\n",
|
|
"</g>\n",
|
|
"<!-- 0->1 -->\n",
|
|
"<g class=\"edge\" id=\"edge3\"><title>0->1</title>\n",
|
|
"<path d=\"M97.1632,-405.948C93.9364,-392.198 88.0849,-372.783 78.475,-358 74.4421,-351.796 69.062,-345.956 63.6219,-340.889\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"58.2095,-336.096 65.5383,-338.379 60.8296,-338.416 63.4498,-340.737 63.4498,-340.737 63.4498,-340.737 60.8296,-338.416 61.3613,-343.095 58.2095,-336.096 58.2095,-336.096\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"102.975\" y=\"-376.8\">b</text>\n",
|
|
"<text fill=\"#ff4da0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"91.475\" y=\"-362.8\">\u2776</text>\n",
|
|
"<text fill=\"#ff7f00\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"107.475\" y=\"-362.8\">\u2777</text>\n",
|
|
"</g>\n",
|
|
"<!-- 2 -->\n",
|
|
"<g class=\"node\" id=\"node4\"><title>2</title>\n",
|
|
"<ellipse cx=\"114.475\" cy=\"-220\" fill=\"#ffffaa\" rx=\"27\" ry=\"18\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"104.475\" y=\"-216.3\">0,1</text>\n",
|
|
"</g>\n",
|
|
"<!-- 0->2 -->\n",
|
|
"<g class=\"edge\" id=\"edge4\"><title>0->2</title>\n",
|
|
"<path d=\"M113.348,-407.885C132.631,-383.949 167.694,-334.994 176.475,-286 178.827,-272.876 183.198,-267.515 176.475,-256 169.639,-244.291 157.279,-236.191 145.384,-230.756\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"138.861,-228.005 146.535,-227.823 142.086,-229.365 145.311,-230.725 145.311,-230.725 145.311,-230.725 142.086,-229.365 144.086,-233.628 138.861,-228.005 138.861,-228.005\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"171.475\" y=\"-318.3\">!b & !c</text>\n",
|
|
"</g>\n",
|
|
"<!-- 1->1 -->\n",
|
|
"<g class=\"edge\" id=\"edge5\"><title>1->1</title>\n",
|
|
"<path d=\"M64.0896,-331.146C75.4482,-332.275 85.475,-329.227 85.475,-322 85.475,-316.354 79.3551,-313.258 71.2615,-312.713\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"64.0896,-312.854 71.0262,-309.567 67.589,-312.785 71.0883,-312.716 71.0883,-312.716 71.0883,-312.716 67.589,-312.785 71.1503,-315.865 64.0896,-312.854 64.0896,-312.854\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"85.475\" y=\"-325.8\">a & !b & c</text>\n",
|
|
"<text fill=\"#1f78b4\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"100.475\" y=\"-311.8\">\u24ff</text>\n",
|
|
"<text fill=\"#ff4da0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"116.475\" y=\"-311.8\">\u2776</text>\n",
|
|
"</g>\n",
|
|
"<!-- 1->2 -->\n",
|
|
"<g class=\"edge\" id=\"edge6\"><title>1->2</title>\n",
|
|
"<path d=\"M61.9369,-310.795C72.4273,-304.855 84.4815,-296.464 92.475,-286 101.567,-274.098 107.035,-258.21 110.246,-245.121\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"111.806,-238.181 113.344,-245.701 111.038,-241.596 110.27,-245.01 110.27,-245.01 110.27,-245.01 111.038,-241.596 107.197,-244.32 111.806,-238.181 111.806,-238.181\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"106.475\" y=\"-274.8\">a & !b & !c</text>\n",
|
|
"<text fill=\"#1f78b4\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"131.475\" y=\"-259.8\">\u24ff</text>\n",
|
|
"</g>\n",
|
|
"<!-- 3 -->\n",
|
|
"<g class=\"node\" id=\"node5\"><title>3</title>\n",
|
|
"<ellipse cx=\"93.475\" cy=\"-18\" fill=\"#ffffaa\" rx=\"27\" ry=\"18\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"83.475\" y=\"-14.3\">2,0</text>\n",
|
|
"</g>\n",
|
|
"<!-- 1->3 -->\n",
|
|
"<g class=\"edge\" id=\"edge7\"><title>1->3</title>\n",
|
|
"<path d=\"M28.3704,-305.878C24.4066,-300.02 20.5022,-293.034 18.475,-286 14.7828,-273.188 18.343,-269.333 18.475,-256 19.364,-166.209 -25.7013,-129.778 22.475,-54 31.0924,-40.4456 46.64,-31.9724 60.9938,-26.766\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"67.9087,-24.4646 62.2617,-29.664 64.5878,-25.5699 61.2669,-26.6752 61.2669,-26.6752 61.2669,-26.6752 64.5878,-25.5699 60.2722,-23.6864 67.9087,-24.4646 67.9087,-24.4646\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"29.975\" y=\"-173.8\">b</text>\n",
|
|
"<text fill=\"#1f78b4\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"10.475\" y=\"-159.8\">\u24ff</text>\n",
|
|
"<text fill=\"#ff4da0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"26.475\" y=\"-159.8\">\u2776</text>\n",
|
|
"<text fill=\"#ff7f00\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"42.475\" y=\"-159.8\">\u2777</text>\n",
|
|
"</g>\n",
|
|
"<!-- 2->1 -->\n",
|
|
"<g class=\"edge\" id=\"edge8\"><title>2->1</title>\n",
|
|
"<path d=\"M87.9982,-223.68C67.4145,-227.312 40.1371,-235.863 26.475,-256 18.031,-268.446 21.8083,-285.06 27.5543,-298.375\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"30.6842,-304.998 24.8452,-300.015 29.1887,-301.834 27.6932,-298.669 27.6932,-298.669 27.6932,-298.669 29.1887,-301.834 30.5412,-297.323 30.6842,-304.998 30.6842,-304.998\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"26.475\" y=\"-274.8\">a & !b & c</text>\n",
|
|
"<text fill=\"#1f78b4\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"41.475\" y=\"-260.8\">\u24ff</text>\n",
|
|
"<text fill=\"#ff4da0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"57.475\" y=\"-260.8\">\u2776</text>\n",
|
|
"</g>\n",
|
|
"<!-- 2->2 -->\n",
|
|
"<g class=\"edge\" id=\"edge9\"><title>2->2</title>\n",
|
|
"<path d=\"M138.09,-229.146C149.448,-230.275 159.475,-227.227 159.475,-220 159.475,-214.354 153.355,-211.258 145.261,-210.713\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"138.09,-210.854 145.026,-207.567 141.589,-210.785 145.088,-210.716 145.088,-210.716 145.088,-210.716 141.589,-210.785 145.15,-213.865 138.09,-210.854 138.09,-210.854\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"159.475\" y=\"-223.8\">a & !b & !c</text>\n",
|
|
"<text fill=\"#1f78b4\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"184.475\" y=\"-208.8\">\u24ff</text>\n",
|
|
"</g>\n",
|
|
"<!-- 2->3 -->\n",
|
|
"<g class=\"edge\" id=\"edge10\"><title>2->3</title>\n",
|
|
"<path d=\"M137.075,-209.51C162.929,-197.264 203.945,-173.257 221.475,-138 228.598,-123.673 226.828,-117.078 221.475,-102 212.278,-76.0968 204.66,-70.2291 182.475,-54 165.44,-41.5381 143.376,-32.8221 125.48,-27.2048\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"118.594,-25.1301 126.205,-24.1336 121.945,-26.1399 125.297,-27.1497 125.297,-27.1497 125.297,-27.1497 121.945,-26.1399 124.388,-30.1657 118.594,-25.1301 118.594,-25.1301\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"232.475\" y=\"-123.8\">b & c</text>\n",
|
|
"<text fill=\"#1f78b4\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"225.475\" y=\"-109.8\">\u24ff</text>\n",
|
|
"<text fill=\"#ff4da0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"241.475\" y=\"-109.8\">\u2776</text>\n",
|
|
"<text fill=\"#ff7f00\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"257.475\" y=\"-109.8\">\u2777</text>\n",
|
|
"</g>\n",
|
|
"<!-- 4 -->\n",
|
|
"<g class=\"node\" id=\"node6\"><title>4</title>\n",
|
|
"<ellipse cx=\"71.475\" cy=\"-120\" fill=\"#ffffaa\" rx=\"27\" ry=\"18\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"61.475\" y=\"-116.3\">2,1</text>\n",
|
|
"</g>\n",
|
|
"<!-- 2->4 -->\n",
|
|
"<g class=\"edge\" id=\"edge11\"><title>2->4</title>\n",
|
|
"<path d=\"M107.181,-202.376C100.158,-186.37 89.4748,-162.023 81.6234,-144.129\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"78.6617,-137.379 84.3589,-142.523 80.068,-140.584 81.4743,-143.789 81.4743,-143.789 81.4743,-143.789 80.068,-140.584 78.5898,-145.055 78.6617,-137.379 78.6617,-137.379\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"97.475\" y=\"-173.8\">b & !c</text>\n",
|
|
"<text fill=\"#1f78b4\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"99.975\" y=\"-159.8\">\u24ff</text>\n",
|
|
"<text fill=\"#ff7f00\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"115.975\" y=\"-159.8\">\u2777</text>\n",
|
|
"</g>\n",
|
|
"<!-- 3->3 -->\n",
|
|
"<g class=\"edge\" id=\"edge12\"><title>3->3</title>\n",
|
|
"<path d=\"M119.822,-22.6692C130.008,-22.8767 138.475,-21.3203 138.475,-18 138.475,-15.5098 133.712,-14.0117 127.034,-13.5059\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"119.822,-13.3308 126.896,-10.3517 123.321,-13.4158 126.82,-13.5008 126.82,-13.5008 126.82,-13.5008 123.321,-13.4158 126.743,-16.6499 119.822,-13.3308 119.822,-13.3308\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"138.475\" y=\"-21.8\">!b & c</text>\n",
|
|
"<text fill=\"#1f78b4\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"140.975\" y=\"-7.8\">\u24ff</text>\n",
|
|
"<text fill=\"#ff4da0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"156.975\" y=\"-7.8\">\u2776</text>\n",
|
|
"</g>\n",
|
|
"<!-- 3->3 -->\n",
|
|
"<g class=\"edge\" id=\"edge13\"><title>3->3</title>\n",
|
|
"<path d=\"M118.023,-25.5159C143.619,-29.5385 175.475,-27.0332 175.475,-18 175.475,-9.77837 149.086,-6.96436 125.046,-9.55795\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"118.023,-10.4841 124.551,-6.44583 121.493,-10.0264 124.963,-9.56879 124.963,-9.56879 124.963,-9.56879 121.493,-10.0264 125.375,-12.6918 118.023,-10.4841 118.023,-10.4841\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"194.975\" y=\"-21.8\">b</text>\n",
|
|
"<text fill=\"#1f78b4\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"175.475\" y=\"-7.8\">\u24ff</text>\n",
|
|
"<text fill=\"#ff4da0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"191.475\" y=\"-7.8\">\u2776</text>\n",
|
|
"<text fill=\"#ff7f00\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"207.475\" y=\"-7.8\">\u2777</text>\n",
|
|
"</g>\n",
|
|
"<!-- 3->4 -->\n",
|
|
"<g class=\"edge\" id=\"edge14\"><title>3->4</title>\n",
|
|
"<path d=\"M69.0276,-25.7806C55.0894,-31.0394 38.7873,-39.8733 30.475,-54 23.7133,-65.4916 24.8914,-71.8921 30.475,-84 33.8958,-91.4178 39.7499,-97.846 45.9805,-103.097\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"51.7492,-107.583 44.2897,-105.773 48.9863,-105.435 46.2234,-103.286 46.2234,-103.286 46.2234,-103.286 48.9863,-105.435 48.1572,-100.799 51.7492,-107.583 51.7492,-107.583\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"30.475\" y=\"-72.8\">!b & !c</text>\n",
|
|
"<text fill=\"#1f78b4\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"42.975\" y=\"-57.8\">\u24ff</text>\n",
|
|
"</g>\n",
|
|
"<!-- 4->3 -->\n",
|
|
"<g class=\"edge\" id=\"edge15\"><title>4->3</title>\n",
|
|
"<path d=\"M75.207,-102.036C78.7785,-85.8025 84.2001,-61.1589 88.2101,-42.9316\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"89.7247,-36.0469 91.297,-43.5602 88.9727,-39.4651 88.2206,-42.8834 88.2206,-42.8834 88.2206,-42.8834 88.9727,-39.4651 85.1442,-42.2065 89.7247,-36.0469 89.7247,-36.0469\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"85.475\" y=\"-72.8\">!b & c</text>\n",
|
|
"<text fill=\"#1f78b4\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"87.975\" y=\"-58.8\">\u24ff</text>\n",
|
|
"<text fill=\"#ff4da0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"103.975\" y=\"-58.8\">\u2776</text>\n",
|
|
"</g>\n",
|
|
"<!-- 4->3 -->\n",
|
|
"<g class=\"edge\" id=\"edge16\"><title>4->3</title>\n",
|
|
"<path d=\"M94.5936,-110.627C106.395,-105.037 119.667,-96.4018 126.475,-84 132.891,-72.3119 131.396,-66.3921 126.475,-54 124.03,-47.8439 119.933,-42.1428 115.442,-37.2057\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"110.473,-32.1629 117.63,-34.9383 112.93,-34.656 115.386,-37.1492 115.386,-37.1492 115.386,-37.1492 112.93,-34.656 113.142,-39.36 110.473,-32.1629 110.473,-32.1629\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"137.475\" y=\"-72.8\">b & c</text>\n",
|
|
"<text fill=\"#1f78b4\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"130.475\" y=\"-58.8\">\u24ff</text>\n",
|
|
"<text fill=\"#ff4da0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"146.475\" y=\"-58.8\">\u2776</text>\n",
|
|
"<text fill=\"#ff7f00\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"162.475\" y=\"-58.8\">\u2777</text>\n",
|
|
"</g>\n",
|
|
"<!-- 4->4 -->\n",
|
|
"<g class=\"edge\" id=\"edge17\"><title>4->4</title>\n",
|
|
"<path d=\"M97.8216,-124.669C108.008,-124.877 116.475,-123.32 116.475,-120 116.475,-117.51 111.712,-116.012 105.034,-115.506\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"97.8216,-115.331 104.896,-112.352 101.321,-115.416 104.82,-115.501 104.82,-115.501 104.82,-115.501 101.321,-115.416 104.743,-118.65 97.8216,-115.331 97.8216,-115.331\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"116.475\" y=\"-123.8\">!b & !c</text>\n",
|
|
"<text fill=\"#1f78b4\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"128.975\" y=\"-108.8\">\u24ff</text>\n",
|
|
"</g>\n",
|
|
"<!-- 4->4 -->\n",
|
|
"<g class=\"edge\" id=\"edge18\"><title>4->4</title>\n",
|
|
"<path d=\"M96.3425,-127.45C123.162,-131.565 157.475,-129.082 157.475,-120 157.475,-111.698 128.806,-108.91 103.396,-111.635\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"96.3425,-112.55 102.879,-108.526 99.8135,-112.1 103.284,-111.65 103.284,-111.65 103.284,-111.65 99.8135,-112.1 103.69,-114.773 96.3425,-112.55 96.3425,-112.55\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"157.475\" y=\"-123.8\">b & !c</text>\n",
|
|
"<text fill=\"#1f78b4\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"159.975\" y=\"-109.8\">\u24ff</text>\n",
|
|
"<text fill=\"#ff7f00\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"175.975\" y=\"-109.8\">\u2777</text>\n",
|
|
"</g>\n",
|
|
"</g>\n",
|
|
"</svg></td></tr></table>"
|
|
],
|
|
"metadata": {},
|
|
"output_type": "pyout",
|
|
"prompt_number": 2,
|
|
"text": [
|
|
"<IPython.core.display.HTML object>"
|
|
]
|
|
}
|
|
],
|
|
"prompt_number": 2
|
|
},
|
|
{
|
|
"cell_type": "markdown",
|
|
"metadata": {},
|
|
"source": [
|
|
"The builtin `spot.product()` function produces an automaton whose language is the intersection of the two input languages. It does so by building an automaton that keeps track of the runs in the two input automata. The states are labeled by pairs of input states so that we can more easily follow what is going on, but those labels are purely cosmetic. The acceptance condition is the conjunction of the two acceptance condition, but the acceptance sets of one input automaton have been shifted to not conflict with the other automaton.\n",
|
|
"\n",
|
|
"In fact, that automaton printer has an option to shift those sets in its output, and this is perfect for illustrating products. For instance `a.show('+3')` will display `a1` with all its acceptance sets shifted by 3. \n",
|
|
"\n",
|
|
"Let's define a function for displaying the three automata involved in a product, using this shift option so we can follow what is going on with the acceptance sets."
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"collapsed": false,
|
|
"input": [
|
|
"def show_prod(a1, a2, res):\n",
|
|
" s1 = a1.num_sets()\n",
|
|
" display(horiz(a1.show(), a2.show('.tavb+{}'.format(s1)), res.show()))\n",
|
|
"\n",
|
|
"show_prod(a1, a2, prod)"
|
|
],
|
|
"language": "python",
|
|
"metadata": {},
|
|
"outputs": [
|
|
{
|
|
"html": [
|
|
"<table><tr><td style=\"vertical-align: top;\"><svg height=\"307pt\" viewBox=\"0.00 0.00 99.00 307.00\" width=\"99pt\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
|
|
"<g class=\"graph\" id=\"graph0\" transform=\"scale(1 1) rotate(0) translate(4 303)\">\n",
|
|
"<title>G</title>\n",
|
|
"<polygon fill=\"white\" points=\"-4,4 -4,-303 95,-303 95,4 -4,4\" stroke=\"none\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"24.5\" y=\"-284.8\">Inf(</text>\n",
|
|
"<text fill=\"#1f78b4\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"46.5\" y=\"-284.8\">\u24ff</text>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"62.5\" y=\"-284.8\">)</text>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"22.5\" y=\"-270.8\">[B\u00fcchi]</text>\n",
|
|
"<!-- I -->\n",
|
|
"<!-- 1 -->\n",
|
|
"<g class=\"node\" id=\"node2\"><title>1</title>\n",
|
|
"<ellipse cx=\"18\" cy=\"-207\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"18\" y=\"-203.3\">1</text>\n",
|
|
"</g>\n",
|
|
"<!-- I->1 -->\n",
|
|
"<g class=\"edge\" id=\"edge1\"><title>I->1</title>\n",
|
|
"<path d=\"M18,-261.845C18,-260.206 18,-245.846 18,-232.368\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"18,-225.058 21.1501,-232.058 18,-228.558 18.0001,-232.058 18.0001,-232.058 18.0001,-232.058 18,-228.558 14.8501,-232.058 18,-225.058 18,-225.058\" stroke=\"black\"/>\n",
|
|
"</g>\n",
|
|
"<!-- 0 -->\n",
|
|
"<g class=\"node\" id=\"node3\"><title>0</title>\n",
|
|
"<ellipse cx=\"18\" cy=\"-120\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"18\" y=\"-116.3\">0</text>\n",
|
|
"</g>\n",
|
|
"<!-- 1->0 -->\n",
|
|
"<g class=\"edge\" id=\"edge4\"><title>1->0</title>\n",
|
|
"<path d=\"M18,-188.799C18,-176.356 18,-159.364 18,-145.504\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"18,-138.175 21.1501,-145.175 18,-141.675 18.0001,-145.175 18.0001,-145.175 18.0001,-145.175 18,-141.675 14.8501,-145.175 18,-138.175 18,-138.175\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"22.5\" y=\"-159.8\">1</text>\n",
|
|
"</g>\n",
|
|
"<!-- 0->0 -->\n",
|
|
"<g class=\"edge\" id=\"edge2\"><title>0->0</title>\n",
|
|
"<path d=\"M34.6641,-127.383C44.625,-129.023 54,-126.562 54,-120 54,-115.078 48.7266,-112.463 41.8876,-112.156\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"34.6641,-112.617 41.449,-109.027 38.1569,-112.394 41.6498,-112.171 41.6498,-112.171 41.6498,-112.171 38.1569,-112.394 41.8507,-115.314 34.6641,-112.617 34.6641,-112.617\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"54\" y=\"-123.8\">a & !b</text>\n",
|
|
"<text fill=\"#1f78b4\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"64.5\" y=\"-108.8\">\u24ff</text>\n",
|
|
"</g>\n",
|
|
"<!-- 2 -->\n",
|
|
"<g class=\"node\" id=\"node4\"><title>2</title>\n",
|
|
"<ellipse cx=\"18\" cy=\"-18\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"18\" y=\"-14.3\">2</text>\n",
|
|
"</g>\n",
|
|
"<!-- 0->2 -->\n",
|
|
"<g class=\"edge\" id=\"edge3\"><title>0->2</title>\n",
|
|
"<path d=\"M18,-101.581C18,-85.5213 18,-61.5179 18,-43.5228\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"18,-36.2191 21.1501,-43.219 18,-39.7191 18.0001,-43.2191 18.0001,-43.2191 18.0001,-43.2191 18,-39.7191 14.8501,-43.2191 18,-36.2191 18,-36.2191\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"21.5\" y=\"-72.8\">b</text>\n",
|
|
"<text fill=\"#1f78b4\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"18\" y=\"-57.8\">\u24ff</text>\n",
|
|
"</g>\n",
|
|
"<!-- 2->2 -->\n",
|
|
"<g class=\"edge\" id=\"edge5\"><title>2->2</title>\n",
|
|
"<path d=\"M33.916,-26.6334C44.1504,-28.8856 54,-26.0078 54,-18 54,-11.869 48.2263,-8.74515 40.9268,-8.6284\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"33.916,-9.36658 40.5477,-5.50081 37.3968,-9.00004 40.8775,-8.6335 40.8775,-8.6335 40.8775,-8.6335 37.3968,-9.00004 41.2074,-11.7662 33.916,-9.36658 33.916,-9.36658\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"57.5\" y=\"-21.8\">1</text>\n",
|
|
"<text fill=\"#1f78b4\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"54\" y=\"-6.8\">\u24ff</text>\n",
|
|
"</g>\n",
|
|
"</g>\n",
|
|
"</svg></td><td style=\"vertical-align: top;\"><svg height=\"220pt\" viewBox=\"0.00 0.00 208.07 220.00\" width=\"208pt\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
|
|
"<g class=\"graph\" id=\"graph0\" transform=\"scale(1 1) rotate(0) translate(4 216)\">\n",
|
|
"<title>G</title>\n",
|
|
"<polygon fill=\"white\" points=\"-4,4 -4,-216 204.071,-216 204.071,4 -4,4\" stroke=\"none\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"53.0356\" y=\"-197.8\">Inf(</text>\n",
|
|
"<text fill=\"#ff4da0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"75.0356\" y=\"-197.8\">\u2776</text>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"91.0356\" y=\"-197.8\">)&Inf(</text>\n",
|
|
"<text fill=\"#ff7f00\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"127.036\" y=\"-197.8\">\u2777</text>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"143.036\" y=\"-197.8\">)</text>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"56.0356\" y=\"-183.8\">[gen. B\u00fcchi 2]</text>\n",
|
|
"<!-- I -->\n",
|
|
"<!-- 0 -->\n",
|
|
"<g class=\"node\" id=\"node2\"><title>0</title>\n",
|
|
"<ellipse cx=\"68.0713\" cy=\"-120\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"68.0713\" y=\"-116.3\">0</text>\n",
|
|
"</g>\n",
|
|
"<!-- I->0 -->\n",
|
|
"<g class=\"edge\" id=\"edge1\"><title>I->0</title>\n",
|
|
"<path d=\"M68.0713,-174.845C68.0713,-173.206 68.0713,-158.846 68.0713,-145.368\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"68.0713,-138.058 71.2214,-145.058 68.0713,-141.558 68.0714,-145.058 68.0714,-145.058 68.0714,-145.058 68.0713,-141.558 64.9214,-145.058 68.0713,-138.058 68.0713,-138.058\" stroke=\"black\"/>\n",
|
|
"</g>\n",
|
|
"<!-- 0->0 -->\n",
|
|
"<g class=\"edge\" id=\"edge2\"><title>0->0</title>\n",
|
|
"<path d=\"M85.853,-123.236C95.3862,-123.786 104.071,-122.707 104.071,-120 104.071,-118.012 99.3874,-116.902 93.1234,-116.671\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"85.853,-116.764 92.8119,-113.524 89.3527,-116.719 92.8524,-116.674 92.8524,-116.674 92.8524,-116.674 89.3527,-116.719 92.893,-119.824 85.853,-116.764 85.853,-116.764\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"104.071\" y=\"-123.8\">!b & c</text>\n",
|
|
"<text fill=\"#ff4da0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"114.571\" y=\"-108.8\">\u2776</text>\n",
|
|
"</g>\n",
|
|
"<!-- 0->0 -->\n",
|
|
"<g class=\"edge\" id=\"edge3\"><title>0->0</title>\n",
|
|
"<path d=\"M85.6405,-124.845C108.831,-128.506 141.071,-126.891 141.071,-120 141.071,-113.782 114.821,-111.86 92.6551,-114.234\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"85.6405,-115.155 92.1705,-111.12 89.1107,-114.699 92.5808,-114.243 92.5808,-114.243 92.5808,-114.243 89.1107,-114.699 92.9912,-117.366 85.6405,-115.155 85.6405,-115.155\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"152.571\" y=\"-123.8\">b</text>\n",
|
|
"<text fill=\"#ff4da0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"141.071\" y=\"-109.8\">\u2776</text>\n",
|
|
"<text fill=\"#ff7f00\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"157.071\" y=\"-109.8\">\u2777</text>\n",
|
|
"</g>\n",
|
|
"<!-- 1 -->\n",
|
|
"<g class=\"node\" id=\"node3\"><title>1</title>\n",
|
|
"<ellipse cx=\"68.0713\" cy=\"-18\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"68.0713\" y=\"-14.3\">1</text>\n",
|
|
"</g>\n",
|
|
"<!-- 0->1 -->\n",
|
|
"<g class=\"edge\" id=\"edge4\"><title>0->1</title>\n",
|
|
"<path d=\"M50.6907,-114.668C35.6563,-109.899 14.8429,-100.607 5.07128,-84 -1.69043,-72.5084 -1.69043,-65.4916 5.07128,-54 13.4688,-39.7284 30.0209,-30.8587 44.052,-25.6199\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"50.6907,-23.3321 45.0991,-28.591 47.3817,-24.4725 44.0727,-25.6129 44.0727,-25.6129 44.0727,-25.6129 47.3817,-24.4725 43.0464,-22.6348 50.6907,-23.3321 50.6907,-23.3321\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"5.07128\" y=\"-65.3\">!b & !c</text>\n",
|
|
"</g>\n",
|
|
"<!-- 1->0 -->\n",
|
|
"<g class=\"edge\" id=\"edge5\"><title>1->0</title>\n",
|
|
"<path d=\"M68.0713,-36.2191C68.0713,-52.2129 68.0713,-76.208 68.0713,-94.2528\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"68.0713,-101.581 64.9214,-94.5813 68.0713,-98.0813 68.0714,-94.5813 68.0714,-94.5813 68.0714,-94.5813 68.0713,-98.0813 71.2214,-94.5814 68.0713,-101.581 68.0713,-101.581\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"68.0713\" y=\"-72.8\">!b & c</text>\n",
|
|
"<text fill=\"#ff4da0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"78.5713\" y=\"-57.8\">\u2776</text>\n",
|
|
"</g>\n",
|
|
"<!-- 1->0 -->\n",
|
|
"<g class=\"edge\" id=\"edge6\"><title>1->0</title>\n",
|
|
"<path d=\"M83.2231,-28.3294C91.6629,-34.4628 101.389,-43.3215 106.071,-54 111.426,-66.211 111.426,-71.789 106.071,-84 102.413,-92.3425 95.6767,-99.5744 88.8801,-105.264\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"83.2231,-109.671 86.8095,-102.884 85.9842,-107.52 88.7453,-105.369 88.7453,-105.369 88.7453,-105.369 85.9842,-107.52 90.6812,-107.854 83.2231,-109.671 83.2231,-109.671\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"110.071\" y=\"-72.8\">b & c</text>\n",
|
|
"<text fill=\"#ff4da0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"111.071\" y=\"-58.8\">\u2776</text>\n",
|
|
"<text fill=\"#ff7f00\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"127.071\" y=\"-58.8\">\u2777</text>\n",
|
|
"</g>\n",
|
|
"<!-- 1->1 -->\n",
|
|
"<g class=\"edge\" id=\"edge7\"><title>1->1</title>\n",
|
|
"<path d=\"M85.853,-22.4941C95.3862,-23.2578 104.071,-21.7598 104.071,-18 104.071,-15.2389 99.3874,-13.6976 93.1234,-13.3761\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"85.853,-13.5059 92.7956,-10.2313 89.3525,-13.4434 92.8519,-13.3808 92.8519,-13.3808 92.8519,-13.3808 89.3525,-13.4434 92.9082,-16.5303 85.853,-13.5059 85.853,-13.5059\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"104.071\" y=\"-14.3\">!b & !c</text>\n",
|
|
"</g>\n",
|
|
"<!-- 1->1 -->\n",
|
|
"<g class=\"edge\" id=\"edge8\"><title>1->1</title>\n",
|
|
"<path d=\"M85.0887,-24.4905C109.42,-29.8803 145.071,-27.7168 145.071,-18 145.071,-9.19415 115.791,-6.59174 92.1916,-10.1928\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"85.0887,-11.5095 91.3972,-7.13627 88.5301,-10.8715 91.9714,-10.2335 91.9714,-10.2335 91.9714,-10.2335 88.5301,-10.8715 92.5456,-13.3307 85.0887,-11.5095 85.0887,-11.5095\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"145.071\" y=\"-21.8\">b & !c</text>\n",
|
|
"<text fill=\"#ff7f00\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"155.571\" y=\"-6.8\">\u2777</text>\n",
|
|
"</g>\n",
|
|
"</g>\n",
|
|
"</svg></td><td style=\"vertical-align: top;\"><svg height=\"360pt\" viewBox=\"0.00 0.00 193.38 360.00\" width=\"193pt\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
|
|
"<g class=\"graph\" id=\"graph0\" transform=\"scale(0.687023 0.687023) rotate(0) translate(4 520)\">\n",
|
|
"<title>G</title>\n",
|
|
"<polygon fill=\"white\" points=\"-4,4 -4,-520 277.475,-520 277.475,4 -4,4\" stroke=\"none\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"63.7375\" y=\"-501.8\">Inf(</text>\n",
|
|
"<text fill=\"#1f78b4\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"85.7375\" y=\"-501.8\">\u24ff</text>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"101.738\" y=\"-501.8\">)&Inf(</text>\n",
|
|
"<text fill=\"#ff4da0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"137.738\" y=\"-501.8\">\u2776</text>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"153.738\" y=\"-501.8\">)&Inf(</text>\n",
|
|
"<text fill=\"#ff7f00\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"189.738\" y=\"-501.8\">\u2777</text>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"205.738\" y=\"-501.8\">)</text>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"92.7375\" y=\"-487.8\">[gen. B\u00fcchi 3]</text>\n",
|
|
"<!-- I -->\n",
|
|
"<!-- 0 -->\n",
|
|
"<g class=\"node\" id=\"node2\"><title>0</title>\n",
|
|
"<ellipse cx=\"100.475\" cy=\"-424\" fill=\"#ffffaa\" rx=\"27\" ry=\"18\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"90.475\" y=\"-420.3\">1,0</text>\n",
|
|
"</g>\n",
|
|
"<!-- I->0 -->\n",
|
|
"<g class=\"edge\" id=\"edge1\"><title>I->0</title>\n",
|
|
"<path d=\"M100.475,-478.845C100.475,-477.206 100.475,-462.846 100.475,-449.368\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"100.475,-442.058 103.625,-449.058 100.475,-445.558 100.475,-449.058 100.475,-449.058 100.475,-449.058 100.475,-445.558 97.3251,-449.058 100.475,-442.058 100.475,-442.058\" stroke=\"black\"/>\n",
|
|
"</g>\n",
|
|
"<!-- 1 -->\n",
|
|
"<g class=\"node\" id=\"node3\"><title>1</title>\n",
|
|
"<ellipse cx=\"40.475\" cy=\"-322\" fill=\"#ffffaa\" rx=\"27\" ry=\"18\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"30.475\" y=\"-318.3\">0,0</text>\n",
|
|
"</g>\n",
|
|
"<!-- 0->1 -->\n",
|
|
"<g class=\"edge\" id=\"edge2\"><title>0->1</title>\n",
|
|
"<path d=\"M76.7094,-415.391C63.8708,-409.939 49.1208,-401.189 41.475,-388 34.4247,-375.839 33.9982,-360.124 35.419,-347.193\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"36.4329,-339.949 38.5821,-347.318 35.9477,-343.415 35.4625,-346.881 35.4625,-346.881 35.4625,-346.881 35.9477,-343.415 32.3429,-346.445 36.4329,-339.949 36.4329,-339.949\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"41.475\" y=\"-376.8\">!b & c</text>\n",
|
|
"<text fill=\"#ff4da0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"51.975\" y=\"-361.8\">\u2776</text>\n",
|
|
"</g>\n",
|
|
"<!-- 0->1 -->\n",
|
|
"<g class=\"edge\" id=\"edge3\"><title>0->1</title>\n",
|
|
"<path d=\"M97.1632,-405.948C93.9364,-392.198 88.0849,-372.783 78.475,-358 74.4421,-351.796 69.062,-345.956 63.6219,-340.889\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"58.2095,-336.096 65.5383,-338.379 60.8296,-338.416 63.4498,-340.737 63.4498,-340.737 63.4498,-340.737 60.8296,-338.416 61.3613,-343.095 58.2095,-336.096 58.2095,-336.096\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"102.975\" y=\"-376.8\">b</text>\n",
|
|
"<text fill=\"#ff4da0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"91.475\" y=\"-362.8\">\u2776</text>\n",
|
|
"<text fill=\"#ff7f00\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"107.475\" y=\"-362.8\">\u2777</text>\n",
|
|
"</g>\n",
|
|
"<!-- 2 -->\n",
|
|
"<g class=\"node\" id=\"node4\"><title>2</title>\n",
|
|
"<ellipse cx=\"114.475\" cy=\"-220\" fill=\"#ffffaa\" rx=\"27\" ry=\"18\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"104.475\" y=\"-216.3\">0,1</text>\n",
|
|
"</g>\n",
|
|
"<!-- 0->2 -->\n",
|
|
"<g class=\"edge\" id=\"edge4\"><title>0->2</title>\n",
|
|
"<path d=\"M113.348,-407.885C132.631,-383.949 167.694,-334.994 176.475,-286 178.827,-272.876 183.198,-267.515 176.475,-256 169.639,-244.291 157.279,-236.191 145.384,-230.756\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"138.861,-228.005 146.535,-227.823 142.086,-229.365 145.311,-230.725 145.311,-230.725 145.311,-230.725 142.086,-229.365 144.086,-233.628 138.861,-228.005 138.861,-228.005\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"171.475\" y=\"-318.3\">!b & !c</text>\n",
|
|
"</g>\n",
|
|
"<!-- 1->1 -->\n",
|
|
"<g class=\"edge\" id=\"edge5\"><title>1->1</title>\n",
|
|
"<path d=\"M64.0896,-331.146C75.4482,-332.275 85.475,-329.227 85.475,-322 85.475,-316.354 79.3551,-313.258 71.2615,-312.713\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"64.0896,-312.854 71.0262,-309.567 67.589,-312.785 71.0883,-312.716 71.0883,-312.716 71.0883,-312.716 67.589,-312.785 71.1503,-315.865 64.0896,-312.854 64.0896,-312.854\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"85.475\" y=\"-325.8\">a & !b & c</text>\n",
|
|
"<text fill=\"#1f78b4\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"100.475\" y=\"-311.8\">\u24ff</text>\n",
|
|
"<text fill=\"#ff4da0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"116.475\" y=\"-311.8\">\u2776</text>\n",
|
|
"</g>\n",
|
|
"<!-- 1->2 -->\n",
|
|
"<g class=\"edge\" id=\"edge6\"><title>1->2</title>\n",
|
|
"<path d=\"M61.9369,-310.795C72.4273,-304.855 84.4815,-296.464 92.475,-286 101.567,-274.098 107.035,-258.21 110.246,-245.121\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"111.806,-238.181 113.344,-245.701 111.038,-241.596 110.27,-245.01 110.27,-245.01 110.27,-245.01 111.038,-241.596 107.197,-244.32 111.806,-238.181 111.806,-238.181\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"106.475\" y=\"-274.8\">a & !b & !c</text>\n",
|
|
"<text fill=\"#1f78b4\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"131.475\" y=\"-259.8\">\u24ff</text>\n",
|
|
"</g>\n",
|
|
"<!-- 3 -->\n",
|
|
"<g class=\"node\" id=\"node5\"><title>3</title>\n",
|
|
"<ellipse cx=\"93.475\" cy=\"-18\" fill=\"#ffffaa\" rx=\"27\" ry=\"18\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"83.475\" y=\"-14.3\">2,0</text>\n",
|
|
"</g>\n",
|
|
"<!-- 1->3 -->\n",
|
|
"<g class=\"edge\" id=\"edge7\"><title>1->3</title>\n",
|
|
"<path d=\"M28.3704,-305.878C24.4066,-300.02 20.5022,-293.034 18.475,-286 14.7828,-273.188 18.343,-269.333 18.475,-256 19.364,-166.209 -25.7013,-129.778 22.475,-54 31.0924,-40.4456 46.64,-31.9724 60.9938,-26.766\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"67.9087,-24.4646 62.2617,-29.664 64.5878,-25.5699 61.2669,-26.6752 61.2669,-26.6752 61.2669,-26.6752 64.5878,-25.5699 60.2722,-23.6864 67.9087,-24.4646 67.9087,-24.4646\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"29.975\" y=\"-173.8\">b</text>\n",
|
|
"<text fill=\"#1f78b4\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"10.475\" y=\"-159.8\">\u24ff</text>\n",
|
|
"<text fill=\"#ff4da0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"26.475\" y=\"-159.8\">\u2776</text>\n",
|
|
"<text fill=\"#ff7f00\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"42.475\" y=\"-159.8\">\u2777</text>\n",
|
|
"</g>\n",
|
|
"<!-- 2->1 -->\n",
|
|
"<g class=\"edge\" id=\"edge8\"><title>2->1</title>\n",
|
|
"<path d=\"M87.9982,-223.68C67.4145,-227.312 40.1371,-235.863 26.475,-256 18.031,-268.446 21.8083,-285.06 27.5543,-298.375\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"30.6842,-304.998 24.8452,-300.015 29.1887,-301.834 27.6932,-298.669 27.6932,-298.669 27.6932,-298.669 29.1887,-301.834 30.5412,-297.323 30.6842,-304.998 30.6842,-304.998\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"26.475\" y=\"-274.8\">a & !b & c</text>\n",
|
|
"<text fill=\"#1f78b4\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"41.475\" y=\"-260.8\">\u24ff</text>\n",
|
|
"<text fill=\"#ff4da0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"57.475\" y=\"-260.8\">\u2776</text>\n",
|
|
"</g>\n",
|
|
"<!-- 2->2 -->\n",
|
|
"<g class=\"edge\" id=\"edge9\"><title>2->2</title>\n",
|
|
"<path d=\"M138.09,-229.146C149.448,-230.275 159.475,-227.227 159.475,-220 159.475,-214.354 153.355,-211.258 145.261,-210.713\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"138.09,-210.854 145.026,-207.567 141.589,-210.785 145.088,-210.716 145.088,-210.716 145.088,-210.716 141.589,-210.785 145.15,-213.865 138.09,-210.854 138.09,-210.854\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"159.475\" y=\"-223.8\">a & !b & !c</text>\n",
|
|
"<text fill=\"#1f78b4\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"184.475\" y=\"-208.8\">\u24ff</text>\n",
|
|
"</g>\n",
|
|
"<!-- 2->3 -->\n",
|
|
"<g class=\"edge\" id=\"edge10\"><title>2->3</title>\n",
|
|
"<path d=\"M137.075,-209.51C162.929,-197.264 203.945,-173.257 221.475,-138 228.598,-123.673 226.828,-117.078 221.475,-102 212.278,-76.0968 204.66,-70.2291 182.475,-54 165.44,-41.5381 143.376,-32.8221 125.48,-27.2048\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"118.594,-25.1301 126.205,-24.1336 121.945,-26.1399 125.297,-27.1497 125.297,-27.1497 125.297,-27.1497 121.945,-26.1399 124.388,-30.1657 118.594,-25.1301 118.594,-25.1301\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"232.475\" y=\"-123.8\">b & c</text>\n",
|
|
"<text fill=\"#1f78b4\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"225.475\" y=\"-109.8\">\u24ff</text>\n",
|
|
"<text fill=\"#ff4da0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"241.475\" y=\"-109.8\">\u2776</text>\n",
|
|
"<text fill=\"#ff7f00\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"257.475\" y=\"-109.8\">\u2777</text>\n",
|
|
"</g>\n",
|
|
"<!-- 4 -->\n",
|
|
"<g class=\"node\" id=\"node6\"><title>4</title>\n",
|
|
"<ellipse cx=\"71.475\" cy=\"-120\" fill=\"#ffffaa\" rx=\"27\" ry=\"18\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"61.475\" y=\"-116.3\">2,1</text>\n",
|
|
"</g>\n",
|
|
"<!-- 2->4 -->\n",
|
|
"<g class=\"edge\" id=\"edge11\"><title>2->4</title>\n",
|
|
"<path d=\"M107.181,-202.376C100.158,-186.37 89.4748,-162.023 81.6234,-144.129\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"78.6617,-137.379 84.3589,-142.523 80.068,-140.584 81.4743,-143.789 81.4743,-143.789 81.4743,-143.789 80.068,-140.584 78.5898,-145.055 78.6617,-137.379 78.6617,-137.379\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"97.475\" y=\"-173.8\">b & !c</text>\n",
|
|
"<text fill=\"#1f78b4\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"99.975\" y=\"-159.8\">\u24ff</text>\n",
|
|
"<text fill=\"#ff7f00\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"115.975\" y=\"-159.8\">\u2777</text>\n",
|
|
"</g>\n",
|
|
"<!-- 3->3 -->\n",
|
|
"<g class=\"edge\" id=\"edge12\"><title>3->3</title>\n",
|
|
"<path d=\"M119.822,-22.6692C130.008,-22.8767 138.475,-21.3203 138.475,-18 138.475,-15.5098 133.712,-14.0117 127.034,-13.5059\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"119.822,-13.3308 126.896,-10.3517 123.321,-13.4158 126.82,-13.5008 126.82,-13.5008 126.82,-13.5008 123.321,-13.4158 126.743,-16.6499 119.822,-13.3308 119.822,-13.3308\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"138.475\" y=\"-21.8\">!b & c</text>\n",
|
|
"<text fill=\"#1f78b4\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"140.975\" y=\"-7.8\">\u24ff</text>\n",
|
|
"<text fill=\"#ff4da0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"156.975\" y=\"-7.8\">\u2776</text>\n",
|
|
"</g>\n",
|
|
"<!-- 3->3 -->\n",
|
|
"<g class=\"edge\" id=\"edge13\"><title>3->3</title>\n",
|
|
"<path d=\"M118.023,-25.5159C143.619,-29.5385 175.475,-27.0332 175.475,-18 175.475,-9.77837 149.086,-6.96436 125.046,-9.55795\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"118.023,-10.4841 124.551,-6.44583 121.493,-10.0264 124.963,-9.56879 124.963,-9.56879 124.963,-9.56879 121.493,-10.0264 125.375,-12.6918 118.023,-10.4841 118.023,-10.4841\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"194.975\" y=\"-21.8\">b</text>\n",
|
|
"<text fill=\"#1f78b4\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"175.475\" y=\"-7.8\">\u24ff</text>\n",
|
|
"<text fill=\"#ff4da0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"191.475\" y=\"-7.8\">\u2776</text>\n",
|
|
"<text fill=\"#ff7f00\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"207.475\" y=\"-7.8\">\u2777</text>\n",
|
|
"</g>\n",
|
|
"<!-- 3->4 -->\n",
|
|
"<g class=\"edge\" id=\"edge14\"><title>3->4</title>\n",
|
|
"<path d=\"M69.0276,-25.7806C55.0894,-31.0394 38.7873,-39.8733 30.475,-54 23.7133,-65.4916 24.8914,-71.8921 30.475,-84 33.8958,-91.4178 39.7499,-97.846 45.9805,-103.097\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"51.7492,-107.583 44.2897,-105.773 48.9863,-105.435 46.2234,-103.286 46.2234,-103.286 46.2234,-103.286 48.9863,-105.435 48.1572,-100.799 51.7492,-107.583 51.7492,-107.583\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"30.475\" y=\"-72.8\">!b & !c</text>\n",
|
|
"<text fill=\"#1f78b4\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"42.975\" y=\"-57.8\">\u24ff</text>\n",
|
|
"</g>\n",
|
|
"<!-- 4->3 -->\n",
|
|
"<g class=\"edge\" id=\"edge15\"><title>4->3</title>\n",
|
|
"<path d=\"M75.207,-102.036C78.7785,-85.8025 84.2001,-61.1589 88.2101,-42.9316\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"89.7247,-36.0469 91.297,-43.5602 88.9727,-39.4651 88.2206,-42.8834 88.2206,-42.8834 88.2206,-42.8834 88.9727,-39.4651 85.1442,-42.2065 89.7247,-36.0469 89.7247,-36.0469\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"85.475\" y=\"-72.8\">!b & c</text>\n",
|
|
"<text fill=\"#1f78b4\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"87.975\" y=\"-58.8\">\u24ff</text>\n",
|
|
"<text fill=\"#ff4da0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"103.975\" y=\"-58.8\">\u2776</text>\n",
|
|
"</g>\n",
|
|
"<!-- 4->3 -->\n",
|
|
"<g class=\"edge\" id=\"edge16\"><title>4->3</title>\n",
|
|
"<path d=\"M94.5936,-110.627C106.395,-105.037 119.667,-96.4018 126.475,-84 132.891,-72.3119 131.396,-66.3921 126.475,-54 124.03,-47.8439 119.933,-42.1428 115.442,-37.2057\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"110.473,-32.1629 117.63,-34.9383 112.93,-34.656 115.386,-37.1492 115.386,-37.1492 115.386,-37.1492 112.93,-34.656 113.142,-39.36 110.473,-32.1629 110.473,-32.1629\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"137.475\" y=\"-72.8\">b & c</text>\n",
|
|
"<text fill=\"#1f78b4\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"130.475\" y=\"-58.8\">\u24ff</text>\n",
|
|
"<text fill=\"#ff4da0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"146.475\" y=\"-58.8\">\u2776</text>\n",
|
|
"<text fill=\"#ff7f00\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"162.475\" y=\"-58.8\">\u2777</text>\n",
|
|
"</g>\n",
|
|
"<!-- 4->4 -->\n",
|
|
"<g class=\"edge\" id=\"edge17\"><title>4->4</title>\n",
|
|
"<path d=\"M97.8216,-124.669C108.008,-124.877 116.475,-123.32 116.475,-120 116.475,-117.51 111.712,-116.012 105.034,-115.506\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"97.8216,-115.331 104.896,-112.352 101.321,-115.416 104.82,-115.501 104.82,-115.501 104.82,-115.501 101.321,-115.416 104.743,-118.65 97.8216,-115.331 97.8216,-115.331\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"116.475\" y=\"-123.8\">!b & !c</text>\n",
|
|
"<text fill=\"#1f78b4\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"128.975\" y=\"-108.8\">\u24ff</text>\n",
|
|
"</g>\n",
|
|
"<!-- 4->4 -->\n",
|
|
"<g class=\"edge\" id=\"edge18\"><title>4->4</title>\n",
|
|
"<path d=\"M96.3425,-127.45C123.162,-131.565 157.475,-129.082 157.475,-120 157.475,-111.698 128.806,-108.91 103.396,-111.635\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"96.3425,-112.55 102.879,-108.526 99.8135,-112.1 103.284,-111.65 103.284,-111.65 103.284,-111.65 99.8135,-112.1 103.69,-114.773 96.3425,-112.55 96.3425,-112.55\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"157.475\" y=\"-123.8\">b & !c</text>\n",
|
|
"<text fill=\"#1f78b4\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"159.975\" y=\"-109.8\">\u24ff</text>\n",
|
|
"<text fill=\"#ff7f00\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"175.975\" y=\"-109.8\">\u2777</text>\n",
|
|
"</g>\n",
|
|
"</g>\n",
|
|
"</svg></td></tr></table>"
|
|
],
|
|
"metadata": {},
|
|
"output_type": "display_data",
|
|
"text": [
|
|
"<IPython.core.display.HTML object>"
|
|
]
|
|
}
|
|
],
|
|
"prompt_number": 3
|
|
},
|
|
{
|
|
"cell_type": "markdown",
|
|
"metadata": {},
|
|
"source": [
|
|
"# Building a product\n",
|
|
"\n",
|
|
"Let's now rewrite `product()` in Python. We will do that in three steps.\n",
|
|
"\n",
|
|
"\n",
|
|
"## First attempt\n",
|
|
"\n",
|
|
"First, we build a product without taking care of the acceptance sets. We just want to get the general shape of the algorithm.\n",
|
|
"\n",
|
|
"We will build an automaton of type `twa_graph`, i.e., an automaton represented explicitely using a graph. In those automata, states are numbered by integers, starting from `0`. (Those states can also be given a different name, which is why the the `product()` shows us something that appears to be labeled by pairs, but the real identifier of each state is an integer.)\n",
|
|
"\n",
|
|
"We will use a dictionary to keep track of the association between a pair `(ls,rs)` of input states, and its number in the output."
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"collapsed": false,
|
|
"input": [
|
|
"def product1(left, right):\n",
|
|
" # A bdd_dict object associates BDD variables (that are \n",
|
|
" # used in BDDs labeleing the edges) to atomic propositions.\n",
|
|
" bdict = left.get_dict()\n",
|
|
" # If the two automata do not have the same BDD dict, then\n",
|
|
" # we cannot easily detect compatible transitions.\n",
|
|
" if right.get_dict() != bdict:\n",
|
|
" raise RuntimeError(\"automata should share their dictionary\")\n",
|
|
" \n",
|
|
" result = spot.make_twa_graph(bdict)\n",
|
|
" # This will be our state dictionary\n",
|
|
" sdict = {}\n",
|
|
" # The list of output states for which we have not yet\n",
|
|
" # computed the successors. Items on this list are triplets\n",
|
|
" # of the form (ls, rs, p) where ls,rs are the state number in\n",
|
|
" # the left and right automata, and p is the state number if\n",
|
|
" # the output automaton.\n",
|
|
" todo = []\n",
|
|
" # Transform a pair of state number (ls, rs) into a state number in\n",
|
|
" # the output automaton, creating a new state if needed. Whenever\n",
|
|
" # a new state is created, we can add it to todo.\n",
|
|
" def dst(ls, rs):\n",
|
|
" pair = (ls, rs)\n",
|
|
" p = sdict.get(pair)\n",
|
|
" if p is None:\n",
|
|
" p = result.new_state()\n",
|
|
" sdict[pair] = p\n",
|
|
" todo.append((ls, rs, p))\n",
|
|
" return p\n",
|
|
" \n",
|
|
" # Setup the initial state. It always exists.\n",
|
|
" result.set_init_state(dst(left.get_init_state_number(), \n",
|
|
" right.get_init_state_number()))\n",
|
|
"\n",
|
|
" # Build all states and edges in the product\n",
|
|
" while todo:\n",
|
|
" lsrc, rsrc, osrc = todo.pop()\n",
|
|
" for lt in left.out(lsrc):\n",
|
|
" for rt in right.out(rsrc):\n",
|
|
" cond = lt.cond & rt.cond\n",
|
|
" if cond != buddy.bddfalse:\n",
|
|
" result.new_edge(osrc, dst(lt.dst, rt.dst), cond)\n",
|
|
" return result\n",
|
|
"\n",
|
|
"p1 = product1(a1, a2)\n",
|
|
"show_prod(a1, a2, p1)"
|
|
],
|
|
"language": "python",
|
|
"metadata": {},
|
|
"outputs": [
|
|
{
|
|
"html": [
|
|
"<table><tr><td style=\"vertical-align: top;\"><svg height=\"307pt\" viewBox=\"0.00 0.00 99.00 307.00\" width=\"99pt\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
|
|
"<g class=\"graph\" id=\"graph0\" transform=\"scale(1 1) rotate(0) translate(4 303)\">\n",
|
|
"<title>G</title>\n",
|
|
"<polygon fill=\"white\" points=\"-4,4 -4,-303 95,-303 95,4 -4,4\" stroke=\"none\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"24.5\" y=\"-284.8\">Inf(</text>\n",
|
|
"<text fill=\"#1f78b4\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"46.5\" y=\"-284.8\">\u24ff</text>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"62.5\" y=\"-284.8\">)</text>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"22.5\" y=\"-270.8\">[B\u00fcchi]</text>\n",
|
|
"<!-- I -->\n",
|
|
"<!-- 1 -->\n",
|
|
"<g class=\"node\" id=\"node2\"><title>1</title>\n",
|
|
"<ellipse cx=\"18\" cy=\"-207\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"18\" y=\"-203.3\">1</text>\n",
|
|
"</g>\n",
|
|
"<!-- I->1 -->\n",
|
|
"<g class=\"edge\" id=\"edge1\"><title>I->1</title>\n",
|
|
"<path d=\"M18,-261.845C18,-260.206 18,-245.846 18,-232.368\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"18,-225.058 21.1501,-232.058 18,-228.558 18.0001,-232.058 18.0001,-232.058 18.0001,-232.058 18,-228.558 14.8501,-232.058 18,-225.058 18,-225.058\" stroke=\"black\"/>\n",
|
|
"</g>\n",
|
|
"<!-- 0 -->\n",
|
|
"<g class=\"node\" id=\"node3\"><title>0</title>\n",
|
|
"<ellipse cx=\"18\" cy=\"-120\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"18\" y=\"-116.3\">0</text>\n",
|
|
"</g>\n",
|
|
"<!-- 1->0 -->\n",
|
|
"<g class=\"edge\" id=\"edge4\"><title>1->0</title>\n",
|
|
"<path d=\"M18,-188.799C18,-176.356 18,-159.364 18,-145.504\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"18,-138.175 21.1501,-145.175 18,-141.675 18.0001,-145.175 18.0001,-145.175 18.0001,-145.175 18,-141.675 14.8501,-145.175 18,-138.175 18,-138.175\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"22.5\" y=\"-159.8\">1</text>\n",
|
|
"</g>\n",
|
|
"<!-- 0->0 -->\n",
|
|
"<g class=\"edge\" id=\"edge2\"><title>0->0</title>\n",
|
|
"<path d=\"M34.6641,-127.383C44.625,-129.023 54,-126.562 54,-120 54,-115.078 48.7266,-112.463 41.8876,-112.156\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"34.6641,-112.617 41.449,-109.027 38.1569,-112.394 41.6498,-112.171 41.6498,-112.171 41.6498,-112.171 38.1569,-112.394 41.8507,-115.314 34.6641,-112.617 34.6641,-112.617\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"54\" y=\"-123.8\">a & !b</text>\n",
|
|
"<text fill=\"#1f78b4\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"64.5\" y=\"-108.8\">\u24ff</text>\n",
|
|
"</g>\n",
|
|
"<!-- 2 -->\n",
|
|
"<g class=\"node\" id=\"node4\"><title>2</title>\n",
|
|
"<ellipse cx=\"18\" cy=\"-18\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"18\" y=\"-14.3\">2</text>\n",
|
|
"</g>\n",
|
|
"<!-- 0->2 -->\n",
|
|
"<g class=\"edge\" id=\"edge3\"><title>0->2</title>\n",
|
|
"<path d=\"M18,-101.581C18,-85.5213 18,-61.5179 18,-43.5228\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"18,-36.2191 21.1501,-43.219 18,-39.7191 18.0001,-43.2191 18.0001,-43.2191 18.0001,-43.2191 18,-39.7191 14.8501,-43.2191 18,-36.2191 18,-36.2191\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"21.5\" y=\"-72.8\">b</text>\n",
|
|
"<text fill=\"#1f78b4\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"18\" y=\"-57.8\">\u24ff</text>\n",
|
|
"</g>\n",
|
|
"<!-- 2->2 -->\n",
|
|
"<g class=\"edge\" id=\"edge5\"><title>2->2</title>\n",
|
|
"<path d=\"M33.916,-26.6334C44.1504,-28.8856 54,-26.0078 54,-18 54,-11.869 48.2263,-8.74515 40.9268,-8.6284\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"33.916,-9.36658 40.5477,-5.50081 37.3968,-9.00004 40.8775,-8.6335 40.8775,-8.6335 40.8775,-8.6335 37.3968,-9.00004 41.2074,-11.7662 33.916,-9.36658 33.916,-9.36658\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"57.5\" y=\"-21.8\">1</text>\n",
|
|
"<text fill=\"#1f78b4\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"54\" y=\"-6.8\">\u24ff</text>\n",
|
|
"</g>\n",
|
|
"</g>\n",
|
|
"</svg></td><td style=\"vertical-align: top;\"><svg height=\"220pt\" viewBox=\"0.00 0.00 208.07 220.00\" width=\"208pt\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
|
|
"<g class=\"graph\" id=\"graph0\" transform=\"scale(1 1) rotate(0) translate(4 216)\">\n",
|
|
"<title>G</title>\n",
|
|
"<polygon fill=\"white\" points=\"-4,4 -4,-216 204.071,-216 204.071,4 -4,4\" stroke=\"none\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"53.0356\" y=\"-197.8\">Inf(</text>\n",
|
|
"<text fill=\"#ff4da0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"75.0356\" y=\"-197.8\">\u2776</text>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"91.0356\" y=\"-197.8\">)&Inf(</text>\n",
|
|
"<text fill=\"#ff7f00\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"127.036\" y=\"-197.8\">\u2777</text>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"143.036\" y=\"-197.8\">)</text>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"56.0356\" y=\"-183.8\">[gen. B\u00fcchi 2]</text>\n",
|
|
"<!-- I -->\n",
|
|
"<!-- 0 -->\n",
|
|
"<g class=\"node\" id=\"node2\"><title>0</title>\n",
|
|
"<ellipse cx=\"68.0713\" cy=\"-120\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"68.0713\" y=\"-116.3\">0</text>\n",
|
|
"</g>\n",
|
|
"<!-- I->0 -->\n",
|
|
"<g class=\"edge\" id=\"edge1\"><title>I->0</title>\n",
|
|
"<path d=\"M68.0713,-174.845C68.0713,-173.206 68.0713,-158.846 68.0713,-145.368\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"68.0713,-138.058 71.2214,-145.058 68.0713,-141.558 68.0714,-145.058 68.0714,-145.058 68.0714,-145.058 68.0713,-141.558 64.9214,-145.058 68.0713,-138.058 68.0713,-138.058\" stroke=\"black\"/>\n",
|
|
"</g>\n",
|
|
"<!-- 0->0 -->\n",
|
|
"<g class=\"edge\" id=\"edge2\"><title>0->0</title>\n",
|
|
"<path d=\"M85.853,-123.236C95.3862,-123.786 104.071,-122.707 104.071,-120 104.071,-118.012 99.3874,-116.902 93.1234,-116.671\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"85.853,-116.764 92.8119,-113.524 89.3527,-116.719 92.8524,-116.674 92.8524,-116.674 92.8524,-116.674 89.3527,-116.719 92.893,-119.824 85.853,-116.764 85.853,-116.764\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"104.071\" y=\"-123.8\">!b & c</text>\n",
|
|
"<text fill=\"#ff4da0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"114.571\" y=\"-108.8\">\u2776</text>\n",
|
|
"</g>\n",
|
|
"<!-- 0->0 -->\n",
|
|
"<g class=\"edge\" id=\"edge3\"><title>0->0</title>\n",
|
|
"<path d=\"M85.6405,-124.845C108.831,-128.506 141.071,-126.891 141.071,-120 141.071,-113.782 114.821,-111.86 92.6551,-114.234\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"85.6405,-115.155 92.1705,-111.12 89.1107,-114.699 92.5808,-114.243 92.5808,-114.243 92.5808,-114.243 89.1107,-114.699 92.9912,-117.366 85.6405,-115.155 85.6405,-115.155\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"152.571\" y=\"-123.8\">b</text>\n",
|
|
"<text fill=\"#ff4da0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"141.071\" y=\"-109.8\">\u2776</text>\n",
|
|
"<text fill=\"#ff7f00\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"157.071\" y=\"-109.8\">\u2777</text>\n",
|
|
"</g>\n",
|
|
"<!-- 1 -->\n",
|
|
"<g class=\"node\" id=\"node3\"><title>1</title>\n",
|
|
"<ellipse cx=\"68.0713\" cy=\"-18\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"68.0713\" y=\"-14.3\">1</text>\n",
|
|
"</g>\n",
|
|
"<!-- 0->1 -->\n",
|
|
"<g class=\"edge\" id=\"edge4\"><title>0->1</title>\n",
|
|
"<path d=\"M50.6907,-114.668C35.6563,-109.899 14.8429,-100.607 5.07128,-84 -1.69043,-72.5084 -1.69043,-65.4916 5.07128,-54 13.4688,-39.7284 30.0209,-30.8587 44.052,-25.6199\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"50.6907,-23.3321 45.0991,-28.591 47.3817,-24.4725 44.0727,-25.6129 44.0727,-25.6129 44.0727,-25.6129 47.3817,-24.4725 43.0464,-22.6348 50.6907,-23.3321 50.6907,-23.3321\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"5.07128\" y=\"-65.3\">!b & !c</text>\n",
|
|
"</g>\n",
|
|
"<!-- 1->0 -->\n",
|
|
"<g class=\"edge\" id=\"edge5\"><title>1->0</title>\n",
|
|
"<path d=\"M68.0713,-36.2191C68.0713,-52.2129 68.0713,-76.208 68.0713,-94.2528\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"68.0713,-101.581 64.9214,-94.5813 68.0713,-98.0813 68.0714,-94.5813 68.0714,-94.5813 68.0714,-94.5813 68.0713,-98.0813 71.2214,-94.5814 68.0713,-101.581 68.0713,-101.581\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"68.0713\" y=\"-72.8\">!b & c</text>\n",
|
|
"<text fill=\"#ff4da0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"78.5713\" y=\"-57.8\">\u2776</text>\n",
|
|
"</g>\n",
|
|
"<!-- 1->0 -->\n",
|
|
"<g class=\"edge\" id=\"edge6\"><title>1->0</title>\n",
|
|
"<path d=\"M83.2231,-28.3294C91.6629,-34.4628 101.389,-43.3215 106.071,-54 111.426,-66.211 111.426,-71.789 106.071,-84 102.413,-92.3425 95.6767,-99.5744 88.8801,-105.264\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"83.2231,-109.671 86.8095,-102.884 85.9842,-107.52 88.7453,-105.369 88.7453,-105.369 88.7453,-105.369 85.9842,-107.52 90.6812,-107.854 83.2231,-109.671 83.2231,-109.671\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"110.071\" y=\"-72.8\">b & c</text>\n",
|
|
"<text fill=\"#ff4da0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"111.071\" y=\"-58.8\">\u2776</text>\n",
|
|
"<text fill=\"#ff7f00\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"127.071\" y=\"-58.8\">\u2777</text>\n",
|
|
"</g>\n",
|
|
"<!-- 1->1 -->\n",
|
|
"<g class=\"edge\" id=\"edge7\"><title>1->1</title>\n",
|
|
"<path d=\"M85.853,-22.4941C95.3862,-23.2578 104.071,-21.7598 104.071,-18 104.071,-15.2389 99.3874,-13.6976 93.1234,-13.3761\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"85.853,-13.5059 92.7956,-10.2313 89.3525,-13.4434 92.8519,-13.3808 92.8519,-13.3808 92.8519,-13.3808 89.3525,-13.4434 92.9082,-16.5303 85.853,-13.5059 85.853,-13.5059\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"104.071\" y=\"-14.3\">!b & !c</text>\n",
|
|
"</g>\n",
|
|
"<!-- 1->1 -->\n",
|
|
"<g class=\"edge\" id=\"edge8\"><title>1->1</title>\n",
|
|
"<path d=\"M85.0887,-24.4905C109.42,-29.8803 145.071,-27.7168 145.071,-18 145.071,-9.19415 115.791,-6.59174 92.1916,-10.1928\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"85.0887,-11.5095 91.3972,-7.13627 88.5301,-10.8715 91.9714,-10.2335 91.9714,-10.2335 91.9714,-10.2335 88.5301,-10.8715 92.5456,-13.3307 85.0887,-11.5095 85.0887,-11.5095\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"145.071\" y=\"-21.8\">b & !c</text>\n",
|
|
"<text fill=\"#ff7f00\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"155.571\" y=\"-6.8\">\u2777</text>\n",
|
|
"</g>\n",
|
|
"</g>\n",
|
|
"</svg></td><td style=\"vertical-align: top;\"><svg height=\"360pt\" viewBox=\"0.00 0.00 241.25 360.00\" width=\"241pt\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
|
|
"<g class=\"graph\" id=\"graph0\" transform=\"scale(0.769231 0.769231) rotate(0) translate(4 464)\">\n",
|
|
"<title>G</title>\n",
|
|
"<polygon fill=\"white\" points=\"-4,4 -4,-464 309.624,-464 309.624,4 -4,4\" stroke=\"none\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"149.812\" y=\"-444.8\">t</text>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"141.812\" y=\"-429.8\">[all]</text>\n",
|
|
"<!-- I -->\n",
|
|
"<!-- 0 -->\n",
|
|
"<g class=\"node\" id=\"node2\"><title>0</title>\n",
|
|
"<ellipse cx=\"170.624\" cy=\"-366\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"170.624\" y=\"-362.3\">0</text>\n",
|
|
"</g>\n",
|
|
"<!-- I->0 -->\n",
|
|
"<g class=\"edge\" id=\"edge1\"><title>I->0</title>\n",
|
|
"<path d=\"M170.624,-420.845C170.624,-419.206 170.624,-404.846 170.624,-391.368\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"170.624,-384.058 173.774,-391.058 170.624,-387.558 170.624,-391.058 170.624,-391.058 170.624,-391.058 170.624,-387.558 167.474,-391.058 170.624,-384.058 170.624,-384.058\" stroke=\"black\"/>\n",
|
|
"</g>\n",
|
|
"<!-- 1 -->\n",
|
|
"<g class=\"node\" id=\"node3\"><title>1</title>\n",
|
|
"<ellipse cx=\"110.624\" cy=\"-279\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"110.624\" y=\"-275.3\">1</text>\n",
|
|
"</g>\n",
|
|
"<!-- 0->1 -->\n",
|
|
"<g class=\"edge\" id=\"edge2\"><title>0->1</title>\n",
|
|
"<path d=\"M153.56,-360.008C139.579,-354.923 120.679,-345.537 111.624,-330 107.115,-322.264 106.077,-312.647 106.444,-303.92\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"107.039,-296.859 109.59,-304.099 106.745,-300.347 106.452,-303.834 106.452,-303.834 106.452,-303.834 106.745,-300.347 103.313,-303.57 107.039,-296.859 107.039,-296.859\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"111.624\" y=\"-318.8\">!b & c</text>\n",
|
|
"</g>\n",
|
|
"<!-- 0->1 -->\n",
|
|
"<g class=\"edge\" id=\"edge3\"><title>0->1</title>\n",
|
|
"<path d=\"M165.262,-348.34C161.524,-338.16 155.902,-325.185 148.624,-315 143.513,-307.849 136.747,-301.044 130.341,-295.367\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"124.617,-290.495 131.989,-292.634 127.282,-292.764 129.947,-295.032 129.947,-295.032 129.947,-295.032 127.282,-292.764 127.905,-297.431 124.617,-290.495 124.617,-290.495\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"156.624\" y=\"-318.8\">b</text>\n",
|
|
"</g>\n",
|
|
"<!-- 2 -->\n",
|
|
"<g class=\"node\" id=\"node4\"><title>2</title>\n",
|
|
"<ellipse cx=\"179.624\" cy=\"-192\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"179.624\" y=\"-188.3\">2</text>\n",
|
|
"</g>\n",
|
|
"<!-- 0->2 -->\n",
|
|
"<g class=\"edge\" id=\"edge4\"><title>0->2</title>\n",
|
|
"<path d=\"M181.559,-351.652C191.963,-338.433 207.491,-317.285 217.624,-297 228.929,-274.368 231.571,-267.972 235.624,-243 236.692,-236.419 238.856,-233.831 235.624,-228 228.637,-215.393 215.007,-206.728 202.943,-201.173\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"196.455,-198.401 204.13,-198.254 199.674,-199.776 202.892,-201.151 202.892,-201.151 202.892,-201.151 199.674,-199.776 201.655,-204.048 196.455,-198.401 196.455,-198.401\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"231.624\" y=\"-275.3\">!b & !c</text>\n",
|
|
"</g>\n",
|
|
"<!-- 1->1 -->\n",
|
|
"<g class=\"edge\" id=\"edge5\"><title>1->1</title>\n",
|
|
"<path d=\"M127.288,-286.383C137.249,-288.023 146.624,-285.562 146.624,-279 146.624,-274.078 141.35,-271.463 134.511,-271.156\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"127.288,-271.617 134.073,-268.027 130.781,-271.394 134.274,-271.171 134.274,-271.171 134.274,-271.171 130.781,-271.394 134.474,-274.314 127.288,-271.617 127.288,-271.617\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"146.624\" y=\"-275.3\">a & !b & c</text>\n",
|
|
"</g>\n",
|
|
"<!-- 1->2 -->\n",
|
|
"<g class=\"edge\" id=\"edge6\"><title>1->2</title>\n",
|
|
"<path d=\"M126.241,-269.273C136.278,-263.024 149.003,-253.823 157.624,-243 163.933,-235.079 168.807,-225.067 172.344,-216.086\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"174.791,-209.471 175.317,-217.129 173.577,-212.753 172.363,-216.036 172.363,-216.036 172.363,-216.036 173.577,-212.753 169.408,-214.943 174.791,-209.471 174.791,-209.471\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"165.624\" y=\"-231.8\">a & !b & !c</text>\n",
|
|
"</g>\n",
|
|
"<!-- 3 -->\n",
|
|
"<g class=\"node\" id=\"node5\"><title>3</title>\n",
|
|
"<ellipse cx=\"158.624\" cy=\"-18\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"158.624\" y=\"-14.3\">3</text>\n",
|
|
"</g>\n",
|
|
"<!-- 1->3 -->\n",
|
|
"<g class=\"edge\" id=\"edge7\"><title>1->3</title>\n",
|
|
"<path d=\"M98.2752,-265.526C92.9783,-259.304 87.3814,-251.336 84.6238,-243 67.727,-191.919 -99.6014,-352.461 89.6238,-54 99.4784,-38.4565 118.55,-29.5253 134.149,-24.5809\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"141.027,-22.5803 135.185,-27.5602 137.666,-23.5579 134.305,-24.5356 134.305,-24.5356 134.305,-24.5356 137.666,-23.5579 133.425,-21.511 141.027,-22.5803 141.027,-22.5803\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"35.6238\" y=\"-144.8\">b</text>\n",
|
|
"</g>\n",
|
|
"<!-- 2->1 -->\n",
|
|
"<g class=\"edge\" id=\"edge8\"><title>2->1</title>\n",
|
|
"<path d=\"M161.447,-194.412C140.578,-197.118 107.224,-205.006 91.6238,-228 85.2941,-237.329 89.2413,-249.055 95.1414,-258.806\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"99.2123,-264.884 92.6996,-260.821 97.2645,-261.976 95.3167,-259.068 95.3167,-259.068 95.3167,-259.068 97.2645,-261.976 97.9339,-257.315 99.2123,-264.884 99.2123,-264.884\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"91.6238\" y=\"-231.8\">a & !b & c</text>\n",
|
|
"</g>\n",
|
|
"<!-- 2->2 -->\n",
|
|
"<g class=\"edge\" id=\"edge9\"><title>2->2</title>\n",
|
|
"<path d=\"M196.288,-199.383C206.249,-201.023 215.624,-198.562 215.624,-192 215.624,-187.078 210.35,-184.463 203.511,-184.156\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"196.288,-184.617 203.073,-181.027 199.781,-184.394 203.274,-184.171 203.274,-184.171 203.274,-184.171 199.781,-184.394 203.474,-187.314 196.288,-184.617 196.288,-184.617\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"215.624\" y=\"-188.3\">a & !b & !c</text>\n",
|
|
"</g>\n",
|
|
"<!-- 2->3 -->\n",
|
|
"<g class=\"edge\" id=\"edge10\"><title>2->3</title>\n",
|
|
"<path d=\"M195.826,-183.942C216.664,-173.859 251.92,-153.155 266.624,-123 273.636,-108.619 273.618,-101.39 266.624,-87 250.442,-53.7064 209.383,-34.9069 182.809,-25.8634\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"176.06,-23.6693 183.691,-22.8379 179.389,-24.7514 182.717,-25.8336 182.717,-25.8336 182.717,-25.8336 179.389,-24.7514 181.744,-28.8292 176.06,-23.6693 176.06,-23.6693\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"271.624\" y=\"-101.3\">b & c</text>\n",
|
|
"</g>\n",
|
|
"<!-- 4 -->\n",
|
|
"<g class=\"node\" id=\"node6\"><title>4</title>\n",
|
|
"<ellipse cx=\"125.624\" cy=\"-105\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"125.624\" y=\"-101.3\">4</text>\n",
|
|
"</g>\n",
|
|
"<!-- 2->4 -->\n",
|
|
"<g class=\"edge\" id=\"edge11\"><title>2->4</title>\n",
|
|
"<path d=\"M170.218,-176.194C161.545,-162.543 148.584,-142.14 138.866,-126.844\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"134.922,-120.636 141.335,-124.856 136.799,-123.59 138.676,-126.545 138.676,-126.545 138.676,-126.545 136.799,-123.59 136.017,-128.234 134.922,-120.636 134.922,-120.636\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"155.624\" y=\"-144.8\">b & !c</text>\n",
|
|
"</g>\n",
|
|
"<!-- 3->3 -->\n",
|
|
"<g class=\"edge\" id=\"edge12\"><title>3->3</title>\n",
|
|
"<path d=\"M176.406,-21.775C185.939,-22.4165 194.624,-21.1582 194.624,-18 194.624,-15.6807 189.94,-14.386 183.676,-14.1159\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"176.406,-14.225 183.357,-10.9702 179.905,-14.1724 183.405,-14.1199 183.405,-14.1199 183.405,-14.1199 179.905,-14.1724 183.452,-17.2695 176.406,-14.225 176.406,-14.225\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"194.624\" y=\"-14.3\">!b & c</text>\n",
|
|
"</g>\n",
|
|
"<!-- 3->3 -->\n",
|
|
"<g class=\"edge\" id=\"edge13\"><title>3->3</title>\n",
|
|
"<path d=\"M175.839,-23.5866C199.054,-27.9423 231.624,-26.0801 231.624,-18 231.624,-10.709 205.105,-8.48073 182.869,-11.3152\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"175.839,-12.4134 182.269,-8.22064 179.297,-11.8731 182.755,-11.3329 182.755,-11.3329 182.755,-11.3329 179.297,-11.8731 183.241,-14.4452 175.839,-12.4134 175.839,-12.4134\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"231.624\" y=\"-14.3\">b</text>\n",
|
|
"</g>\n",
|
|
"<!-- 3->4 -->\n",
|
|
"<g class=\"edge\" id=\"edge14\"><title>3->4</title>\n",
|
|
"<path d=\"M141.243,-23.3321C126.209,-28.1006 105.395,-37.393 95.6238,-54 88.804,-65.5905 97.1404,-78.6158 106.74,-88.4658\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"111.801,-93.3028 104.564,-90.7437 109.271,-90.8846 106.74,-88.4665 106.74,-88.4665 106.74,-88.4665 109.271,-90.8846 108.917,-86.1892 111.801,-93.3028 111.801,-93.3028\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"95.6238\" y=\"-57.8\">!b & !c</text>\n",
|
|
"</g>\n",
|
|
"<!-- 4->3 -->\n",
|
|
"<g class=\"edge\" id=\"edge15\"><title>4->3</title>\n",
|
|
"<path d=\"M131.831,-88.0122C136.901,-74.9525 144.13,-56.332 149.802,-41.7234\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"152.445,-34.9162 152.848,-42.5817 151.178,-38.1789 149.911,-41.4416 149.911,-41.4416 149.911,-41.4416 151.178,-38.1789 146.975,-40.3016 152.445,-34.9162 152.445,-34.9162\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"143.624\" y=\"-57.8\">!b & c</text>\n",
|
|
"</g>\n",
|
|
"<!-- 4->3 -->\n",
|
|
"<g class=\"edge\" id=\"edge16\"><title>4->3</title>\n",
|
|
"<path d=\"M142.767,-99.0529C156.796,-93.9963 175.724,-84.6273 184.624,-69 190.776,-58.1972 184.416,-45.8005 176.449,-36.0534\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"171.654,-30.6527 178.657,-33.7964 173.978,-33.2702 176.301,-35.8876 176.301,-35.8876 176.301,-35.8876 173.978,-33.2702 173.946,-37.9789 171.654,-30.6527 171.654,-30.6527\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"186.624\" y=\"-57.8\">b & c</text>\n",
|
|
"</g>\n",
|
|
"<!-- 4->4 -->\n",
|
|
"<g class=\"edge\" id=\"edge17\"><title>4->4</title>\n",
|
|
"<path d=\"M143.406,-108.775C152.939,-109.417 161.624,-108.158 161.624,-105 161.624,-102.681 156.94,-101.386 150.676,-101.116\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"143.406,-101.225 150.357,-97.9702 146.905,-101.172 150.405,-101.12 150.405,-101.12 150.405,-101.12 146.905,-101.172 150.452,-104.27 143.406,-101.225 143.406,-101.225\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"161.624\" y=\"-101.3\">!b & !c</text>\n",
|
|
"</g>\n",
|
|
"<!-- 4->4 -->\n",
|
|
"<g class=\"edge\" id=\"edge18\"><title>4->4</title>\n",
|
|
"<path d=\"M143.009,-110.52C167.33,-114.961 202.624,-113.121 202.624,-105 202.624,-97.6403 173.637,-95.4392 150.1,-98.3967\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"143.009,-99.4802 149.453,-95.309 146.469,-98.9515 149.929,-98.4229 149.929,-98.4229 149.929,-98.4229 146.469,-98.9515 150.404,-101.537 143.009,-99.4802 143.009,-99.4802\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"202.624\" y=\"-101.3\">b & !c</text>\n",
|
|
"</g>\n",
|
|
"</g>\n",
|
|
"</svg></td></tr></table>"
|
|
],
|
|
"metadata": {},
|
|
"output_type": "display_data",
|
|
"text": [
|
|
"<IPython.core.display.HTML object>"
|
|
]
|
|
}
|
|
],
|
|
"prompt_number": 4
|
|
},
|
|
{
|
|
"cell_type": "markdown",
|
|
"metadata": {},
|
|
"source": [
|
|
"Besides the obvious lack of acceptance condition (which defaults to `t`) and acceptance sets, there is a less obvious problem: we never declared the set of atomic propositions used by the result automaton. This as two consequences:\n",
|
|
"- calling `p1.ap()` will return an empty set of atomic propositions"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"collapsed": false,
|
|
"input": [
|
|
"print(a1.ap())\n",
|
|
"print(a2.ap())\n",
|
|
"print(p1.ap())"
|
|
],
|
|
"language": "python",
|
|
"metadata": {},
|
|
"outputs": [
|
|
{
|
|
"output_type": "stream",
|
|
"stream": "stdout",
|
|
"text": [
|
|
"(a, b)\n",
|
|
"(c, b)\n",
|
|
"()\n"
|
|
]
|
|
}
|
|
],
|
|
"prompt_number": 5
|
|
},
|
|
{
|
|
"cell_type": "markdown",
|
|
"metadata": {},
|
|
"source": [
|
|
"- the `bdd_dict` instance that is shared by the three automata knows that the atomic propositions `a` and `b` are used by automata `a1` and that `b` and `c` are used by `a2`. But it is unaware of `p1`. That means that if we delete automata `a1` and `a2`, then the `bdd_dict` will release the associated BDD variables, and attempting to print automaton `p1` will either crash (because it uses bdd variables that are not associated to any atomic proposition) or display different atomic propositions (in case the BDD variables have been associated to different propositions in the meantime).\n",
|
|
"\n",
|
|
"These two issues are fixed by either calling `p1.register_ap(...)` for each atomic proposition, or in our case `p1.copy_ap_of(...)` to copy the atomic propositions of each input automaton. "
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "markdown",
|
|
"metadata": {},
|
|
"source": [
|
|
"## Second attempt: a working product\n",
|
|
"\n",
|
|
"This fixes the list of atomtic propositions, as discussed above, and also sets the correct acceptance condition.\n",
|
|
"The `set_acceptance` method takes two arguments: a number of sets, and an acceptance function. In our case, both of these arguments are readily computed from the number of states and acceptance functions of the input automata."
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"collapsed": false,
|
|
"input": [
|
|
"def product2(left, right):\n",
|
|
" bdict = left.get_dict()\n",
|
|
" if right.get_dict() != bdict:\n",
|
|
" raise RuntimeError(\"automata should share their dictionary\")\n",
|
|
" \n",
|
|
" result = spot.make_twa_graph(bdict)\n",
|
|
" # Copy the atomic propositions of the two input automata\n",
|
|
" result.copy_ap_of(left)\n",
|
|
" result.copy_ap_of(right)\n",
|
|
" \n",
|
|
" sdict = {}\n",
|
|
" todo = []\n",
|
|
" def dst(ls, rs):\n",
|
|
" pair = (ls, rs)\n",
|
|
" p = sdict.get(pair)\n",
|
|
" if p is None:\n",
|
|
" p = result.new_state()\n",
|
|
" sdict[pair] = p\n",
|
|
" todo.append((ls, rs, p))\n",
|
|
" return p\n",
|
|
" \n",
|
|
" result.set_init_state(dst(left.get_init_state_number(), \n",
|
|
" right.get_init_state_number()))\n",
|
|
"\n",
|
|
" # The acceptance sets of the right automaton will be shifted by this amount\n",
|
|
" shift = left.num_sets()\n",
|
|
" result.set_acceptance(shift + right.num_sets(),\n",
|
|
" left.get_acceptance() & (right.get_acceptance() << shift))\n",
|
|
" \n",
|
|
" while todo:\n",
|
|
" lsrc, rsrc, osrc = todo.pop()\n",
|
|
" for lt in left.out(lsrc):\n",
|
|
" for rt in right.out(rsrc):\n",
|
|
" cond = lt.cond & rt.cond\n",
|
|
" if cond != buddy.bddfalse:\n",
|
|
" # membership of this transitions to the new acceptance sets\n",
|
|
" acc = lt.acc | (rt.acc << shift)\n",
|
|
" result.new_edge(osrc, dst(lt.dst, rt.dst), cond, acc)\n",
|
|
" return result\n",
|
|
"\n",
|
|
"p2 = product2(a1, a2)\n",
|
|
"show_prod(a1, a2, p2)\n",
|
|
"print(p2.ap())"
|
|
],
|
|
"language": "python",
|
|
"metadata": {},
|
|
"outputs": [
|
|
{
|
|
"html": [
|
|
"<table><tr><td style=\"vertical-align: top;\"><svg height=\"307pt\" viewBox=\"0.00 0.00 99.00 307.00\" width=\"99pt\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
|
|
"<g class=\"graph\" id=\"graph0\" transform=\"scale(1 1) rotate(0) translate(4 303)\">\n",
|
|
"<title>G</title>\n",
|
|
"<polygon fill=\"white\" points=\"-4,4 -4,-303 95,-303 95,4 -4,4\" stroke=\"none\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"24.5\" y=\"-284.8\">Inf(</text>\n",
|
|
"<text fill=\"#1f78b4\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"46.5\" y=\"-284.8\">\u24ff</text>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"62.5\" y=\"-284.8\">)</text>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"22.5\" y=\"-270.8\">[B\u00fcchi]</text>\n",
|
|
"<!-- I -->\n",
|
|
"<!-- 1 -->\n",
|
|
"<g class=\"node\" id=\"node2\"><title>1</title>\n",
|
|
"<ellipse cx=\"18\" cy=\"-207\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"18\" y=\"-203.3\">1</text>\n",
|
|
"</g>\n",
|
|
"<!-- I->1 -->\n",
|
|
"<g class=\"edge\" id=\"edge1\"><title>I->1</title>\n",
|
|
"<path d=\"M18,-261.845C18,-260.206 18,-245.846 18,-232.368\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"18,-225.058 21.1501,-232.058 18,-228.558 18.0001,-232.058 18.0001,-232.058 18.0001,-232.058 18,-228.558 14.8501,-232.058 18,-225.058 18,-225.058\" stroke=\"black\"/>\n",
|
|
"</g>\n",
|
|
"<!-- 0 -->\n",
|
|
"<g class=\"node\" id=\"node3\"><title>0</title>\n",
|
|
"<ellipse cx=\"18\" cy=\"-120\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"18\" y=\"-116.3\">0</text>\n",
|
|
"</g>\n",
|
|
"<!-- 1->0 -->\n",
|
|
"<g class=\"edge\" id=\"edge4\"><title>1->0</title>\n",
|
|
"<path d=\"M18,-188.799C18,-176.356 18,-159.364 18,-145.504\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"18,-138.175 21.1501,-145.175 18,-141.675 18.0001,-145.175 18.0001,-145.175 18.0001,-145.175 18,-141.675 14.8501,-145.175 18,-138.175 18,-138.175\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"22.5\" y=\"-159.8\">1</text>\n",
|
|
"</g>\n",
|
|
"<!-- 0->0 -->\n",
|
|
"<g class=\"edge\" id=\"edge2\"><title>0->0</title>\n",
|
|
"<path d=\"M34.6641,-127.383C44.625,-129.023 54,-126.562 54,-120 54,-115.078 48.7266,-112.463 41.8876,-112.156\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"34.6641,-112.617 41.449,-109.027 38.1569,-112.394 41.6498,-112.171 41.6498,-112.171 41.6498,-112.171 38.1569,-112.394 41.8507,-115.314 34.6641,-112.617 34.6641,-112.617\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"54\" y=\"-123.8\">a & !b</text>\n",
|
|
"<text fill=\"#1f78b4\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"64.5\" y=\"-108.8\">\u24ff</text>\n",
|
|
"</g>\n",
|
|
"<!-- 2 -->\n",
|
|
"<g class=\"node\" id=\"node4\"><title>2</title>\n",
|
|
"<ellipse cx=\"18\" cy=\"-18\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"18\" y=\"-14.3\">2</text>\n",
|
|
"</g>\n",
|
|
"<!-- 0->2 -->\n",
|
|
"<g class=\"edge\" id=\"edge3\"><title>0->2</title>\n",
|
|
"<path d=\"M18,-101.581C18,-85.5213 18,-61.5179 18,-43.5228\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"18,-36.2191 21.1501,-43.219 18,-39.7191 18.0001,-43.2191 18.0001,-43.2191 18.0001,-43.2191 18,-39.7191 14.8501,-43.2191 18,-36.2191 18,-36.2191\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"21.5\" y=\"-72.8\">b</text>\n",
|
|
"<text fill=\"#1f78b4\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"18\" y=\"-57.8\">\u24ff</text>\n",
|
|
"</g>\n",
|
|
"<!-- 2->2 -->\n",
|
|
"<g class=\"edge\" id=\"edge5\"><title>2->2</title>\n",
|
|
"<path d=\"M33.916,-26.6334C44.1504,-28.8856 54,-26.0078 54,-18 54,-11.869 48.2263,-8.74515 40.9268,-8.6284\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"33.916,-9.36658 40.5477,-5.50081 37.3968,-9.00004 40.8775,-8.6335 40.8775,-8.6335 40.8775,-8.6335 37.3968,-9.00004 41.2074,-11.7662 33.916,-9.36658 33.916,-9.36658\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"57.5\" y=\"-21.8\">1</text>\n",
|
|
"<text fill=\"#1f78b4\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"54\" y=\"-6.8\">\u24ff</text>\n",
|
|
"</g>\n",
|
|
"</g>\n",
|
|
"</svg></td><td style=\"vertical-align: top;\"><svg height=\"220pt\" viewBox=\"0.00 0.00 208.07 220.00\" width=\"208pt\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
|
|
"<g class=\"graph\" id=\"graph0\" transform=\"scale(1 1) rotate(0) translate(4 216)\">\n",
|
|
"<title>G</title>\n",
|
|
"<polygon fill=\"white\" points=\"-4,4 -4,-216 204.071,-216 204.071,4 -4,4\" stroke=\"none\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"53.0356\" y=\"-197.8\">Inf(</text>\n",
|
|
"<text fill=\"#ff4da0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"75.0356\" y=\"-197.8\">\u2776</text>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"91.0356\" y=\"-197.8\">)&Inf(</text>\n",
|
|
"<text fill=\"#ff7f00\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"127.036\" y=\"-197.8\">\u2777</text>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"143.036\" y=\"-197.8\">)</text>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"56.0356\" y=\"-183.8\">[gen. B\u00fcchi 2]</text>\n",
|
|
"<!-- I -->\n",
|
|
"<!-- 0 -->\n",
|
|
"<g class=\"node\" id=\"node2\"><title>0</title>\n",
|
|
"<ellipse cx=\"68.0713\" cy=\"-120\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"68.0713\" y=\"-116.3\">0</text>\n",
|
|
"</g>\n",
|
|
"<!-- I->0 -->\n",
|
|
"<g class=\"edge\" id=\"edge1\"><title>I->0</title>\n",
|
|
"<path d=\"M68.0713,-174.845C68.0713,-173.206 68.0713,-158.846 68.0713,-145.368\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"68.0713,-138.058 71.2214,-145.058 68.0713,-141.558 68.0714,-145.058 68.0714,-145.058 68.0714,-145.058 68.0713,-141.558 64.9214,-145.058 68.0713,-138.058 68.0713,-138.058\" stroke=\"black\"/>\n",
|
|
"</g>\n",
|
|
"<!-- 0->0 -->\n",
|
|
"<g class=\"edge\" id=\"edge2\"><title>0->0</title>\n",
|
|
"<path d=\"M85.853,-123.236C95.3862,-123.786 104.071,-122.707 104.071,-120 104.071,-118.012 99.3874,-116.902 93.1234,-116.671\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"85.853,-116.764 92.8119,-113.524 89.3527,-116.719 92.8524,-116.674 92.8524,-116.674 92.8524,-116.674 89.3527,-116.719 92.893,-119.824 85.853,-116.764 85.853,-116.764\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"104.071\" y=\"-123.8\">!b & c</text>\n",
|
|
"<text fill=\"#ff4da0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"114.571\" y=\"-108.8\">\u2776</text>\n",
|
|
"</g>\n",
|
|
"<!-- 0->0 -->\n",
|
|
"<g class=\"edge\" id=\"edge3\"><title>0->0</title>\n",
|
|
"<path d=\"M85.6405,-124.845C108.831,-128.506 141.071,-126.891 141.071,-120 141.071,-113.782 114.821,-111.86 92.6551,-114.234\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"85.6405,-115.155 92.1705,-111.12 89.1107,-114.699 92.5808,-114.243 92.5808,-114.243 92.5808,-114.243 89.1107,-114.699 92.9912,-117.366 85.6405,-115.155 85.6405,-115.155\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"152.571\" y=\"-123.8\">b</text>\n",
|
|
"<text fill=\"#ff4da0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"141.071\" y=\"-109.8\">\u2776</text>\n",
|
|
"<text fill=\"#ff7f00\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"157.071\" y=\"-109.8\">\u2777</text>\n",
|
|
"</g>\n",
|
|
"<!-- 1 -->\n",
|
|
"<g class=\"node\" id=\"node3\"><title>1</title>\n",
|
|
"<ellipse cx=\"68.0713\" cy=\"-18\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"68.0713\" y=\"-14.3\">1</text>\n",
|
|
"</g>\n",
|
|
"<!-- 0->1 -->\n",
|
|
"<g class=\"edge\" id=\"edge4\"><title>0->1</title>\n",
|
|
"<path d=\"M50.6907,-114.668C35.6563,-109.899 14.8429,-100.607 5.07128,-84 -1.69043,-72.5084 -1.69043,-65.4916 5.07128,-54 13.4688,-39.7284 30.0209,-30.8587 44.052,-25.6199\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"50.6907,-23.3321 45.0991,-28.591 47.3817,-24.4725 44.0727,-25.6129 44.0727,-25.6129 44.0727,-25.6129 47.3817,-24.4725 43.0464,-22.6348 50.6907,-23.3321 50.6907,-23.3321\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"5.07128\" y=\"-65.3\">!b & !c</text>\n",
|
|
"</g>\n",
|
|
"<!-- 1->0 -->\n",
|
|
"<g class=\"edge\" id=\"edge5\"><title>1->0</title>\n",
|
|
"<path d=\"M68.0713,-36.2191C68.0713,-52.2129 68.0713,-76.208 68.0713,-94.2528\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"68.0713,-101.581 64.9214,-94.5813 68.0713,-98.0813 68.0714,-94.5813 68.0714,-94.5813 68.0714,-94.5813 68.0713,-98.0813 71.2214,-94.5814 68.0713,-101.581 68.0713,-101.581\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"68.0713\" y=\"-72.8\">!b & c</text>\n",
|
|
"<text fill=\"#ff4da0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"78.5713\" y=\"-57.8\">\u2776</text>\n",
|
|
"</g>\n",
|
|
"<!-- 1->0 -->\n",
|
|
"<g class=\"edge\" id=\"edge6\"><title>1->0</title>\n",
|
|
"<path d=\"M83.2231,-28.3294C91.6629,-34.4628 101.389,-43.3215 106.071,-54 111.426,-66.211 111.426,-71.789 106.071,-84 102.413,-92.3425 95.6767,-99.5744 88.8801,-105.264\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"83.2231,-109.671 86.8095,-102.884 85.9842,-107.52 88.7453,-105.369 88.7453,-105.369 88.7453,-105.369 85.9842,-107.52 90.6812,-107.854 83.2231,-109.671 83.2231,-109.671\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"110.071\" y=\"-72.8\">b & c</text>\n",
|
|
"<text fill=\"#ff4da0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"111.071\" y=\"-58.8\">\u2776</text>\n",
|
|
"<text fill=\"#ff7f00\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"127.071\" y=\"-58.8\">\u2777</text>\n",
|
|
"</g>\n",
|
|
"<!-- 1->1 -->\n",
|
|
"<g class=\"edge\" id=\"edge7\"><title>1->1</title>\n",
|
|
"<path d=\"M85.853,-22.4941C95.3862,-23.2578 104.071,-21.7598 104.071,-18 104.071,-15.2389 99.3874,-13.6976 93.1234,-13.3761\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"85.853,-13.5059 92.7956,-10.2313 89.3525,-13.4434 92.8519,-13.3808 92.8519,-13.3808 92.8519,-13.3808 89.3525,-13.4434 92.9082,-16.5303 85.853,-13.5059 85.853,-13.5059\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"104.071\" y=\"-14.3\">!b & !c</text>\n",
|
|
"</g>\n",
|
|
"<!-- 1->1 -->\n",
|
|
"<g class=\"edge\" id=\"edge8\"><title>1->1</title>\n",
|
|
"<path d=\"M85.0887,-24.4905C109.42,-29.8803 145.071,-27.7168 145.071,-18 145.071,-9.19415 115.791,-6.59174 92.1916,-10.1928\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"85.0887,-11.5095 91.3972,-7.13627 88.5301,-10.8715 91.9714,-10.2335 91.9714,-10.2335 91.9714,-10.2335 88.5301,-10.8715 92.5456,-13.3307 85.0887,-11.5095 85.0887,-11.5095\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"145.071\" y=\"-21.8\">b & !c</text>\n",
|
|
"<text fill=\"#ff7f00\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"155.571\" y=\"-6.8\">\u2777</text>\n",
|
|
"</g>\n",
|
|
"</g>\n",
|
|
"</svg></td><td style=\"vertical-align: top;\"><svg height=\"360pt\" viewBox=\"0.00 0.00 213.50 360.00\" width=\"213pt\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
|
|
"<g class=\"graph\" id=\"graph0\" transform=\"scale(0.687023 0.687023) rotate(0) translate(4 520)\">\n",
|
|
"<title>G</title>\n",
|
|
"<polygon fill=\"white\" points=\"-4,4 -4,-520 306.758,-520 306.758,4 -4,4\" stroke=\"none\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"78.379\" y=\"-501.8\">Inf(</text>\n",
|
|
"<text fill=\"#1f78b4\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"100.379\" y=\"-501.8\">\u24ff</text>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"116.379\" y=\"-501.8\">)&Inf(</text>\n",
|
|
"<text fill=\"#ff4da0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"152.379\" y=\"-501.8\">\u2776</text>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"168.379\" y=\"-501.8\">)&Inf(</text>\n",
|
|
"<text fill=\"#ff7f00\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"204.379\" y=\"-501.8\">\u2777</text>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"220.379\" y=\"-501.8\">)</text>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"107.379\" y=\"-487.8\">[gen. B\u00fcchi 3]</text>\n",
|
|
"<!-- I -->\n",
|
|
"<!-- 0 -->\n",
|
|
"<g class=\"node\" id=\"node2\"><title>0</title>\n",
|
|
"<ellipse cx=\"145.758\" cy=\"-424\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"145.758\" y=\"-420.3\">0</text>\n",
|
|
"</g>\n",
|
|
"<!-- I->0 -->\n",
|
|
"<g class=\"edge\" id=\"edge1\"><title>I->0</title>\n",
|
|
"<path d=\"M145.758,-478.845C145.758,-477.206 145.758,-462.846 145.758,-449.368\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"145.758,-442.058 148.908,-449.058 145.758,-445.558 145.758,-449.058 145.758,-449.058 145.758,-449.058 145.758,-445.558 142.608,-449.058 145.758,-442.058 145.758,-442.058\" stroke=\"black\"/>\n",
|
|
"</g>\n",
|
|
"<!-- 1 -->\n",
|
|
"<g class=\"node\" id=\"node3\"><title>1</title>\n",
|
|
"<ellipse cx=\"85.758\" cy=\"-322\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"85.758\" y=\"-318.3\">1</text>\n",
|
|
"</g>\n",
|
|
"<!-- 0->1 -->\n",
|
|
"<g class=\"edge\" id=\"edge2\"><title>0->1</title>\n",
|
|
"<path d=\"M128.676,-418.018C114.684,-412.94 95.7776,-403.558 86.758,-388 79.6603,-375.757 79.2757,-359.913 80.7308,-346.933\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"81.7632,-339.671 83.8966,-347.044 81.2706,-343.136 80.7779,-346.601 80.7779,-346.601 80.7779,-346.601 81.2706,-343.136 77.6593,-346.158 81.7632,-339.671 81.7632,-339.671\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"86.758\" y=\"-376.8\">!b & c</text>\n",
|
|
"<text fill=\"#ff4da0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"97.258\" y=\"-361.8\">\u2776</text>\n",
|
|
"</g>\n",
|
|
"<!-- 0->1 -->\n",
|
|
"<g class=\"edge\" id=\"edge3\"><title>0->1</title>\n",
|
|
"<path d=\"M142.511,-406.226C139.298,-392.461 133.433,-372.883 123.758,-358 118.87,-350.48 112.002,-343.494 105.447,-337.773\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"100.065,-333.281 107.458,-335.348 102.752,-335.524 105.439,-337.767 105.439,-337.767 105.439,-337.767 102.752,-335.524 103.421,-340.185 100.065,-333.281 100.065,-333.281\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"148.258\" y=\"-376.8\">b</text>\n",
|
|
"<text fill=\"#ff4da0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"136.758\" y=\"-362.8\">\u2776</text>\n",
|
|
"<text fill=\"#ff7f00\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"152.758\" y=\"-362.8\">\u2777</text>\n",
|
|
"</g>\n",
|
|
"<!-- 2 -->\n",
|
|
"<g class=\"node\" id=\"node4\"><title>2</title>\n",
|
|
"<ellipse cx=\"154.758\" cy=\"-220\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"154.758\" y=\"-216.3\">2</text>\n",
|
|
"</g>\n",
|
|
"<!-- 0->2 -->\n",
|
|
"<g class=\"edge\" id=\"edge4\"><title>0->2</title>\n",
|
|
"<path d=\"M157.127,-409.946C162.309,-403.597 168.273,-395.69 172.758,-388 197.545,-345.503 206.009,-334.221 215.758,-286 218.4,-272.931 222.44,-267.538 215.758,-256 207.786,-242.234 192.128,-233.414 178.673,-228.072\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"171.889,-225.588 179.546,-225.037 175.176,-226.791 178.462,-227.995 178.462,-227.995 178.462,-227.995 175.176,-226.791 177.379,-230.953 171.889,-225.588 171.889,-225.588\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"210.758\" y=\"-318.3\">!b & !c</text>\n",
|
|
"</g>\n",
|
|
"<!-- 1->1 -->\n",
|
|
"<g class=\"edge\" id=\"edge5\"><title>1->1</title>\n",
|
|
"<path d=\"M101.674,-330.633C111.908,-332.886 121.758,-330.008 121.758,-322 121.758,-315.869 115.984,-312.745 108.685,-312.628\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"101.674,-313.367 108.306,-309.501 105.155,-313 108.636,-312.633 108.636,-312.633 108.636,-312.633 105.155,-313 108.965,-315.766 101.674,-313.367 101.674,-313.367\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"121.758\" y=\"-325.8\">a & !b & c</text>\n",
|
|
"<text fill=\"#1f78b4\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"136.758\" y=\"-311.8\">\u24ff</text>\n",
|
|
"<text fill=\"#ff4da0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"152.758\" y=\"-311.8\">\u2776</text>\n",
|
|
"</g>\n",
|
|
"<!-- 1->2 -->\n",
|
|
"<g class=\"edge\" id=\"edge6\"><title>1->2</title>\n",
|
|
"<path d=\"M101.248,-312.785C111.49,-306.64 124.503,-297.357 132.758,-286 141.564,-273.885 147.027,-257.993 150.306,-244.956\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"151.911,-238.048 153.395,-245.58 151.119,-241.458 150.327,-244.867 150.327,-244.867 150.327,-244.867 151.119,-241.458 147.258,-244.154 151.911,-238.048 151.911,-238.048\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"145.758\" y=\"-274.8\">a & !b & !c</text>\n",
|
|
"<text fill=\"#1f78b4\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"170.758\" y=\"-259.8\">\u24ff</text>\n",
|
|
"</g>\n",
|
|
"<!-- 3 -->\n",
|
|
"<g class=\"node\" id=\"node5\"><title>3</title>\n",
|
|
"<ellipse cx=\"133.758\" cy=\"-18\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"133.758\" y=\"-14.3\">3</text>\n",
|
|
"</g>\n",
|
|
"<!-- 1->3 -->\n",
|
|
"<g class=\"edge\" id=\"edge7\"><title>1->3</title>\n",
|
|
"<path d=\"M73.2264,-308.926C67.6447,-302.677 61.6799,-294.571 58.758,-286 38.9792,-227.979 -64.8477,-254.714 62.758,-54 72.9243,-38.0092 92.7361,-29.0905 108.854,-24.2647\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"115.952,-22.3247 110.03,-27.2089 112.576,-23.2475 109.199,-24.1703 109.199,-24.1703 109.199,-24.1703 112.576,-23.2475 108.369,-21.1318 115.952,-22.3247 115.952,-22.3247\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"28.258\" y=\"-173.8\">b</text>\n",
|
|
"<text fill=\"#1f78b4\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"8.75799\" y=\"-159.8\">\u24ff</text>\n",
|
|
"<text fill=\"#ff4da0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"24.758\" y=\"-159.8\">\u2776</text>\n",
|
|
"<text fill=\"#ff7f00\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"40.758\" y=\"-159.8\">\u2777</text>\n",
|
|
"</g>\n",
|
|
"<!-- 2->1 -->\n",
|
|
"<g class=\"edge\" id=\"edge8\"><title>2->1</title>\n",
|
|
"<path d=\"M136.581,-222.412C115.712,-225.118 82.3585,-233.006 66.758,-256 57.6819,-269.377 63.8367,-287.136 71.4795,-300.711\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"75.2907,-307.001 68.9692,-302.646 73.477,-304.007 71.6632,-301.014 71.6632,-301.014 71.6632,-301.014 73.477,-304.007 74.3573,-299.382 75.2907,-307.001 75.2907,-307.001\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"66.758\" y=\"-274.8\">a & !b & c</text>\n",
|
|
"<text fill=\"#1f78b4\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"81.758\" y=\"-260.8\">\u24ff</text>\n",
|
|
"<text fill=\"#ff4da0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"97.758\" y=\"-260.8\">\u2776</text>\n",
|
|
"</g>\n",
|
|
"<!-- 2->2 -->\n",
|
|
"<g class=\"edge\" id=\"edge9\"><title>2->2</title>\n",
|
|
"<path d=\"M170.674,-228.633C180.908,-230.886 190.758,-228.008 190.758,-220 190.758,-213.869 184.984,-210.745 177.685,-210.628\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"170.674,-211.367 177.306,-207.501 174.155,-211 177.636,-210.633 177.636,-210.633 177.636,-210.633 174.155,-211 177.965,-213.766 170.674,-211.367 170.674,-211.367\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"190.758\" y=\"-223.8\">a & !b & !c</text>\n",
|
|
"<text fill=\"#1f78b4\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"215.758\" y=\"-208.8\">\u24ff</text>\n",
|
|
"</g>\n",
|
|
"<!-- 2->3 -->\n",
|
|
"<g class=\"edge\" id=\"edge10\"><title>2->3</title>\n",
|
|
"<path d=\"M170.744,-211.234C193.476,-199.181 234.218,-173.597 250.758,-138 257.5,-123.49 255.052,-117.413 250.758,-102 244.068,-77.99 240.774,-70.1127 221.758,-54 203.405,-38.449 177.286,-29.2412 158.273,-24.2055\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"151.365,-22.4753 158.921,-21.1205 154.76,-23.3257 158.155,-24.1761 158.155,-24.1761 158.155,-24.1761 154.76,-23.3257 157.39,-27.2317 151.365,-22.4753 151.365,-22.4753\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"261.758\" y=\"-123.8\">b & c</text>\n",
|
|
"<text fill=\"#1f78b4\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"254.758\" y=\"-109.8\">\u24ff</text>\n",
|
|
"<text fill=\"#ff4da0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"270.758\" y=\"-109.8\">\u2776</text>\n",
|
|
"<text fill=\"#ff7f00\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"286.758\" y=\"-109.8\">\u2777</text>\n",
|
|
"</g>\n",
|
|
"<!-- 4 -->\n",
|
|
"<g class=\"node\" id=\"node6\"><title>4</title>\n",
|
|
"<ellipse cx=\"109.758\" cy=\"-120\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"109.758\" y=\"-116.3\">4</text>\n",
|
|
"</g>\n",
|
|
"<!-- 2->4 -->\n",
|
|
"<g class=\"edge\" id=\"edge11\"><title>2->4</title>\n",
|
|
"<path d=\"M147.528,-203.255C140.049,-186.967 128.308,-161.398 119.902,-143.091\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"116.97,-136.706 122.754,-141.753 118.431,-139.887 119.891,-143.068 119.891,-143.068 119.891,-143.068 118.431,-139.887 117.029,-144.382 116.97,-136.706 116.97,-136.706\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"136.758\" y=\"-173.8\">b & !c</text>\n",
|
|
"<text fill=\"#1f78b4\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"139.258\" y=\"-159.8\">\u24ff</text>\n",
|
|
"<text fill=\"#ff7f00\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"155.258\" y=\"-159.8\">\u2777</text>\n",
|
|
"</g>\n",
|
|
"<!-- 3->3 -->\n",
|
|
"<g class=\"edge\" id=\"edge12\"><title>3->3</title>\n",
|
|
"<path d=\"M151.54,-22.4941C161.073,-23.2578 169.758,-21.7598 169.758,-18 169.758,-15.2389 165.074,-13.6976 158.81,-13.3761\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"151.54,-13.5059 158.482,-10.2313 155.039,-13.4434 158.539,-13.3808 158.539,-13.3808 158.539,-13.3808 155.039,-13.4434 158.595,-16.5303 151.54,-13.5059 151.54,-13.5059\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"169.758\" y=\"-21.8\">!b & c</text>\n",
|
|
"<text fill=\"#1f78b4\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"172.258\" y=\"-7.8\">\u24ff</text>\n",
|
|
"<text fill=\"#ff4da0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"188.258\" y=\"-7.8\">\u2776</text>\n",
|
|
"</g>\n",
|
|
"<!-- 3->3 -->\n",
|
|
"<g class=\"edge\" id=\"edge13\"><title>3->3</title>\n",
|
|
"<path d=\"M150.62,-24.5712C173.857,-29.8584 206.758,-27.668 206.758,-18 206.758,-9.27617 179.969,-6.64076 157.665,-10.0938\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"150.62,-11.4288 156.911,-7.0304 154.059,-10.7771 157.498,-10.1253 157.498,-10.1253 157.498,-10.1253 154.059,-10.7771 158.084,-13.2202 150.62,-11.4288 150.62,-11.4288\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"226.258\" y=\"-21.8\">b</text>\n",
|
|
"<text fill=\"#1f78b4\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"206.758\" y=\"-7.8\">\u24ff</text>\n",
|
|
"<text fill=\"#ff4da0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"222.758\" y=\"-7.8\">\u2776</text>\n",
|
|
"<text fill=\"#ff7f00\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"238.758\" y=\"-7.8\">\u2777</text>\n",
|
|
"</g>\n",
|
|
"<!-- 3->4 -->\n",
|
|
"<g class=\"edge\" id=\"edge14\"><title>3->4</title>\n",
|
|
"<path d=\"M116.377,-23.3321C101.343,-28.1006 80.5296,-37.393 70.758,-54 63.9963,-65.4916 65.3248,-71.8238 70.758,-84 74.581,-92.5677 81.6526,-99.9123 88.7352,-105.629\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"94.616,-110.039 87.1259,-108.359 91.8159,-107.939 89.0158,-105.839 89.0158,-105.839 89.0158,-105.839 91.8159,-107.939 90.9057,-103.319 94.616,-110.039 94.616,-110.039\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"70.758\" y=\"-72.8\">!b & !c</text>\n",
|
|
"<text fill=\"#1f78b4\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"83.258\" y=\"-57.8\">\u24ff</text>\n",
|
|
"</g>\n",
|
|
"<!-- 4->3 -->\n",
|
|
"<g class=\"edge\" id=\"edge15\"><title>4->3</title>\n",
|
|
"<path d=\"M113.829,-102.036C117.749,-85.7041 123.712,-60.8598 128.094,-42.6009\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"129.747,-35.7131 131.176,-43.255 128.93,-39.1165 128.113,-42.5198 128.113,-42.5198 128.113,-42.5198 128.93,-39.1165 125.05,-41.7847 129.747,-35.7131 129.747,-35.7131\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"124.758\" y=\"-72.8\">!b & c</text>\n",
|
|
"<text fill=\"#1f78b4\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"127.258\" y=\"-58.8\">\u24ff</text>\n",
|
|
"<text fill=\"#ff4da0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"143.258\" y=\"-58.8\">\u2776</text>\n",
|
|
"</g>\n",
|
|
"<!-- 4->3 -->\n",
|
|
"<g class=\"edge\" id=\"edge16\"><title>4->3</title>\n",
|
|
"<path d=\"M126.589,-113.599C139.865,-108.347 157.477,-98.9413 165.758,-84 172.222,-72.3381 170.584,-66.4295 165.758,-54 162.987,-46.8621 158.006,-40.2913 152.787,-34.8175\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"147.561,-29.7291 154.773,-32.3556 150.068,-32.1708 152.576,-34.6125 152.576,-34.6125 152.576,-34.6125 150.068,-32.1708 150.378,-36.8694 147.561,-29.7291 147.561,-29.7291\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"176.758\" y=\"-72.8\">b & c</text>\n",
|
|
"<text fill=\"#1f78b4\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"169.758\" y=\"-58.8\">\u24ff</text>\n",
|
|
"<text fill=\"#ff4da0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"185.758\" y=\"-58.8\">\u2776</text>\n",
|
|
"<text fill=\"#ff7f00\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"201.758\" y=\"-58.8\">\u2777</text>\n",
|
|
"</g>\n",
|
|
"<!-- 4->4 -->\n",
|
|
"<g class=\"edge\" id=\"edge17\"><title>4->4</title>\n",
|
|
"<path d=\"M127.54,-124.494C137.073,-125.258 145.758,-123.76 145.758,-120 145.758,-117.239 141.074,-115.698 134.81,-115.376\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"127.54,-115.506 134.482,-112.231 131.039,-115.443 134.539,-115.381 134.539,-115.381 134.539,-115.381 131.039,-115.443 134.595,-118.53 127.54,-115.506 127.54,-115.506\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"145.758\" y=\"-123.8\">!b & !c</text>\n",
|
|
"<text fill=\"#1f78b4\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"158.258\" y=\"-108.8\">\u24ff</text>\n",
|
|
"</g>\n",
|
|
"<!-- 4->4 -->\n",
|
|
"<g class=\"edge\" id=\"edge18\"><title>4->4</title>\n",
|
|
"<path d=\"M126.775,-126.491C151.106,-131.88 186.758,-129.717 186.758,-120 186.758,-111.194 157.478,-108.592 133.878,-112.193\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"126.775,-113.509 133.084,-109.136 130.217,-112.871 133.658,-112.233 133.658,-112.233 133.658,-112.233 130.217,-112.871 134.232,-115.331 126.775,-113.509 126.775,-113.509\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"186.758\" y=\"-123.8\">b & !c</text>\n",
|
|
"<text fill=\"#1f78b4\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"189.258\" y=\"-109.8\">\u24ff</text>\n",
|
|
"<text fill=\"#ff7f00\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"205.258\" y=\"-109.8\">\u2777</text>\n",
|
|
"</g>\n",
|
|
"</g>\n",
|
|
"</svg></td></tr></table>"
|
|
],
|
|
"metadata": {},
|
|
"output_type": "display_data",
|
|
"text": [
|
|
"<IPython.core.display.HTML object>"
|
|
]
|
|
},
|
|
{
|
|
"output_type": "stream",
|
|
"stream": "stdout",
|
|
"text": [
|
|
"(a, b, c)\n"
|
|
]
|
|
}
|
|
],
|
|
"prompt_number": 6
|
|
},
|
|
{
|
|
"cell_type": "markdown",
|
|
"metadata": {},
|
|
"source": [
|
|
"## Third attempt: a more usable product\n",
|
|
"\n",
|
|
"We could stop with the previous function: the result is a correct product from a theoretical point of view. However our function is still inferior to `spot.product()` in a couple of points:\n",
|
|
"- states are not presented as pairs\n",
|
|
"- the properties of the resulting automaton are not set\n",
|
|
"\n",
|
|
"The former point could be addressed by calling `set_state_names()` and passing an array of strings: if a state number is smaller than the size of that array, then the string at that position will be displayed instead of the state number in the dot output. However we can do even better by using `set_product_states()` and passing an array of pairs of states. Besides the output routines, some algorithms actually retrieve this vector of pair of states to work on the product.\n",
|
|
"\n",
|
|
"Regarding the latter point, consider for instance the deterministic nature of these automata. In Spot an automaton is deterministic if it is both existential (no universal branching) and universal (no non-deterministic branching). In our case we will restrict the algorithm to existantial input (by asserting `is_existential()` on both operands), so we can consider that the `prop_universal()` property is an indication of determinism:"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"collapsed": false,
|
|
"input": [
|
|
"print(a1.prop_universal())\n",
|
|
"print(a2.prop_universal())\n",
|
|
"print(prod.prop_universal())\n",
|
|
"print(p1.prop_universal())"
|
|
],
|
|
"language": "python",
|
|
"metadata": {},
|
|
"outputs": [
|
|
{
|
|
"output_type": "stream",
|
|
"stream": "stdout",
|
|
"text": [
|
|
"yes\n",
|
|
"yes\n",
|
|
"yes\n",
|
|
"maybe\n"
|
|
]
|
|
}
|
|
],
|
|
"prompt_number": 7
|
|
},
|
|
{
|
|
"cell_type": "markdown",
|
|
"metadata": {},
|
|
"source": [
|
|
"Because `a1` and `a2` are deterministic, their product is necessarily deterministic. This is a property that the `spot.product()` algorithm will preserve, but that our version does not *yet* preserve. We can fix that by adding\n",
|
|
"\n",
|
|
" if left.prop_universal() and right.prop_universal():\n",
|
|
" result.prop_universal(True)\n",
|
|
" \n",
|
|
"at the end of our function. Note that this is **not** the same as\n",
|
|
"\n",
|
|
" result.prop_universal(left.prop_universal() and right.prop_universal())\n",
|
|
"\n",
|
|
"because the results the `prop_*()` family of functions take and return instances of `spot.trival` values. These `spot.trival`, can, as their name implies, take one amongst three values representing `yes`, `no`, and `maybe`. `yes` and `no` should be used when we actually know that the automaton is deterministic or not (not deterministic meaning that there actually exists some non determinitic state in the automaton), and `maybe` when we do not know. \n",
|
|
"\n",
|
|
"The one-liner above is wrong for two reasons:\n",
|
|
"\n",
|
|
" - if `left` and `right` are non-deterministic, their product could be deterministic, so calling prop_universal(False) would be wrong. \n",
|
|
"\n",
|
|
" - the use of the `and` operator on `trival` is misleading in non-Boolean context. The `&` operator would be the correct operator to use if you want to work in threed-valued logic. Compare: "
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"collapsed": false,
|
|
"input": [
|
|
"yes = spot.trival(True)\n",
|
|
"no = spot.trival(False)\n",
|
|
"maybe = spot.trival_maybe()\n",
|
|
"for u in (no, maybe, yes):\n",
|
|
" for v in (no, maybe, yes):\n",
|
|
" print(\"{u!s:>5} & {v!s:<5} = {r1!s:<5} {u!s:>5} and {v!s:<5} = {r2!s:<5}\"\n",
|
|
" .format(u=u, v=v, r1=(u&v), r2=(u and v)))"
|
|
],
|
|
"language": "python",
|
|
"metadata": {},
|
|
"outputs": [
|
|
{
|
|
"output_type": "stream",
|
|
"stream": "stdout",
|
|
"text": [
|
|
" no & no = no no and no = no \n",
|
|
" no & maybe = no no and maybe = no \n",
|
|
" no & yes = no no and yes = no \n",
|
|
"maybe & no = no maybe and no = maybe\n",
|
|
"maybe & maybe = maybe maybe and maybe = maybe\n",
|
|
"maybe & yes = maybe maybe and yes = maybe\n",
|
|
" yes & no = no yes and no = no \n",
|
|
" yes & maybe = maybe yes and maybe = maybe\n",
|
|
" yes & yes = yes yes and yes = yes \n"
|
|
]
|
|
}
|
|
],
|
|
"prompt_number": 8
|
|
},
|
|
{
|
|
"cell_type": "markdown",
|
|
"metadata": {},
|
|
"source": [
|
|
"The reason `maybe and no` is equal to `maybe` is that Python evaluate it like `no if maybe else maybe`, but when a trival is evaluated in a Boolean context (as in `if maybe`) the result is True only if the trival is equal to yes.\n",
|
|
"\n",
|
|
"So our\n",
|
|
"\n",
|
|
" if left.prop_universal() and right.prop_universal():\n",
|
|
" result.prop_universal(True)\n",
|
|
"\n",
|
|
"is OK because the `if` body will only be entered of both input automata are known to be deterministic."
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "markdown",
|
|
"metadata": {},
|
|
"source": [
|
|
"However the question is in fact more general than just determinism: the product of two weak automata is weak, the product of two stutter-invariant automata is stutter-invariant, etc. So when writing an algorithm one should consider which of the [property bits](https://spot.lrde.epita.fr/hoa.html#property-bits) are naturally preserved by the algorithm, and set the relevant bits: this can save time later if the resulting automaton is used as input for another algorithm."
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"collapsed": false,
|
|
"input": [
|
|
"def product3(left, right):\n",
|
|
" # the twa_graph.is_existential() method returns a Boolean, not a spot.trival\n",
|
|
" if not (left.is_existential() and right.is_existential()):\n",
|
|
" raise RuntimeError(\"alternating automata are not supported\")\n",
|
|
" bdict = left.get_dict()\n",
|
|
" if right.get_dict() != bdict:\n",
|
|
" raise RuntimeError(\"automata should share their dictionary\")\n",
|
|
" \n",
|
|
" result = spot.make_twa_graph(bdict)\n",
|
|
" result.copy_ap_of(left)\n",
|
|
" result.copy_ap_of(right)\n",
|
|
" \n",
|
|
" pairs = [] # our array of state pairs\n",
|
|
" sdict = {}\n",
|
|
" todo = []\n",
|
|
" def dst(ls, rs):\n",
|
|
" pair = (ls, rs)\n",
|
|
" p = sdict.get(pair)\n",
|
|
" if p is None:\n",
|
|
" p = result.new_state()\n",
|
|
" sdict[pair] = p\n",
|
|
" todo.append((ls, rs, p))\n",
|
|
" pairs.append((ls, rs)) # name each state\n",
|
|
" return p\n",
|
|
" \n",
|
|
" result.set_init_state(dst(left.get_init_state_number(), \n",
|
|
" right.get_init_state_number()))\n",
|
|
"\n",
|
|
" shift = left.num_sets()\n",
|
|
" result.set_acceptance(shift + right.num_sets(),\n",
|
|
" left.get_acceptance() & (right.get_acceptance() << shift))\n",
|
|
" \n",
|
|
" while todo:\n",
|
|
" lsrc, rsrc, osrc = todo.pop()\n",
|
|
" for lt in left.out(lsrc):\n",
|
|
" for rt in right.out(rsrc):\n",
|
|
" cond = lt.cond & rt.cond\n",
|
|
" if cond != buddy.bddfalse:\n",
|
|
" acc = lt.acc | (rt.acc << shift)\n",
|
|
" result.new_edge(osrc, dst(lt.dst, rt.dst), cond, acc)\n",
|
|
"\n",
|
|
" # Remember the origin of our states\n",
|
|
" result.set_product_states(pairs)\n",
|
|
" \n",
|
|
" # Loop over all the properties we want to preserve if they hold in both automata\n",
|
|
" for p in ('prop_universal', 'prop_complete', 'prop_weak', 'prop_inherently_weak', \n",
|
|
" 'prop_terminal', 'prop_stutter_invariant', 'prop_state_acc'):\n",
|
|
" if getattr(left, p)() and getattr(right, p)():\n",
|
|
" getattr(result, p)(True)\n",
|
|
" return result\n",
|
|
"\n",
|
|
"p3 = product3(a1, a2)\n",
|
|
"show_prod(a1, a2, p3)\n",
|
|
"print(p3.prop_universal())"
|
|
],
|
|
"language": "python",
|
|
"metadata": {},
|
|
"outputs": [
|
|
{
|
|
"html": [
|
|
"<table><tr><td style=\"vertical-align: top;\"><svg height=\"307pt\" viewBox=\"0.00 0.00 99.00 307.00\" width=\"99pt\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
|
|
"<g class=\"graph\" id=\"graph0\" transform=\"scale(1 1) rotate(0) translate(4 303)\">\n",
|
|
"<title>G</title>\n",
|
|
"<polygon fill=\"white\" points=\"-4,4 -4,-303 95,-303 95,4 -4,4\" stroke=\"none\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"24.5\" y=\"-284.8\">Inf(</text>\n",
|
|
"<text fill=\"#1f78b4\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"46.5\" y=\"-284.8\">\u24ff</text>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"62.5\" y=\"-284.8\">)</text>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"22.5\" y=\"-270.8\">[B\u00fcchi]</text>\n",
|
|
"<!-- I -->\n",
|
|
"<!-- 1 -->\n",
|
|
"<g class=\"node\" id=\"node2\"><title>1</title>\n",
|
|
"<ellipse cx=\"18\" cy=\"-207\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"18\" y=\"-203.3\">1</text>\n",
|
|
"</g>\n",
|
|
"<!-- I->1 -->\n",
|
|
"<g class=\"edge\" id=\"edge1\"><title>I->1</title>\n",
|
|
"<path d=\"M18,-261.845C18,-260.206 18,-245.846 18,-232.368\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"18,-225.058 21.1501,-232.058 18,-228.558 18.0001,-232.058 18.0001,-232.058 18.0001,-232.058 18,-228.558 14.8501,-232.058 18,-225.058 18,-225.058\" stroke=\"black\"/>\n",
|
|
"</g>\n",
|
|
"<!-- 0 -->\n",
|
|
"<g class=\"node\" id=\"node3\"><title>0</title>\n",
|
|
"<ellipse cx=\"18\" cy=\"-120\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"18\" y=\"-116.3\">0</text>\n",
|
|
"</g>\n",
|
|
"<!-- 1->0 -->\n",
|
|
"<g class=\"edge\" id=\"edge4\"><title>1->0</title>\n",
|
|
"<path d=\"M18,-188.799C18,-176.356 18,-159.364 18,-145.504\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"18,-138.175 21.1501,-145.175 18,-141.675 18.0001,-145.175 18.0001,-145.175 18.0001,-145.175 18,-141.675 14.8501,-145.175 18,-138.175 18,-138.175\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"22.5\" y=\"-159.8\">1</text>\n",
|
|
"</g>\n",
|
|
"<!-- 0->0 -->\n",
|
|
"<g class=\"edge\" id=\"edge2\"><title>0->0</title>\n",
|
|
"<path d=\"M34.6641,-127.383C44.625,-129.023 54,-126.562 54,-120 54,-115.078 48.7266,-112.463 41.8876,-112.156\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"34.6641,-112.617 41.449,-109.027 38.1569,-112.394 41.6498,-112.171 41.6498,-112.171 41.6498,-112.171 38.1569,-112.394 41.8507,-115.314 34.6641,-112.617 34.6641,-112.617\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"54\" y=\"-123.8\">a & !b</text>\n",
|
|
"<text fill=\"#1f78b4\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"64.5\" y=\"-108.8\">\u24ff</text>\n",
|
|
"</g>\n",
|
|
"<!-- 2 -->\n",
|
|
"<g class=\"node\" id=\"node4\"><title>2</title>\n",
|
|
"<ellipse cx=\"18\" cy=\"-18\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"18\" y=\"-14.3\">2</text>\n",
|
|
"</g>\n",
|
|
"<!-- 0->2 -->\n",
|
|
"<g class=\"edge\" id=\"edge3\"><title>0->2</title>\n",
|
|
"<path d=\"M18,-101.581C18,-85.5213 18,-61.5179 18,-43.5228\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"18,-36.2191 21.1501,-43.219 18,-39.7191 18.0001,-43.2191 18.0001,-43.2191 18.0001,-43.2191 18,-39.7191 14.8501,-43.2191 18,-36.2191 18,-36.2191\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"21.5\" y=\"-72.8\">b</text>\n",
|
|
"<text fill=\"#1f78b4\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"18\" y=\"-57.8\">\u24ff</text>\n",
|
|
"</g>\n",
|
|
"<!-- 2->2 -->\n",
|
|
"<g class=\"edge\" id=\"edge5\"><title>2->2</title>\n",
|
|
"<path d=\"M33.916,-26.6334C44.1504,-28.8856 54,-26.0078 54,-18 54,-11.869 48.2263,-8.74515 40.9268,-8.6284\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"33.916,-9.36658 40.5477,-5.50081 37.3968,-9.00004 40.8775,-8.6335 40.8775,-8.6335 40.8775,-8.6335 37.3968,-9.00004 41.2074,-11.7662 33.916,-9.36658 33.916,-9.36658\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"57.5\" y=\"-21.8\">1</text>\n",
|
|
"<text fill=\"#1f78b4\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"54\" y=\"-6.8\">\u24ff</text>\n",
|
|
"</g>\n",
|
|
"</g>\n",
|
|
"</svg></td><td style=\"vertical-align: top;\"><svg height=\"220pt\" viewBox=\"0.00 0.00 208.07 220.00\" width=\"208pt\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
|
|
"<g class=\"graph\" id=\"graph0\" transform=\"scale(1 1) rotate(0) translate(4 216)\">\n",
|
|
"<title>G</title>\n",
|
|
"<polygon fill=\"white\" points=\"-4,4 -4,-216 204.071,-216 204.071,4 -4,4\" stroke=\"none\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"53.0356\" y=\"-197.8\">Inf(</text>\n",
|
|
"<text fill=\"#ff4da0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"75.0356\" y=\"-197.8\">\u2776</text>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"91.0356\" y=\"-197.8\">)&Inf(</text>\n",
|
|
"<text fill=\"#ff7f00\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"127.036\" y=\"-197.8\">\u2777</text>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"143.036\" y=\"-197.8\">)</text>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"56.0356\" y=\"-183.8\">[gen. B\u00fcchi 2]</text>\n",
|
|
"<!-- I -->\n",
|
|
"<!-- 0 -->\n",
|
|
"<g class=\"node\" id=\"node2\"><title>0</title>\n",
|
|
"<ellipse cx=\"68.0713\" cy=\"-120\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"68.0713\" y=\"-116.3\">0</text>\n",
|
|
"</g>\n",
|
|
"<!-- I->0 -->\n",
|
|
"<g class=\"edge\" id=\"edge1\"><title>I->0</title>\n",
|
|
"<path d=\"M68.0713,-174.845C68.0713,-173.206 68.0713,-158.846 68.0713,-145.368\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"68.0713,-138.058 71.2214,-145.058 68.0713,-141.558 68.0714,-145.058 68.0714,-145.058 68.0714,-145.058 68.0713,-141.558 64.9214,-145.058 68.0713,-138.058 68.0713,-138.058\" stroke=\"black\"/>\n",
|
|
"</g>\n",
|
|
"<!-- 0->0 -->\n",
|
|
"<g class=\"edge\" id=\"edge2\"><title>0->0</title>\n",
|
|
"<path d=\"M85.853,-123.236C95.3862,-123.786 104.071,-122.707 104.071,-120 104.071,-118.012 99.3874,-116.902 93.1234,-116.671\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"85.853,-116.764 92.8119,-113.524 89.3527,-116.719 92.8524,-116.674 92.8524,-116.674 92.8524,-116.674 89.3527,-116.719 92.893,-119.824 85.853,-116.764 85.853,-116.764\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"104.071\" y=\"-123.8\">!b & c</text>\n",
|
|
"<text fill=\"#ff4da0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"114.571\" y=\"-108.8\">\u2776</text>\n",
|
|
"</g>\n",
|
|
"<!-- 0->0 -->\n",
|
|
"<g class=\"edge\" id=\"edge3\"><title>0->0</title>\n",
|
|
"<path d=\"M85.6405,-124.845C108.831,-128.506 141.071,-126.891 141.071,-120 141.071,-113.782 114.821,-111.86 92.6551,-114.234\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"85.6405,-115.155 92.1705,-111.12 89.1107,-114.699 92.5808,-114.243 92.5808,-114.243 92.5808,-114.243 89.1107,-114.699 92.9912,-117.366 85.6405,-115.155 85.6405,-115.155\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"152.571\" y=\"-123.8\">b</text>\n",
|
|
"<text fill=\"#ff4da0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"141.071\" y=\"-109.8\">\u2776</text>\n",
|
|
"<text fill=\"#ff7f00\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"157.071\" y=\"-109.8\">\u2777</text>\n",
|
|
"</g>\n",
|
|
"<!-- 1 -->\n",
|
|
"<g class=\"node\" id=\"node3\"><title>1</title>\n",
|
|
"<ellipse cx=\"68.0713\" cy=\"-18\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"68.0713\" y=\"-14.3\">1</text>\n",
|
|
"</g>\n",
|
|
"<!-- 0->1 -->\n",
|
|
"<g class=\"edge\" id=\"edge4\"><title>0->1</title>\n",
|
|
"<path d=\"M50.6907,-114.668C35.6563,-109.899 14.8429,-100.607 5.07128,-84 -1.69043,-72.5084 -1.69043,-65.4916 5.07128,-54 13.4688,-39.7284 30.0209,-30.8587 44.052,-25.6199\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"50.6907,-23.3321 45.0991,-28.591 47.3817,-24.4725 44.0727,-25.6129 44.0727,-25.6129 44.0727,-25.6129 47.3817,-24.4725 43.0464,-22.6348 50.6907,-23.3321 50.6907,-23.3321\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"5.07128\" y=\"-65.3\">!b & !c</text>\n",
|
|
"</g>\n",
|
|
"<!-- 1->0 -->\n",
|
|
"<g class=\"edge\" id=\"edge5\"><title>1->0</title>\n",
|
|
"<path d=\"M68.0713,-36.2191C68.0713,-52.2129 68.0713,-76.208 68.0713,-94.2528\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"68.0713,-101.581 64.9214,-94.5813 68.0713,-98.0813 68.0714,-94.5813 68.0714,-94.5813 68.0714,-94.5813 68.0713,-98.0813 71.2214,-94.5814 68.0713,-101.581 68.0713,-101.581\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"68.0713\" y=\"-72.8\">!b & c</text>\n",
|
|
"<text fill=\"#ff4da0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"78.5713\" y=\"-57.8\">\u2776</text>\n",
|
|
"</g>\n",
|
|
"<!-- 1->0 -->\n",
|
|
"<g class=\"edge\" id=\"edge6\"><title>1->0</title>\n",
|
|
"<path d=\"M83.2231,-28.3294C91.6629,-34.4628 101.389,-43.3215 106.071,-54 111.426,-66.211 111.426,-71.789 106.071,-84 102.413,-92.3425 95.6767,-99.5744 88.8801,-105.264\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"83.2231,-109.671 86.8095,-102.884 85.9842,-107.52 88.7453,-105.369 88.7453,-105.369 88.7453,-105.369 85.9842,-107.52 90.6812,-107.854 83.2231,-109.671 83.2231,-109.671\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"110.071\" y=\"-72.8\">b & c</text>\n",
|
|
"<text fill=\"#ff4da0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"111.071\" y=\"-58.8\">\u2776</text>\n",
|
|
"<text fill=\"#ff7f00\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"127.071\" y=\"-58.8\">\u2777</text>\n",
|
|
"</g>\n",
|
|
"<!-- 1->1 -->\n",
|
|
"<g class=\"edge\" id=\"edge7\"><title>1->1</title>\n",
|
|
"<path d=\"M85.853,-22.4941C95.3862,-23.2578 104.071,-21.7598 104.071,-18 104.071,-15.2389 99.3874,-13.6976 93.1234,-13.3761\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"85.853,-13.5059 92.7956,-10.2313 89.3525,-13.4434 92.8519,-13.3808 92.8519,-13.3808 92.8519,-13.3808 89.3525,-13.4434 92.9082,-16.5303 85.853,-13.5059 85.853,-13.5059\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"104.071\" y=\"-14.3\">!b & !c</text>\n",
|
|
"</g>\n",
|
|
"<!-- 1->1 -->\n",
|
|
"<g class=\"edge\" id=\"edge8\"><title>1->1</title>\n",
|
|
"<path d=\"M85.0887,-24.4905C109.42,-29.8803 145.071,-27.7168 145.071,-18 145.071,-9.19415 115.791,-6.59174 92.1916,-10.1928\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"85.0887,-11.5095 91.3972,-7.13627 88.5301,-10.8715 91.9714,-10.2335 91.9714,-10.2335 91.9714,-10.2335 88.5301,-10.8715 92.5456,-13.3307 85.0887,-11.5095 85.0887,-11.5095\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"145.071\" y=\"-21.8\">b & !c</text>\n",
|
|
"<text fill=\"#ff7f00\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"155.571\" y=\"-6.8\">\u2777</text>\n",
|
|
"</g>\n",
|
|
"</g>\n",
|
|
"</svg></td><td style=\"vertical-align: top;\"><svg height=\"360pt\" viewBox=\"0.00 0.00 193.38 360.00\" width=\"193pt\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
|
|
"<g class=\"graph\" id=\"graph0\" transform=\"scale(0.687023 0.687023) rotate(0) translate(4 520)\">\n",
|
|
"<title>G</title>\n",
|
|
"<polygon fill=\"white\" points=\"-4,4 -4,-520 277.475,-520 277.475,4 -4,4\" stroke=\"none\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"63.7375\" y=\"-501.8\">Inf(</text>\n",
|
|
"<text fill=\"#1f78b4\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"85.7375\" y=\"-501.8\">\u24ff</text>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"101.738\" y=\"-501.8\">)&Inf(</text>\n",
|
|
"<text fill=\"#ff4da0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"137.738\" y=\"-501.8\">\u2776</text>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"153.738\" y=\"-501.8\">)&Inf(</text>\n",
|
|
"<text fill=\"#ff7f00\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"189.738\" y=\"-501.8\">\u2777</text>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"205.738\" y=\"-501.8\">)</text>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"92.7375\" y=\"-487.8\">[gen. B\u00fcchi 3]</text>\n",
|
|
"<!-- I -->\n",
|
|
"<!-- 0 -->\n",
|
|
"<g class=\"node\" id=\"node2\"><title>0</title>\n",
|
|
"<ellipse cx=\"100.475\" cy=\"-424\" fill=\"#ffffaa\" rx=\"27\" ry=\"18\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"90.475\" y=\"-420.3\">1,0</text>\n",
|
|
"</g>\n",
|
|
"<!-- I->0 -->\n",
|
|
"<g class=\"edge\" id=\"edge1\"><title>I->0</title>\n",
|
|
"<path d=\"M100.475,-478.845C100.475,-477.206 100.475,-462.846 100.475,-449.368\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"100.475,-442.058 103.625,-449.058 100.475,-445.558 100.475,-449.058 100.475,-449.058 100.475,-449.058 100.475,-445.558 97.3251,-449.058 100.475,-442.058 100.475,-442.058\" stroke=\"black\"/>\n",
|
|
"</g>\n",
|
|
"<!-- 1 -->\n",
|
|
"<g class=\"node\" id=\"node3\"><title>1</title>\n",
|
|
"<ellipse cx=\"40.475\" cy=\"-322\" fill=\"#ffffaa\" rx=\"27\" ry=\"18\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"30.475\" y=\"-318.3\">0,0</text>\n",
|
|
"</g>\n",
|
|
"<!-- 0->1 -->\n",
|
|
"<g class=\"edge\" id=\"edge2\"><title>0->1</title>\n",
|
|
"<path d=\"M76.7094,-415.391C63.8708,-409.939 49.1208,-401.189 41.475,-388 34.4247,-375.839 33.9982,-360.124 35.419,-347.193\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"36.4329,-339.949 38.5821,-347.318 35.9477,-343.415 35.4625,-346.881 35.4625,-346.881 35.4625,-346.881 35.9477,-343.415 32.3429,-346.445 36.4329,-339.949 36.4329,-339.949\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"41.475\" y=\"-376.8\">!b & c</text>\n",
|
|
"<text fill=\"#ff4da0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"51.975\" y=\"-361.8\">\u2776</text>\n",
|
|
"</g>\n",
|
|
"<!-- 0->1 -->\n",
|
|
"<g class=\"edge\" id=\"edge3\"><title>0->1</title>\n",
|
|
"<path d=\"M97.1632,-405.948C93.9364,-392.198 88.0849,-372.783 78.475,-358 74.4421,-351.796 69.062,-345.956 63.6219,-340.889\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"58.2095,-336.096 65.5383,-338.379 60.8296,-338.416 63.4498,-340.737 63.4498,-340.737 63.4498,-340.737 60.8296,-338.416 61.3613,-343.095 58.2095,-336.096 58.2095,-336.096\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"102.975\" y=\"-376.8\">b</text>\n",
|
|
"<text fill=\"#ff4da0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"91.475\" y=\"-362.8\">\u2776</text>\n",
|
|
"<text fill=\"#ff7f00\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"107.475\" y=\"-362.8\">\u2777</text>\n",
|
|
"</g>\n",
|
|
"<!-- 2 -->\n",
|
|
"<g class=\"node\" id=\"node4\"><title>2</title>\n",
|
|
"<ellipse cx=\"114.475\" cy=\"-220\" fill=\"#ffffaa\" rx=\"27\" ry=\"18\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"104.475\" y=\"-216.3\">0,1</text>\n",
|
|
"</g>\n",
|
|
"<!-- 0->2 -->\n",
|
|
"<g class=\"edge\" id=\"edge4\"><title>0->2</title>\n",
|
|
"<path d=\"M113.348,-407.885C132.631,-383.949 167.694,-334.994 176.475,-286 178.827,-272.876 183.198,-267.515 176.475,-256 169.639,-244.291 157.279,-236.191 145.384,-230.756\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"138.861,-228.005 146.535,-227.823 142.086,-229.365 145.311,-230.725 145.311,-230.725 145.311,-230.725 142.086,-229.365 144.086,-233.628 138.861,-228.005 138.861,-228.005\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"171.475\" y=\"-318.3\">!b & !c</text>\n",
|
|
"</g>\n",
|
|
"<!-- 1->1 -->\n",
|
|
"<g class=\"edge\" id=\"edge5\"><title>1->1</title>\n",
|
|
"<path d=\"M64.0896,-331.146C75.4482,-332.275 85.475,-329.227 85.475,-322 85.475,-316.354 79.3551,-313.258 71.2615,-312.713\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"64.0896,-312.854 71.0262,-309.567 67.589,-312.785 71.0883,-312.716 71.0883,-312.716 71.0883,-312.716 67.589,-312.785 71.1503,-315.865 64.0896,-312.854 64.0896,-312.854\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"85.475\" y=\"-325.8\">a & !b & c</text>\n",
|
|
"<text fill=\"#1f78b4\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"100.475\" y=\"-311.8\">\u24ff</text>\n",
|
|
"<text fill=\"#ff4da0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"116.475\" y=\"-311.8\">\u2776</text>\n",
|
|
"</g>\n",
|
|
"<!-- 1->2 -->\n",
|
|
"<g class=\"edge\" id=\"edge6\"><title>1->2</title>\n",
|
|
"<path d=\"M61.9369,-310.795C72.4273,-304.855 84.4815,-296.464 92.475,-286 101.567,-274.098 107.035,-258.21 110.246,-245.121\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"111.806,-238.181 113.344,-245.701 111.038,-241.596 110.27,-245.01 110.27,-245.01 110.27,-245.01 111.038,-241.596 107.197,-244.32 111.806,-238.181 111.806,-238.181\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"106.475\" y=\"-274.8\">a & !b & !c</text>\n",
|
|
"<text fill=\"#1f78b4\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"131.475\" y=\"-259.8\">\u24ff</text>\n",
|
|
"</g>\n",
|
|
"<!-- 3 -->\n",
|
|
"<g class=\"node\" id=\"node5\"><title>3</title>\n",
|
|
"<ellipse cx=\"93.475\" cy=\"-18\" fill=\"#ffffaa\" rx=\"27\" ry=\"18\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"83.475\" y=\"-14.3\">2,0</text>\n",
|
|
"</g>\n",
|
|
"<!-- 1->3 -->\n",
|
|
"<g class=\"edge\" id=\"edge7\"><title>1->3</title>\n",
|
|
"<path d=\"M28.3704,-305.878C24.4066,-300.02 20.5022,-293.034 18.475,-286 14.7828,-273.188 18.343,-269.333 18.475,-256 19.364,-166.209 -25.7013,-129.778 22.475,-54 31.0924,-40.4456 46.64,-31.9724 60.9938,-26.766\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"67.9087,-24.4646 62.2617,-29.664 64.5878,-25.5699 61.2669,-26.6752 61.2669,-26.6752 61.2669,-26.6752 64.5878,-25.5699 60.2722,-23.6864 67.9087,-24.4646 67.9087,-24.4646\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"29.975\" y=\"-173.8\">b</text>\n",
|
|
"<text fill=\"#1f78b4\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"10.475\" y=\"-159.8\">\u24ff</text>\n",
|
|
"<text fill=\"#ff4da0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"26.475\" y=\"-159.8\">\u2776</text>\n",
|
|
"<text fill=\"#ff7f00\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"42.475\" y=\"-159.8\">\u2777</text>\n",
|
|
"</g>\n",
|
|
"<!-- 2->1 -->\n",
|
|
"<g class=\"edge\" id=\"edge8\"><title>2->1</title>\n",
|
|
"<path d=\"M87.9982,-223.68C67.4145,-227.312 40.1371,-235.863 26.475,-256 18.031,-268.446 21.8083,-285.06 27.5543,-298.375\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"30.6842,-304.998 24.8452,-300.015 29.1887,-301.834 27.6932,-298.669 27.6932,-298.669 27.6932,-298.669 29.1887,-301.834 30.5412,-297.323 30.6842,-304.998 30.6842,-304.998\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"26.475\" y=\"-274.8\">a & !b & c</text>\n",
|
|
"<text fill=\"#1f78b4\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"41.475\" y=\"-260.8\">\u24ff</text>\n",
|
|
"<text fill=\"#ff4da0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"57.475\" y=\"-260.8\">\u2776</text>\n",
|
|
"</g>\n",
|
|
"<!-- 2->2 -->\n",
|
|
"<g class=\"edge\" id=\"edge9\"><title>2->2</title>\n",
|
|
"<path d=\"M138.09,-229.146C149.448,-230.275 159.475,-227.227 159.475,-220 159.475,-214.354 153.355,-211.258 145.261,-210.713\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"138.09,-210.854 145.026,-207.567 141.589,-210.785 145.088,-210.716 145.088,-210.716 145.088,-210.716 141.589,-210.785 145.15,-213.865 138.09,-210.854 138.09,-210.854\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"159.475\" y=\"-223.8\">a & !b & !c</text>\n",
|
|
"<text fill=\"#1f78b4\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"184.475\" y=\"-208.8\">\u24ff</text>\n",
|
|
"</g>\n",
|
|
"<!-- 2->3 -->\n",
|
|
"<g class=\"edge\" id=\"edge10\"><title>2->3</title>\n",
|
|
"<path d=\"M137.075,-209.51C162.929,-197.264 203.945,-173.257 221.475,-138 228.598,-123.673 226.828,-117.078 221.475,-102 212.278,-76.0968 204.66,-70.2291 182.475,-54 165.44,-41.5381 143.376,-32.8221 125.48,-27.2048\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"118.594,-25.1301 126.205,-24.1336 121.945,-26.1399 125.297,-27.1497 125.297,-27.1497 125.297,-27.1497 121.945,-26.1399 124.388,-30.1657 118.594,-25.1301 118.594,-25.1301\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"232.475\" y=\"-123.8\">b & c</text>\n",
|
|
"<text fill=\"#1f78b4\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"225.475\" y=\"-109.8\">\u24ff</text>\n",
|
|
"<text fill=\"#ff4da0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"241.475\" y=\"-109.8\">\u2776</text>\n",
|
|
"<text fill=\"#ff7f00\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"257.475\" y=\"-109.8\">\u2777</text>\n",
|
|
"</g>\n",
|
|
"<!-- 4 -->\n",
|
|
"<g class=\"node\" id=\"node6\"><title>4</title>\n",
|
|
"<ellipse cx=\"71.475\" cy=\"-120\" fill=\"#ffffaa\" rx=\"27\" ry=\"18\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"61.475\" y=\"-116.3\">2,1</text>\n",
|
|
"</g>\n",
|
|
"<!-- 2->4 -->\n",
|
|
"<g class=\"edge\" id=\"edge11\"><title>2->4</title>\n",
|
|
"<path d=\"M107.181,-202.376C100.158,-186.37 89.4748,-162.023 81.6234,-144.129\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"78.6617,-137.379 84.3589,-142.523 80.068,-140.584 81.4743,-143.789 81.4743,-143.789 81.4743,-143.789 80.068,-140.584 78.5898,-145.055 78.6617,-137.379 78.6617,-137.379\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"97.475\" y=\"-173.8\">b & !c</text>\n",
|
|
"<text fill=\"#1f78b4\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"99.975\" y=\"-159.8\">\u24ff</text>\n",
|
|
"<text fill=\"#ff7f00\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"115.975\" y=\"-159.8\">\u2777</text>\n",
|
|
"</g>\n",
|
|
"<!-- 3->3 -->\n",
|
|
"<g class=\"edge\" id=\"edge12\"><title>3->3</title>\n",
|
|
"<path d=\"M119.822,-22.6692C130.008,-22.8767 138.475,-21.3203 138.475,-18 138.475,-15.5098 133.712,-14.0117 127.034,-13.5059\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"119.822,-13.3308 126.896,-10.3517 123.321,-13.4158 126.82,-13.5008 126.82,-13.5008 126.82,-13.5008 123.321,-13.4158 126.743,-16.6499 119.822,-13.3308 119.822,-13.3308\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"138.475\" y=\"-21.8\">!b & c</text>\n",
|
|
"<text fill=\"#1f78b4\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"140.975\" y=\"-7.8\">\u24ff</text>\n",
|
|
"<text fill=\"#ff4da0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"156.975\" y=\"-7.8\">\u2776</text>\n",
|
|
"</g>\n",
|
|
"<!-- 3->3 -->\n",
|
|
"<g class=\"edge\" id=\"edge13\"><title>3->3</title>\n",
|
|
"<path d=\"M118.023,-25.5159C143.619,-29.5385 175.475,-27.0332 175.475,-18 175.475,-9.77837 149.086,-6.96436 125.046,-9.55795\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"118.023,-10.4841 124.551,-6.44583 121.493,-10.0264 124.963,-9.56879 124.963,-9.56879 124.963,-9.56879 121.493,-10.0264 125.375,-12.6918 118.023,-10.4841 118.023,-10.4841\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"194.975\" y=\"-21.8\">b</text>\n",
|
|
"<text fill=\"#1f78b4\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"175.475\" y=\"-7.8\">\u24ff</text>\n",
|
|
"<text fill=\"#ff4da0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"191.475\" y=\"-7.8\">\u2776</text>\n",
|
|
"<text fill=\"#ff7f00\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"207.475\" y=\"-7.8\">\u2777</text>\n",
|
|
"</g>\n",
|
|
"<!-- 3->4 -->\n",
|
|
"<g class=\"edge\" id=\"edge14\"><title>3->4</title>\n",
|
|
"<path d=\"M69.0276,-25.7806C55.0894,-31.0394 38.7873,-39.8733 30.475,-54 23.7133,-65.4916 24.8914,-71.8921 30.475,-84 33.8958,-91.4178 39.7499,-97.846 45.9805,-103.097\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"51.7492,-107.583 44.2897,-105.773 48.9863,-105.435 46.2234,-103.286 46.2234,-103.286 46.2234,-103.286 48.9863,-105.435 48.1572,-100.799 51.7492,-107.583 51.7492,-107.583\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"30.475\" y=\"-72.8\">!b & !c</text>\n",
|
|
"<text fill=\"#1f78b4\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"42.975\" y=\"-57.8\">\u24ff</text>\n",
|
|
"</g>\n",
|
|
"<!-- 4->3 -->\n",
|
|
"<g class=\"edge\" id=\"edge15\"><title>4->3</title>\n",
|
|
"<path d=\"M75.207,-102.036C78.7785,-85.8025 84.2001,-61.1589 88.2101,-42.9316\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"89.7247,-36.0469 91.297,-43.5602 88.9727,-39.4651 88.2206,-42.8834 88.2206,-42.8834 88.2206,-42.8834 88.9727,-39.4651 85.1442,-42.2065 89.7247,-36.0469 89.7247,-36.0469\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"85.475\" y=\"-72.8\">!b & c</text>\n",
|
|
"<text fill=\"#1f78b4\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"87.975\" y=\"-58.8\">\u24ff</text>\n",
|
|
"<text fill=\"#ff4da0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"103.975\" y=\"-58.8\">\u2776</text>\n",
|
|
"</g>\n",
|
|
"<!-- 4->3 -->\n",
|
|
"<g class=\"edge\" id=\"edge16\"><title>4->3</title>\n",
|
|
"<path d=\"M94.5936,-110.627C106.395,-105.037 119.667,-96.4018 126.475,-84 132.891,-72.3119 131.396,-66.3921 126.475,-54 124.03,-47.8439 119.933,-42.1428 115.442,-37.2057\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"110.473,-32.1629 117.63,-34.9383 112.93,-34.656 115.386,-37.1492 115.386,-37.1492 115.386,-37.1492 112.93,-34.656 113.142,-39.36 110.473,-32.1629 110.473,-32.1629\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"137.475\" y=\"-72.8\">b & c</text>\n",
|
|
"<text fill=\"#1f78b4\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"130.475\" y=\"-58.8\">\u24ff</text>\n",
|
|
"<text fill=\"#ff4da0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"146.475\" y=\"-58.8\">\u2776</text>\n",
|
|
"<text fill=\"#ff7f00\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"162.475\" y=\"-58.8\">\u2777</text>\n",
|
|
"</g>\n",
|
|
"<!-- 4->4 -->\n",
|
|
"<g class=\"edge\" id=\"edge17\"><title>4->4</title>\n",
|
|
"<path d=\"M97.8216,-124.669C108.008,-124.877 116.475,-123.32 116.475,-120 116.475,-117.51 111.712,-116.012 105.034,-115.506\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"97.8216,-115.331 104.896,-112.352 101.321,-115.416 104.82,-115.501 104.82,-115.501 104.82,-115.501 101.321,-115.416 104.743,-118.65 97.8216,-115.331 97.8216,-115.331\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"116.475\" y=\"-123.8\">!b & !c</text>\n",
|
|
"<text fill=\"#1f78b4\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"128.975\" y=\"-108.8\">\u24ff</text>\n",
|
|
"</g>\n",
|
|
"<!-- 4->4 -->\n",
|
|
"<g class=\"edge\" id=\"edge18\"><title>4->4</title>\n",
|
|
"<path d=\"M96.3425,-127.45C123.162,-131.565 157.475,-129.082 157.475,-120 157.475,-111.698 128.806,-108.91 103.396,-111.635\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"96.3425,-112.55 102.879,-108.526 99.8135,-112.1 103.284,-111.65 103.284,-111.65 103.284,-111.65 99.8135,-112.1 103.69,-114.773 96.3425,-112.55 96.3425,-112.55\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"157.475\" y=\"-123.8\">b & !c</text>\n",
|
|
"<text fill=\"#1f78b4\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"159.975\" y=\"-109.8\">\u24ff</text>\n",
|
|
"<text fill=\"#ff7f00\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"175.975\" y=\"-109.8\">\u2777</text>\n",
|
|
"</g>\n",
|
|
"</g>\n",
|
|
"</svg></td></tr></table>"
|
|
],
|
|
"metadata": {},
|
|
"output_type": "display_data",
|
|
"text": [
|
|
"<IPython.core.display.HTML object>"
|
|
]
|
|
},
|
|
{
|
|
"output_type": "stream",
|
|
"stream": "stdout",
|
|
"text": [
|
|
"yes\n"
|
|
]
|
|
}
|
|
],
|
|
"prompt_number": 9
|
|
},
|
|
{
|
|
"cell_type": "markdown",
|
|
"metadata": {},
|
|
"source": [
|
|
"For development, it is useful to know that we can force the automaton printer to show the real state numbers (not the pairs) by passing option `1`, and that we can retrieve the associated pairs ourselves."
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"collapsed": false,
|
|
"input": [
|
|
"display(p3.show('.1'))\n",
|
|
"pairs = p3.get_product_states()\n",
|
|
"for s in range(p3.num_states()):\n",
|
|
" print(\"{}: {}\".format(s, pairs[s]))"
|
|
],
|
|
"language": "python",
|
|
"metadata": {},
|
|
"outputs": [
|
|
{
|
|
"metadata": {},
|
|
"output_type": "display_data",
|
|
"svg": [
|
|
"<svg height=\"249pt\" viewBox=\"0.00 0.00 592.00 249.00\" width=\"592pt\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
|
|
"<g class=\"graph\" id=\"graph0\" transform=\"scale(1 1) rotate(0) translate(4 245)\">\n",
|
|
"<title>G</title>\n",
|
|
"<polygon fill=\"white\" points=\"-4,4 -4,-245 588,-245 588,4 -4,4\" stroke=\"none\"/>\n",
|
|
"<!-- I -->\n",
|
|
"<!-- 0 -->\n",
|
|
"<g class=\"node\" id=\"node2\"><title>0</title>\n",
|
|
"<ellipse cx=\"56\" cy=\"-126\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"56\" y=\"-122.3\">0</text>\n",
|
|
"</g>\n",
|
|
"<!-- I->0 -->\n",
|
|
"<g class=\"edge\" id=\"edge1\"><title>I->0</title>\n",
|
|
"<path d=\"M1.15491,-126C2.79388,-126 17.1543,-126 30.6317,-126\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"37.9419,-126 30.9419,-129.15 34.4419,-126 30.9419,-126 30.9419,-126 30.9419,-126 34.4419,-126 30.9418,-122.85 37.9419,-126 37.9419,-126\" stroke=\"black\"/>\n",
|
|
"</g>\n",
|
|
"<!-- 1 -->\n",
|
|
"<g class=\"node\" id=\"node3\"><title>1</title>\n",
|
|
"<ellipse cx=\"167.5\" cy=\"-177\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"167.5\" y=\"-173.3\">1</text>\n",
|
|
"</g>\n",
|
|
"<!-- 0->1 -->\n",
|
|
"<g class=\"edge\" id=\"edge2\"><title>0->1</title>\n",
|
|
"<path d=\"M69.3825,-138.379C75.7038,-144.118 83.782,-150.622 92,-155 107.854,-163.447 127.38,-169.06 142.464,-172.501\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"149.476,-174.019 141.968,-175.617 146.055,-173.278 142.635,-172.538 142.635,-172.538 142.635,-172.538 146.055,-173.278 143.301,-169.459 149.476,-174.019 149.476,-174.019\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"92\" y=\"-186.8\">!b & c</text>\n",
|
|
"<text fill=\"#ff4da0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"102.5\" y=\"-171.8\">\u2776</text>\n",
|
|
"</g>\n",
|
|
"<!-- 0->1 -->\n",
|
|
"<g class=\"edge\" id=\"edge3\"><title>0->1</title>\n",
|
|
"<path d=\"M73.4593,-120.844C88.7526,-117.047 111.706,-113.955 129,-123 141.513,-129.545 150.69,-142.376 156.833,-153.888\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"160.101,-160.457 154.162,-155.593 158.542,-157.323 156.983,-154.19 156.983,-154.19 156.983,-154.19 158.542,-157.323 159.803,-152.787 160.101,-160.457 160.101,-160.457\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"106\" y=\"-140.8\">b</text>\n",
|
|
"<text fill=\"#ff4da0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"94.5\" y=\"-126.8\">\u2776</text>\n",
|
|
"<text fill=\"#ff7f00\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"110.5\" y=\"-126.8\">\u2777</text>\n",
|
|
"</g>\n",
|
|
"<!-- 2 -->\n",
|
|
"<g class=\"node\" id=\"node4\"><title>2</title>\n",
|
|
"<ellipse cx=\"308\" cy=\"-126\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"308\" y=\"-122.3\">2</text>\n",
|
|
"</g>\n",
|
|
"<!-- 0->2 -->\n",
|
|
"<g class=\"edge\" id=\"edge4\"><title>0->2</title>\n",
|
|
"<path d=\"M72.7114,-118.909C78.6337,-116.574 85.5086,-114.255 92,-113 170.557,-97.8128 193.821,-92.9776 272,-110 276.456,-110.97 281.023,-112.56 285.326,-114.371\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"291.816,-117.34 284.14,-117.292 288.634,-115.884 285.451,-114.428 285.451,-114.428 285.451,-114.428 288.634,-115.884 286.761,-111.563 291.816,-117.34 291.816,-117.34\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"147\" y=\"-105.8\">!b & !c</text>\n",
|
|
"</g>\n",
|
|
"<!-- 1->1 -->\n",
|
|
"<g class=\"edge\" id=\"edge5\"><title>1->1</title>\n",
|
|
"<path d=\"M157.925,-192.541C155.23,-202.909 158.422,-213 167.5,-213 174.45,-213 177.95,-207.085 177.999,-199.659\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"177.075,-192.541 181.1,-199.077 177.526,-196.012 177.977,-199.483 177.977,-199.483 177.977,-199.483 177.526,-196.012 174.853,-199.889 177.075,-192.541 177.075,-192.541\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"136.5\" y=\"-230.8\">a & !b & c</text>\n",
|
|
"<text fill=\"#1f78b4\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"151.5\" y=\"-216.8\">\u24ff</text>\n",
|
|
"<text fill=\"#ff4da0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"167.5\" y=\"-216.8\">\u2776</text>\n",
|
|
"</g>\n",
|
|
"<!-- 1->2 -->\n",
|
|
"<g class=\"edge\" id=\"edge6\"><title>1->2</title>\n",
|
|
"<path d=\"M185.802,-175.86C207.043,-173.902 243.724,-168.683 272,-155 278.155,-152.021 284.154,-147.736 289.397,-143.371\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"294.76,-138.66 291.58,-145.646 292.131,-140.97 289.501,-143.279 289.501,-143.279 289.501,-143.279 292.131,-140.97 287.422,-140.912 294.76,-138.66 294.76,-138.66\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"206\" y=\"-191.8\">a & !b & !c</text>\n",
|
|
"<text fill=\"#1f78b4\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"231\" y=\"-176.8\">\u24ff</text>\n",
|
|
"</g>\n",
|
|
"<!-- 3 -->\n",
|
|
"<g class=\"node\" id=\"node5\"><title>3</title>\n",
|
|
"<ellipse cx=\"560\" cy=\"-122\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"560\" y=\"-118.3\">3</text>\n",
|
|
"</g>\n",
|
|
"<!-- 1->3 -->\n",
|
|
"<g class=\"edge\" id=\"edge7\"><title>1->3</title>\n",
|
|
"<path d=\"M180.347,-189.973C187.141,-196.432 196.244,-203.578 206,-207 247.446,-221.538 369.129,-210.747 458,-192 488.395,-185.588 498.955,-187.376 524,-169 533.197,-162.252 541.052,-152.399 546.976,-143.455\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"550.762,-137.458 549.689,-145.059 548.893,-140.417 547.025,-143.377 547.025,-143.377 547.025,-143.377 548.893,-140.417 544.361,-141.696 550.762,-137.458 550.762,-137.458\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"363.5\" y=\"-226.8\">b</text>\n",
|
|
"<text fill=\"#1f78b4\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"344\" y=\"-212.8\">\u24ff</text>\n",
|
|
"<text fill=\"#ff4da0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"360\" y=\"-212.8\">\u2776</text>\n",
|
|
"<text fill=\"#ff7f00\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"376\" y=\"-212.8\">\u2777</text>\n",
|
|
"</g>\n",
|
|
"<!-- 2->1 -->\n",
|
|
"<g class=\"edge\" id=\"edge8\"><title>2->1</title>\n",
|
|
"<path d=\"M290.514,-120.823C269.563,-115.249 232.892,-108.934 206,-123 193.487,-129.545 184.31,-142.376 178.167,-153.888\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"174.899,-160.457 175.197,-152.787 176.458,-157.323 178.017,-154.19 178.017,-154.19 178.017,-154.19 176.458,-157.323 180.838,-155.593 174.899,-160.457 174.899,-160.457\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"208\" y=\"-140.8\">a & !b & c</text>\n",
|
|
"<text fill=\"#1f78b4\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"223\" y=\"-126.8\">\u24ff</text>\n",
|
|
"<text fill=\"#ff4da0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"239\" y=\"-126.8\">\u2776</text>\n",
|
|
"</g>\n",
|
|
"<!-- 2->2 -->\n",
|
|
"<g class=\"edge\" id=\"edge9\"><title>2->2</title>\n",
|
|
"<path d=\"M297.849,-141.167C294.772,-151.664 298.156,-162 308,-162 315.537,-162 319.287,-155.941 319.25,-148.39\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"318.151,-141.167 322.318,-147.614 318.678,-144.627 319.204,-148.087 319.204,-148.087 319.204,-148.087 318.678,-144.627 316.09,-148.561 318.151,-141.167 318.151,-141.167\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"275\" y=\"-180.8\">a & !b & !c</text>\n",
|
|
"<text fill=\"#1f78b4\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"300\" y=\"-165.8\">\u24ff</text>\n",
|
|
"</g>\n",
|
|
"<!-- 2->3 -->\n",
|
|
"<g class=\"edge\" id=\"edge10\"><title>2->3</title>\n",
|
|
"<path d=\"M324.94,-132.618C361.385,-146.743 453.12,-176.549 524,-151 530.542,-148.642 536.728,-144.471 542.027,-140.014\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"547.404,-135.139 544.334,-142.174 544.811,-137.49 542.218,-139.841 542.218,-139.841 542.218,-139.841 544.811,-137.49 540.102,-137.507 547.404,-135.139 547.404,-135.139\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"417\" y=\"-177.8\">b & c</text>\n",
|
|
"<text fill=\"#1f78b4\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"410\" y=\"-163.8\">\u24ff</text>\n",
|
|
"<text fill=\"#ff4da0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"426\" y=\"-163.8\">\u2776</text>\n",
|
|
"<text fill=\"#ff7f00\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"442\" y=\"-163.8\">\u2777</text>\n",
|
|
"</g>\n",
|
|
"<!-- 4 -->\n",
|
|
"<g class=\"node\" id=\"node6\"><title>4</title>\n",
|
|
"<ellipse cx=\"434\" cy=\"-18\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"434\" y=\"-14.3\">4</text>\n",
|
|
"</g>\n",
|
|
"<!-- 2->4 -->\n",
|
|
"<g class=\"edge\" id=\"edge11\"><title>2->4</title>\n",
|
|
"<path d=\"M322.27,-114.442C344.459,-95.1167 389.141,-56.1998 414.437,-34.1681\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"419.825,-29.4748 416.616,-36.4477 417.186,-31.7735 414.547,-34.0723 414.547,-34.0723 414.547,-34.0723 417.186,-31.7735 412.478,-31.6969 419.825,-29.4748 419.825,-29.4748\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"349.5\" y=\"-111.8\">b & !c</text>\n",
|
|
"<text fill=\"#1f78b4\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"352\" y=\"-97.8\">\u24ff</text>\n",
|
|
"<text fill=\"#ff7f00\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"368\" y=\"-97.8\">\u2777</text>\n",
|
|
"</g>\n",
|
|
"<!-- 3->3 -->\n",
|
|
"<g class=\"edge\" id=\"edge12\"><title>3->3</title>\n",
|
|
"<path d=\"M554.644,-139.41C553.644,-149.088 555.43,-158 560,-158 563.356,-158 565.211,-153.194 565.563,-146.807\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"565.356,-139.41 568.701,-146.319 565.454,-142.909 565.552,-146.407 565.552,-146.407 565.552,-146.407 565.454,-142.909 562.403,-146.495 565.356,-139.41 565.356,-139.41\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"541.5\" y=\"-175.8\">!b & c</text>\n",
|
|
"<text fill=\"#1f78b4\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"544\" y=\"-161.8\">\u24ff</text>\n",
|
|
"<text fill=\"#ff4da0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"560\" y=\"-161.8\">\u2776</text>\n",
|
|
"</g>\n",
|
|
"<!-- 3->3 -->\n",
|
|
"<g class=\"edge\" id=\"edge13\"><title>3->3</title>\n",
|
|
"<path d=\"M551.925,-138.318C545.824,-159.036 548.516,-186 560,-186 570.228,-186 573.482,-164.612 569.761,-145.297\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"568.075,-138.318 572.781,-144.382 568.897,-141.72 569.719,-145.122 569.719,-145.122 569.719,-145.122 568.897,-141.72 566.657,-145.862 568.075,-138.318 568.075,-138.318\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"555.5\" y=\"-203.8\">b</text>\n",
|
|
"<text fill=\"#1f78b4\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"536\" y=\"-189.8\">\u24ff</text>\n",
|
|
"<text fill=\"#ff4da0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"552\" y=\"-189.8\">\u2776</text>\n",
|
|
"<text fill=\"#ff7f00\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"568\" y=\"-189.8\">\u2777</text>\n",
|
|
"</g>\n",
|
|
"<!-- 3->4 -->\n",
|
|
"<g class=\"edge\" id=\"edge14\"><title>3->4</title>\n",
|
|
"<path d=\"M558.767,-103.826C557.363,-79.8765 550.913,-38.5086 524,-19 505.251,-5.40945 477.956,-7.38732 458.544,-11.3639\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"451.524,-12.9575 457.653,-8.33586 454.938,-12.1826 458.351,-11.4077 458.351,-11.4077 458.351,-11.4077 454.938,-12.1826 459.048,-14.4795 451.524,-12.9575 451.524,-12.9575\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"479.5\" y=\"-37.8\">!b & !c</text>\n",
|
|
"<text fill=\"#1f78b4\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"492\" y=\"-22.8\">\u24ff</text>\n",
|
|
"</g>\n",
|
|
"<!-- 4->3 -->\n",
|
|
"<g class=\"edge\" id=\"edge15\"><title>4->3</title>\n",
|
|
"<path d=\"M439.138,-35.4338C444.487,-54.1502 455.631,-83.4228 476,-100 492.592,-113.503 516.662,-118.781 534.614,-120.811\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"541.893,-121.497 534.628,-123.977 538.408,-121.169 534.924,-120.841 534.924,-120.841 534.924,-120.841 538.408,-121.169 535.22,-117.704 541.893,-121.497 541.893,-121.497\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"481.5\" y=\"-136.8\">!b & c</text>\n",
|
|
"<text fill=\"#1f78b4\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"484\" y=\"-122.8\">\u24ff</text>\n",
|
|
"<text fill=\"#ff4da0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"500\" y=\"-122.8\">\u2776</text>\n",
|
|
"</g>\n",
|
|
"<!-- 4->3 -->\n",
|
|
"<g class=\"edge\" id=\"edge16\"><title>4->3</title>\n",
|
|
"<path d=\"M448.032,-29.3018C455.793,-35.6525 466.043,-43.4025 476,-49 496,-60.2437 506.251,-53.4607 524,-68 534.306,-76.4424 542.605,-88.7369 548.531,-99.4628\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"551.91,-105.89 545.864,-101.16 550.281,-102.792 548.653,-99.6944 548.653,-99.6944 548.653,-99.6944 550.281,-102.792 551.441,-98.2283 551.91,-105.89 551.91,-105.89\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"483\" y=\"-85.8\">b & c</text>\n",
|
|
"<text fill=\"#1f78b4\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"476\" y=\"-71.8\">\u24ff</text>\n",
|
|
"<text fill=\"#ff4da0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"492\" y=\"-71.8\">\u2776</text>\n",
|
|
"<text fill=\"#ff7f00\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"508\" y=\"-71.8\">\u2777</text>\n",
|
|
"</g>\n",
|
|
"<!-- 4->4 -->\n",
|
|
"<g class=\"edge\" id=\"edge17\"><title>4->4</title>\n",
|
|
"<path d=\"M428.152,-35.0373C426.959,-44.8579 428.908,-54 434,-54 437.819,-54 439.87,-48.8576 440.153,-42.1433\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"439.848,-35.0373 443.296,-41.8954 439.998,-38.5341 440.149,-42.0308 440.149,-42.0308 440.149,-42.0308 439.998,-38.5341 437.002,-42.1663 439.848,-35.0373 439.848,-35.0373\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"413.5\" y=\"-72.8\">!b & !c</text>\n",
|
|
"<text fill=\"#1f78b4\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"426\" y=\"-57.8\">\u24ff</text>\n",
|
|
"</g>\n",
|
|
"<!-- 4->4 -->\n",
|
|
"<g class=\"edge\" id=\"edge18\"><title>4->4</title>\n",
|
|
"<path d=\"M425.326,-33.947C418.347,-55.2861 421.238,-84 434,-84 445.416,-84 448.933,-61.0236 444.553,-40.9026\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"442.674,-33.947 447.54,-39.8834 443.587,-37.3259 444.499,-40.7048 444.499,-40.7048 444.499,-40.7048 443.587,-37.3259 441.458,-41.5263 442.674,-33.947 442.674,-33.947\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"415.5\" y=\"-101.8\">b & !c</text>\n",
|
|
"<text fill=\"#1f78b4\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"418\" y=\"-87.8\">\u24ff</text>\n",
|
|
"<text fill=\"#ff7f00\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"434\" y=\"-87.8\">\u2777</text>\n",
|
|
"</g>\n",
|
|
"</g>\n",
|
|
"</svg>"
|
|
],
|
|
"text": [
|
|
"<IPython.core.display.SVG object>"
|
|
]
|
|
},
|
|
{
|
|
"output_type": "stream",
|
|
"stream": "stdout",
|
|
"text": [
|
|
"0: (1, 0)\n",
|
|
"1: (0, 0)\n",
|
|
"2: (0, 1)\n",
|
|
"3: (2, 0)\n",
|
|
"4: (2, 1)\n"
|
|
]
|
|
}
|
|
],
|
|
"prompt_number": 10
|
|
},
|
|
{
|
|
"cell_type": "markdown",
|
|
"metadata": {},
|
|
"source": [
|
|
"# Timings\n",
|
|
"\n",
|
|
"As an indication of how slow it is to implement such an algorithm using the Python bindings of Spot, consider the following comparison:"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"collapsed": false,
|
|
"input": [
|
|
"%timeit product3(a1, a2)"
|
|
],
|
|
"language": "python",
|
|
"metadata": {},
|
|
"outputs": [
|
|
{
|
|
"output_type": "stream",
|
|
"stream": "stdout",
|
|
"text": [
|
|
"1000 loops, best of 3: 231 \u00b5s per loop\n"
|
|
]
|
|
}
|
|
],
|
|
"prompt_number": 11
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"collapsed": false,
|
|
"input": [
|
|
"%timeit spot.product(a1, a2)"
|
|
],
|
|
"language": "python",
|
|
"metadata": {},
|
|
"outputs": [
|
|
{
|
|
"output_type": "stream",
|
|
"stream": "stdout",
|
|
"text": [
|
|
"The slowest run took 5.96 times longer than the fastest. This could mean that an intermediate result is being cached.\n",
|
|
"100000 loops, best of 3: 4.6 \u00b5s per loop\n"
|
|
]
|
|
}
|
|
],
|
|
"prompt_number": 12
|
|
},
|
|
{
|
|
"cell_type": "markdown",
|
|
"metadata": {},
|
|
"source": [
|
|
"Depending on the machine where this notebook has been run, using the C++ version of the product can be 1 to 2 order of magnitude faster. This is due to all the type conversions (converting Python types to C++ types) that occurs everytime a function/method of Spot is called from Python. When calling high-level C++ functions (such as `spot.product()`) from Python, the overhead is negligible because most of the time is spent on the C++ side, actually executing the function. However when calling low-level functions (such as `new_edge()`, `new_state()`, `out()`) most of the time is spent converting the arguments from Python to C++ and the results from C++ to Python.\n",
|
|
"\n",
|
|
"Despite that speed difference, Python can be useful to prototype an algorithm before implementing it in C++."
|
|
]
|
|
}
|
|
],
|
|
"metadata": {}
|
|
}
|
|
]
|
|
}
|