python: make it possible to modify edges during iteration
Reported by Laurent Xu. * python/spot/impl.i: Fix the iterator to return pointers instead of references. Because references are ultimately copied. * tests/python/automata.ipynb: Add test cases. * NEWS: Mention it.
This commit is contained in:
parent
09c6393942
commit
d271dfd592
3 changed files with 215 additions and 32 deletions
3
NEWS
3
NEWS
|
|
@ -165,6 +165,9 @@ New in spot 2.0.3a (not yet released)
|
|||
|
||||
* Bindings for randomize() were added.
|
||||
|
||||
* Iterating over edges via "aut.out(s)" or "aut.edges()"
|
||||
now allows modifying the edge fields.
|
||||
|
||||
* Under IPython the spot.ltsmin module now offers a
|
||||
%%pml magic to define promela models, compile them
|
||||
with spins, and dynamically load them. This is
|
||||
|
|
|
|||
|
|
@ -163,14 +163,16 @@ using namespace spot;
|
|||
%}
|
||||
|
||||
|
||||
// Swig come with iterators that implement a decrement method.
|
||||
// This is not supported in our "successor" iterators.
|
||||
// Swig come with iterators that implement a decrement method. This
|
||||
// is not supported in our "successor" iterators. Also we want
|
||||
// iterators to return pointers so that data can be modified during
|
||||
// iteration.
|
||||
%fragment("ForwardIterator_T","header",fragment="SwigPyIterator_T") {
|
||||
namespace swig
|
||||
{
|
||||
template<typename OutIterator,
|
||||
typename ValueType =
|
||||
typename std::iterator_traits<OutIterator>::value_type,
|
||||
typename std::iterator_traits<OutIterator>::pointer,
|
||||
typename FromOper = from_oper<ValueType> >
|
||||
class ForwardIterator_T : public SwigPyIterator_T<OutIterator>
|
||||
{
|
||||
|
|
@ -191,7 +193,7 @@ namespace swig
|
|||
if (base::current == end) {
|
||||
throw stop_iteration();
|
||||
} else {
|
||||
return from(static_cast<const value_type&>(*(base::current)));
|
||||
return from(static_cast<value_type>(&*(base::current)));
|
||||
}
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -18,7 +18,7 @@
|
|||
"version": "3.4.3+"
|
||||
},
|
||||
"name": "",
|
||||
"signature": "sha256:29d335e40a65f0ca04a3b2b07bfcbf92f794407b413644546d957487dcbf4bb1"
|
||||
"signature": "sha256:91af67353e0a35fefd672b53bd005af28720c0c7a8dfc922ce70fa8f3ef6a42e"
|
||||
},
|
||||
"nbformat": 3,
|
||||
"nbformat_minor": 0,
|
||||
|
|
@ -178,7 +178,7 @@
|
|||
"</svg>\n"
|
||||
],
|
||||
"text": [
|
||||
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f09a8369240> >"
|
||||
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f5fc0c24900> >"
|
||||
]
|
||||
}
|
||||
],
|
||||
|
|
@ -317,7 +317,7 @@
|
|||
"</svg>"
|
||||
],
|
||||
"text": [
|
||||
"<IPython.core.display.SVG at 0x7f09a13dd5f8>"
|
||||
"<IPython.core.display.SVG at 0x7f5fc18bd1d0>"
|
||||
]
|
||||
}
|
||||
],
|
||||
|
|
@ -470,7 +470,7 @@
|
|||
"</svg>"
|
||||
],
|
||||
"text": [
|
||||
"<IPython.core.display.SVG at 0x7f09a074abe0>"
|
||||
"<IPython.core.display.SVG at 0x7f5fc013a710>"
|
||||
]
|
||||
}
|
||||
],
|
||||
|
|
@ -570,7 +570,7 @@
|
|||
"</svg>\n"
|
||||
],
|
||||
"text": [
|
||||
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f09a8323fc0> >"
|
||||
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f5fc866e1b0> >"
|
||||
]
|
||||
}
|
||||
],
|
||||
|
|
@ -640,7 +640,7 @@
|
|||
"</svg>\n"
|
||||
],
|
||||
"text": [
|
||||
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f09a8323e70> >"
|
||||
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f5fc866e060> >"
|
||||
]
|
||||
}
|
||||
],
|
||||
|
|
@ -716,7 +716,7 @@
|
|||
"</svg>\n"
|
||||
],
|
||||
"text": [
|
||||
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f09a8323f00> >"
|
||||
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f5fc866e0f0> >"
|
||||
]
|
||||
}
|
||||
],
|
||||
|
|
@ -839,7 +839,7 @@
|
|||
"</svg>"
|
||||
],
|
||||
"text": [
|
||||
"<IPython.core.display.SVG at 0x7f09a0773da0>"
|
||||
"<IPython.core.display.SVG at 0x7f5fc013a908>"
|
||||
]
|
||||
}
|
||||
],
|
||||
|
|
@ -1029,7 +1029,7 @@
|
|||
"</svg>"
|
||||
],
|
||||
"text": [
|
||||
"<IPython.core.display.SVG at 0x7f098bfe96d8>"
|
||||
"<IPython.core.display.SVG at 0x7f5fc0101978>"
|
||||
]
|
||||
}
|
||||
],
|
||||
|
|
@ -1176,7 +1176,7 @@
|
|||
"</svg>\n"
|
||||
],
|
||||
"text": [
|
||||
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f09a8323f30> >"
|
||||
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f5fc866e300> >"
|
||||
]
|
||||
}
|
||||
],
|
||||
|
|
@ -1277,7 +1277,7 @@
|
|||
"</svg>\n"
|
||||
],
|
||||
"text": [
|
||||
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f098bff3210> >"
|
||||
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f5fc866e2d0> >"
|
||||
]
|
||||
}
|
||||
],
|
||||
|
|
@ -1395,7 +1395,7 @@
|
|||
"</svg>\n"
|
||||
],
|
||||
"text": [
|
||||
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f098bff3240> >"
|
||||
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f5fc866e120> >"
|
||||
]
|
||||
}
|
||||
],
|
||||
|
|
@ -1494,7 +1494,7 @@
|
|||
"</svg>\n"
|
||||
],
|
||||
"text": [
|
||||
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f098bff3270> >"
|
||||
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f5fc866e330> >"
|
||||
]
|
||||
}
|
||||
],
|
||||
|
|
@ -1964,7 +1964,7 @@
|
|||
"</svg>\n"
|
||||
],
|
||||
"text": [
|
||||
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f09a8323ed0> >"
|
||||
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f5fc866e2a0> >"
|
||||
]
|
||||
}
|
||||
],
|
||||
|
|
@ -2161,7 +2161,7 @@
|
|||
"</svg>"
|
||||
],
|
||||
"text": [
|
||||
"<IPython.core.display.SVG at 0x7f09a0703dd8>"
|
||||
"<IPython.core.display.SVG at 0x7f5fc00cd3c8>"
|
||||
]
|
||||
},
|
||||
{
|
||||
|
|
@ -2286,7 +2286,7 @@
|
|||
"</svg>"
|
||||
],
|
||||
"text": [
|
||||
"<IPython.core.display.SVG at 0x7f09a0734198>"
|
||||
"<IPython.core.display.SVG at 0x7f5fc00d38d0>"
|
||||
]
|
||||
},
|
||||
{
|
||||
|
|
@ -2428,7 +2428,7 @@
|
|||
"</svg>"
|
||||
],
|
||||
"text": [
|
||||
"<IPython.core.display.SVG at 0x7f09a06db400>"
|
||||
"<IPython.core.display.SVG at 0x7f5fc014cb38>"
|
||||
]
|
||||
},
|
||||
{
|
||||
|
|
@ -2579,7 +2579,7 @@
|
|||
"</svg>\n"
|
||||
],
|
||||
"text": [
|
||||
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f098bff33f0> >"
|
||||
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f5fc0b98ae0> >"
|
||||
]
|
||||
}
|
||||
],
|
||||
|
|
@ -2735,7 +2735,7 @@
|
|||
"</svg>\n"
|
||||
],
|
||||
"text": [
|
||||
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f09a8323c60> >"
|
||||
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f5fc0b98fc0> >"
|
||||
]
|
||||
}
|
||||
],
|
||||
|
|
@ -2805,7 +2805,7 @@
|
|||
"</svg>\n"
|
||||
],
|
||||
"text": [
|
||||
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f098bff31b0> >"
|
||||
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f5fc0b98ae0> >"
|
||||
]
|
||||
}
|
||||
],
|
||||
|
|
@ -2877,7 +2877,7 @@
|
|||
"</svg>"
|
||||
],
|
||||
"text": [
|
||||
"<IPython.core.display.SVG at 0x7f09a06980f0>"
|
||||
"<IPython.core.display.SVG at 0x7f5fc00e4a20>"
|
||||
]
|
||||
},
|
||||
{
|
||||
|
|
@ -2930,7 +2930,7 @@
|
|||
"</svg>"
|
||||
],
|
||||
"text": [
|
||||
"<IPython.core.display.SVG at 0x7f09a0682358>"
|
||||
"<IPython.core.display.SVG at 0x7f5fc010f828>"
|
||||
]
|
||||
},
|
||||
{
|
||||
|
|
@ -3042,7 +3042,7 @@
|
|||
"</svg>"
|
||||
],
|
||||
"text": [
|
||||
"<IPython.core.display.SVG at 0x7f09a0742908>"
|
||||
"<IPython.core.display.SVG at 0x7f5fc01223c8>"
|
||||
]
|
||||
},
|
||||
{
|
||||
|
|
@ -3154,7 +3154,7 @@
|
|||
"</svg>"
|
||||
],
|
||||
"text": [
|
||||
"<IPython.core.display.SVG at 0x7f09a0742828>"
|
||||
"<IPython.core.display.SVG at 0x7f5fc00fcc88>"
|
||||
]
|
||||
}
|
||||
],
|
||||
|
|
@ -3232,7 +3232,7 @@
|
|||
"</svg>\n"
|
||||
],
|
||||
"text": [
|
||||
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f09a82ac5d0> >"
|
||||
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f5fc866e390> >"
|
||||
]
|
||||
},
|
||||
{
|
||||
|
|
@ -3315,7 +3315,7 @@
|
|||
"</svg>"
|
||||
],
|
||||
"text": [
|
||||
"<IPython.core.display.SVG at 0x7f09a06db4a8>"
|
||||
"<IPython.core.display.SVG at 0x7f5fc00c0cf8>"
|
||||
]
|
||||
}
|
||||
],
|
||||
|
|
@ -3332,7 +3332,7 @@
|
|||
"cell_type": "code",
|
||||
"collapsed": false,
|
||||
"input": [
|
||||
"spot.translate('FGa', 'generic', 'deterministic')"
|
||||
"aut = spot.translate('FGa', 'generic', 'deterministic'); aut"
|
||||
],
|
||||
"language": "python",
|
||||
"metadata": {},
|
||||
|
|
@ -3400,11 +3400,189 @@
|
|||
"</svg>\n"
|
||||
],
|
||||
"text": [
|
||||
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f09a82ac480> >"
|
||||
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f5fc85824e0> >"
|
||||
]
|
||||
}
|
||||
],
|
||||
"prompt_number": 26
|
||||
},
|
||||
{
|
||||
"cell_type": "markdown",
|
||||
"metadata": {},
|
||||
"source": [
|
||||
"Adding an automatic proposition to all edges"
|
||||
]
|
||||
},
|
||||
{
|
||||
"cell_type": "code",
|
||||
"collapsed": false,
|
||||
"input": [
|
||||
"import buddy\n",
|
||||
"b = buddy.bdd_ithvar(aut.register_ap('b'))\n",
|
||||
"for e in aut.edges():\n",
|
||||
" e.cond &= b\n",
|
||||
"aut"
|
||||
],
|
||||
"language": "python",
|
||||
"metadata": {},
|
||||
"outputs": [
|
||||
{
|
||||
"metadata": {},
|
||||
"output_type": "pyout",
|
||||
"prompt_number": 27,
|
||||
"svg": [
|
||||
"<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n",
|
||||
"<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n",
|
||||
" \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n",
|
||||
"<!-- Generated by graphviz version 2.38.0 (20140413.2041)\n",
|
||||
" -->\n",
|
||||
"<!-- Title: G Pages: 1 -->\n",
|
||||
"<svg width=\"191pt\" height=\"107pt\"\n",
|
||||
" viewBox=\"0.00 0.00 191.00 107.18\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
|
||||
"<g id=\"graph0\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 103.182)\">\n",
|
||||
"<title>G</title>\n",
|
||||
"<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-103.182 187,-103.182 187,4 -4,4\"/>\n",
|
||||
"<!-- I -->\n",
|
||||
"<!-- 0 -->\n",
|
||||
"<g id=\"node2\" class=\"node\"><title>0</title>\n",
|
||||
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"56\" cy=\"-33.1822\" rx=\"18\" ry=\"18\"/>\n",
|
||||
"<text text-anchor=\"middle\" x=\"56\" y=\"-29.4822\" font-family=\"Lato\" font-size=\"14.00\">0</text>\n",
|
||||
"</g>\n",
|
||||
"<!-- I->0 -->\n",
|
||||
"<g id=\"edge1\" class=\"edge\"><title>I->0</title>\n",
|
||||
"<path fill=\"none\" stroke=\"black\" d=\"M1.15491,-33.1822C2.79388,-33.1822 17.1543,-33.1822 30.6317,-33.1822\"/>\n",
|
||||
"<polygon fill=\"black\" stroke=\"black\" points=\"37.9419,-33.1822 30.9419,-36.3323 34.4419,-33.1823 30.9419,-33.1823 30.9419,-33.1823 30.9419,-33.1823 34.4419,-33.1823 30.9418,-30.0323 37.9419,-33.1822 37.9419,-33.1822\"/>\n",
|
||||
"</g>\n",
|
||||
"<!-- 0->0 -->\n",
|
||||
"<g id=\"edge2\" class=\"edge\"><title>0->0</title>\n",
|
||||
"<path fill=\"none\" stroke=\"black\" d=\"M49.6208,-50.2195C48.3189,-60.0402 50.4453,-69.1822 56,-69.1822 60.166,-69.1822 62.4036,-64.0398 62.7128,-57.3255\"/>\n",
|
||||
"<polygon fill=\"black\" stroke=\"black\" points=\"62.3792,-50.2195 65.8541,-57.0641 62.5434,-53.7157 62.7076,-57.2118 62.7076,-57.2118 62.7076,-57.2118 62.5434,-53.7157 59.561,-57.3596 62.3792,-50.2195 62.3792,-50.2195\"/>\n",
|
||||
"<text text-anchor=\"start\" x=\"37.5\" y=\"-72.9822\" font-family=\"Lato\" font-size=\"14.00\">!a & b</text>\n",
|
||||
"</g>\n",
|
||||
"<!-- 1 -->\n",
|
||||
"<g id=\"node3\" class=\"node\"><title>1</title>\n",
|
||||
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"165\" cy=\"-33.1822\" rx=\"18\" ry=\"18\"/>\n",
|
||||
"<text text-anchor=\"middle\" x=\"165\" y=\"-29.4822\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
|
||||
"</g>\n",
|
||||
"<!-- 0->1 -->\n",
|
||||
"<g id=\"edge3\" class=\"edge\"><title>0->1</title>\n",
|
||||
"<path fill=\"none\" stroke=\"black\" d=\"M74.0378,-36.1107C79.731,-36.957 86.1223,-37.7645 92,-38.1822 108.403,-39.348 112.597,-39.348 129,-38.1822 132.49,-37.9342 136.161,-37.5488 139.759,-37.0994\"/>\n",
|
||||
"<polygon fill=\"black\" stroke=\"black\" points=\"146.962,-36.1107 140.456,-40.1834 143.495,-36.5867 140.027,-37.0627 140.027,-37.0627 140.027,-37.0627 143.495,-36.5867 139.599,-33.9419 146.962,-36.1107 146.962,-36.1107\"/>\n",
|
||||
"<text text-anchor=\"start\" x=\"93.5\" y=\"-56.9822\" font-family=\"Lato\" font-size=\"14.00\">a & b</text>\n",
|
||||
"<text text-anchor=\"start\" x=\"102.5\" y=\"-41.9822\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#f17cb0\">\u2776</text>\n",
|
||||
"</g>\n",
|
||||
"<!-- 1->0 -->\n",
|
||||
"<g id=\"edge4\" class=\"edge\"><title>1->0</title>\n",
|
||||
"<path fill=\"none\" stroke=\"black\" d=\"M152.404,-20.0434C146.156,-13.9661 137.908,-7.39333 129,-4.18224 113.53,1.39408 107.47,1.39408 92,-4.18224 85.4579,-6.54039 79.2724,-10.7115 73.9732,-15.168\"/>\n",
|
||||
"<polygon fill=\"black\" stroke=\"black\" points=\"68.596,-20.0434 71.6659,-13.0079 71.1889,-17.6925 73.7818,-15.3415 73.7818,-15.3415 73.7818,-15.3415 71.1889,-17.6925 75.8976,-17.6751 68.596,-20.0434 68.596,-20.0434\"/>\n",
|
||||
"<text text-anchor=\"start\" x=\"92\" y=\"-22.9822\" font-family=\"Lato\" font-size=\"14.00\">!a & b</text>\n",
|
||||
"<text text-anchor=\"start\" x=\"102.5\" y=\"-7.98224\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#5da5da\">\u24ff</text>\n",
|
||||
"</g>\n",
|
||||
"<!-- 1->1 -->\n",
|
||||
"<g id=\"edge5\" class=\"edge\"><title>1->1</title>\n",
|
||||
"<path fill=\"none\" stroke=\"black\" d=\"M155.767,-48.7237C153.169,-59.0909 156.246,-69.1822 165,-69.1822 171.702,-69.1822 175.077,-63.2669 175.124,-55.8413\"/>\n",
|
||||
"<polygon fill=\"black\" stroke=\"black\" points=\"174.233,-48.7237 178.229,-55.2777 174.668,-52.1965 175.103,-55.6694 175.103,-55.6694 175.103,-55.6694 174.668,-52.1965 171.977,-56.0611 174.233,-48.7237 174.233,-48.7237\"/>\n",
|
||||
"<text text-anchor=\"start\" x=\"148\" y=\"-87.9822\" font-family=\"Lato\" font-size=\"14.00\">a & b</text>\n",
|
||||
"<text text-anchor=\"start\" x=\"157\" y=\"-72.9822\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#f17cb0\">\u2776</text>\n",
|
||||
"</g>\n",
|
||||
"</g>\n",
|
||||
"</svg>\n"
|
||||
],
|
||||
"text": [
|
||||
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f5fc85824e0> >"
|
||||
]
|
||||
}
|
||||
],
|
||||
"prompt_number": 27
|
||||
},
|
||||
{
|
||||
"cell_type": "markdown",
|
||||
"metadata": {},
|
||||
"source": [
|
||||
"Adding an atomic proposition to the edge between 0 and 1:"
|
||||
]
|
||||
},
|
||||
{
|
||||
"cell_type": "code",
|
||||
"collapsed": false,
|
||||
"input": [
|
||||
"c = buddy.bdd_ithvar(aut.register_ap('c'))\n",
|
||||
"for e in aut.out(0):\n",
|
||||
" if e.dst == 1:\n",
|
||||
" e.cond &= c\n",
|
||||
"aut"
|
||||
],
|
||||
"language": "python",
|
||||
"metadata": {},
|
||||
"outputs": [
|
||||
{
|
||||
"metadata": {},
|
||||
"output_type": "pyout",
|
||||
"prompt_number": 28,
|
||||
"svg": [
|
||||
"<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n",
|
||||
"<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n",
|
||||
" \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n",
|
||||
"<!-- Generated by graphviz version 2.38.0 (20140413.2041)\n",
|
||||
" -->\n",
|
||||
"<!-- Title: G Pages: 1 -->\n",
|
||||
"<svg width=\"212pt\" height=\"110pt\"\n",
|
||||
" viewBox=\"0.00 0.00 212.00 109.56\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
|
||||
"<g id=\"graph0\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 105.556)\">\n",
|
||||
"<title>G</title>\n",
|
||||
"<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-105.556 208,-105.556 208,4 -4,4\"/>\n",
|
||||
"<!-- I -->\n",
|
||||
"<!-- 0 -->\n",
|
||||
"<g id=\"node2\" class=\"node\"><title>0</title>\n",
|
||||
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"56\" cy=\"-35.5559\" rx=\"18\" ry=\"18\"/>\n",
|
||||
"<text text-anchor=\"middle\" x=\"56\" y=\"-31.8559\" font-family=\"Lato\" font-size=\"14.00\">0</text>\n",
|
||||
"</g>\n",
|
||||
"<!-- I->0 -->\n",
|
||||
"<g id=\"edge1\" class=\"edge\"><title>I->0</title>\n",
|
||||
"<path fill=\"none\" stroke=\"black\" d=\"M1.15491,-35.5559C2.79388,-35.5559 17.1543,-35.5559 30.6317,-35.5559\"/>\n",
|
||||
"<polygon fill=\"black\" stroke=\"black\" points=\"37.9419,-35.5559 30.9419,-38.706 34.4419,-35.556 30.9419,-35.556 30.9419,-35.556 30.9419,-35.556 34.4419,-35.556 30.9418,-32.406 37.9419,-35.5559 37.9419,-35.5559\"/>\n",
|
||||
"</g>\n",
|
||||
"<!-- 0->0 -->\n",
|
||||
"<g id=\"edge2\" class=\"edge\"><title>0->0</title>\n",
|
||||
"<path fill=\"none\" stroke=\"black\" d=\"M49.6208,-52.5933C48.3189,-62.4139 50.4453,-71.5559 56,-71.5559 60.166,-71.5559 62.4036,-66.4135 62.7128,-59.6992\"/>\n",
|
||||
"<polygon fill=\"black\" stroke=\"black\" points=\"62.3792,-52.5933 65.8541,-59.4378 62.5434,-56.0894 62.7076,-59.5855 62.7076,-59.5855 62.7076,-59.5855 62.5434,-56.0894 59.561,-59.7333 62.3792,-52.5933 62.3792,-52.5933\"/>\n",
|
||||
"<text text-anchor=\"start\" x=\"37.5\" y=\"-75.3559\" font-family=\"Lato\" font-size=\"14.00\">!a & b</text>\n",
|
||||
"</g>\n",
|
||||
"<!-- 1 -->\n",
|
||||
"<g id=\"node3\" class=\"node\"><title>1</title>\n",
|
||||
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"186\" cy=\"-35.5559\" rx=\"18\" ry=\"18\"/>\n",
|
||||
"<text text-anchor=\"middle\" x=\"186\" y=\"-31.8559\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
|
||||
"</g>\n",
|
||||
"<!-- 0->1 -->\n",
|
||||
"<g id=\"edge3\" class=\"edge\"><title>0->1</title>\n",
|
||||
"<path fill=\"none\" stroke=\"black\" d=\"M74.0378,-38.4844C79.731,-39.3307 86.1223,-40.1382 92,-40.5559 117.713,-42.3833 124.287,-42.3833 150,-40.5559 153.49,-40.3079 157.161,-39.9225 160.759,-39.4731\"/>\n",
|
||||
"<polygon fill=\"black\" stroke=\"black\" points=\"167.962,-38.4844 161.456,-42.5571 164.495,-38.9604 161.027,-39.4364 161.027,-39.4364 161.027,-39.4364 164.495,-38.9604 160.599,-36.3156 167.962,-38.4844 167.962,-38.4844\"/>\n",
|
||||
"<text text-anchor=\"start\" x=\"92\" y=\"-60.3559\" font-family=\"Lato\" font-size=\"14.00\">a & b & c</text>\n",
|
||||
"<text text-anchor=\"start\" x=\"113\" y=\"-45.3559\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#f17cb0\">\u2776</text>\n",
|
||||
"</g>\n",
|
||||
"<!-- 1->0 -->\n",
|
||||
"<g id=\"edge4\" class=\"edge\"><title>1->0</title>\n",
|
||||
"<path fill=\"none\" stroke=\"black\" d=\"M173.404,-22.4171C167.156,-16.3398 158.908,-9.76704 150,-6.55595 125.75,2.18532 116.25,2.18532 92,-6.55595 85.4579,-8.91409 79.2724,-13.0852 73.9732,-17.5417\"/>\n",
|
||||
"<polygon fill=\"black\" stroke=\"black\" points=\"68.596,-22.4171 71.6659,-15.3816 71.1889,-20.0662 73.7818,-17.7152 73.7818,-17.7152 73.7818,-17.7152 71.1889,-20.0662 75.8976,-20.0488 68.596,-22.4171 68.596,-22.4171\"/>\n",
|
||||
"<text text-anchor=\"start\" x=\"102.5\" y=\"-25.3559\" font-family=\"Lato\" font-size=\"14.00\">!a & b</text>\n",
|
||||
"<text text-anchor=\"start\" x=\"113\" y=\"-10.3559\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#5da5da\">\u24ff</text>\n",
|
||||
"</g>\n",
|
||||
"<!-- 1->1 -->\n",
|
||||
"<g id=\"edge5\" class=\"edge\"><title>1->1</title>\n",
|
||||
"<path fill=\"none\" stroke=\"black\" d=\"M175.292,-50.3476C171.806,-60.9724 175.375,-71.5559 186,-71.5559 194.135,-71.5559 198.134,-65.3521 197.997,-57.6757\"/>\n",
|
||||
"<polygon fill=\"black\" stroke=\"black\" points=\"196.708,-50.3476 201.023,-56.6963 197.314,-53.7947 197.92,-57.2418 197.92,-57.2418 197.92,-57.2418 197.314,-53.7947 194.818,-57.7874 196.708,-50.3476 196.708,-50.3476\"/>\n",
|
||||
"<text text-anchor=\"start\" x=\"169\" y=\"-90.3559\" font-family=\"Lato\" font-size=\"14.00\">a & b</text>\n",
|
||||
"<text text-anchor=\"start\" x=\"178\" y=\"-75.3559\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#f17cb0\">\u2776</text>\n",
|
||||
"</g>\n",
|
||||
"</g>\n",
|
||||
"</svg>\n"
|
||||
],
|
||||
"text": [
|
||||
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f5fc85824e0> >"
|
||||
]
|
||||
}
|
||||
],
|
||||
"prompt_number": 28
|
||||
}
|
||||
],
|
||||
"metadata": {}
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue