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

remove_alternation: fix serious typo

Browse source 
Fixes #382.

* spot/twaalgos/alternation.cc: Here.
* tests/python/alternation.ipynb: Add test case.
* NEWS: Mention it.
This commit is contained in:
Alexandre Duret-Lutz 2019-03-22 22:16:02 +01:00
parent 510a18b156
commit ef106e2860
3 changed files with 613 additions and 72 deletions
Download patch file Download diff file Expand all files Collapse all files

3
NEWS
View file

@ -30,6 +30,9 @@ New in spot 2.7.2.dev (not yet released)
--stats would output the \r as part of the %> sequence instead
of ignoring it.
- Fix serious typo in removel_alternation() causing incorrect
output for some VWAA. Bug introduced in Spot 2.6.
New in spot 2.7.2 (2019-03-17)
Python:

5
spot/twaalgos/alternation.cc
View file

@ -233,7 +233,7 @@ namespace spot
{
int v = d->register_anonymous_variables(1, this);
scc_to_var_.emplace_back(v);
mark_to_state_.push_back(si_.one_state_of(c));
mark_to_state_.push_back(si_.one_state_of(s));
var_to_mark_.emplace(v, acc_cond::mark_t({mark_pos++}));
bdd bv = bdd_ithvar(v);
all_marks &= bv;
@ -449,7 +449,6 @@ namespace spot
for (unsigned se: s_to_ss[s])
bs &= state_as_bdd(se);
bdd ap = bdd_exist(bdd_support(bs), all_vars_);
bdd all_letters = bdd_exist(bs, all_vars_);
@ -468,7 +467,7 @@ namespace spot
v.clear();
acc_cond::mark_t m = bdd_to_state(dest, v);
// if there is no promise "f" is between a state
// if there is no promise "f" between a state
// that does not have f, and a state that have
// "f", we can add one. Doing so will help later
// simplifications performed by postprocessor. An

677
tests/python/alternation.ipynb
View file

@ -2770,79 +2770,78 @@
"<!-- Generated by graphviz version 2.40.1 (20161225.0304)\n",
" -->\n",
"<!-- Pages: 1 -->\n",
"<svg width=\"161pt\" height=\"360pt\"\n",
" viewBox=\"0.00 0.00 161.31 360.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
"<g id=\"graph0\" class=\"graph\" transform=\"scale(.6923 .6923) rotate(0) translate(4 516)\">\n",
"<polygon fill=\"#ffffff\" stroke=\"transparent\" points=\"-4,4 -4,-516 229,-516 229,4 -4,4\"/>\n",
"<text text-anchor=\"start\" x=\"65.5\" y=\"-497.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">Inf(</text>\n",
"<text text-anchor=\"start\" x=\"87.5\" y=\"-497.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">⓿</text>\n",
"<text text-anchor=\"start\" x=\"103.5\" y=\"-497.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">)&amp;Inf(</text>\n",
"<text text-anchor=\"start\" x=\"139.5\" y=\"-497.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#ff4da0\">❶</text>\n",
"<text text-anchor=\"start\" x=\"155.5\" y=\"-497.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">)</text>\n",
"<text text-anchor=\"start\" x=\"68.5\" y=\"-483.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">[gen. Büchi 2]</text>\n",
"<svg width=\"160pt\" height=\"360pt\"\n",
" viewBox=\"0.00 0.00 160.15 360.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
"<g id=\"graph0\" class=\"graph\" transform=\"scale(.6844 .6844) rotate(0) translate(4 522)\">\n",
"<polygon fill=\"#ffffff\" stroke=\"transparent\" points=\"-4,4 -4,-522 230,-522 230,4 -4,4\"/>\n",
"<text text-anchor=\"start\" x=\"66\" y=\"-503.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">Inf(</text>\n",
"<text text-anchor=\"start\" x=\"88\" y=\"-503.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">⓿</text>\n",
"<text text-anchor=\"start\" x=\"104\" y=\"-503.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">)&amp;Inf(</text>\n",
"<text text-anchor=\"start\" x=\"140\" y=\"-503.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#ff4da0\">❶</text>\n",
"<text text-anchor=\"start\" x=\"156\" y=\"-503.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">)</text>\n",
"<text text-anchor=\"start\" x=\"69\" y=\"-489.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">[gen. Büchi 2]</text>\n",
"<!-- I -->\n",
"<!-- 0 -->\n",
"<g id=\"node2\" class=\"node\">\n",
"<title>0</title>\n",
"<ellipse fill=\"#ffffaa\" stroke=\"#000000\" cx=\"115\" cy=\"-420\" rx=\"27\" ry=\"18\"/>\n",
"<text text-anchor=\"middle\" x=\"115\" y=\"-416.3\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">0</text>\n",
"<ellipse fill=\"#ffffaa\" stroke=\"#000000\" cx=\"115\" cy=\"-426\" rx=\"27\" ry=\"18\"/>\n",
"<text text-anchor=\"middle\" x=\"115\" y=\"-422.3\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">0</text>\n",
"</g>\n",
"<!-- I&#45;&gt;0 -->\n",
"<g id=\"edge1\" class=\"edge\">\n",
"<title>I&#45;&gt;0</title>\n",
"<path fill=\"none\" stroke=\"#000000\" d=\"M115,-474.8767C115,-471.822 115,-458.0552 115,-445.0759\"/>\n",
"<polygon fill=\"#000000\" stroke=\"#000000\" points=\"115,-438.0193 118.1501,-445.0192 115,-441.5193 115.0001,-445.0193 115.0001,-445.0193 115.0001,-445.0193 115,-441.5193 111.8501,-445.0193 115,-438.0193 115,-438.0193\"/>\n",
"<path fill=\"none\" stroke=\"#000000\" d=\"M115,-480.8767C115,-477.822 115,-464.0552 115,-451.0759\"/>\n",
"<polygon fill=\"#000000\" stroke=\"#000000\" points=\"115,-444.0193 118.1501,-451.0192 115,-447.5193 115.0001,-451.0193 115.0001,-451.0193 115.0001,-451.0193 115,-447.5193 111.8501,-451.0193 115,-444.0193 115,-444.0193\"/>\n",
"</g>\n",
"<!-- 1 -->\n",
"<g id=\"node3\" class=\"node\">\n",
"<title>1</title>\n",
"<ellipse fill=\"#ffffaa\" stroke=\"#000000\" cx=\"115\" cy=\"-320\" rx=\"27\" ry=\"18\"/>\n",
"<text text-anchor=\"start\" x=\"105\" y=\"-316.3\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">1,3</text>\n",
"<ellipse fill=\"#ffffaa\" stroke=\"#000000\" cx=\"115\" cy=\"-324\" rx=\"27\" ry=\"18\"/>\n",
"<text text-anchor=\"start\" x=\"105\" y=\"-320.3\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">1,3</text>\n",
"</g>\n",
"<!-- 0&#45;&gt;1 -->\n",
"<g id=\"edge2\" class=\"edge\">\n",
"<title>0&#45;&gt;1</title>\n",
"<path fill=\"none\" stroke=\"#000000\" d=\"M115,-401.6585C115,-385.8706 115,-362.929 115,-345.3797\"/>\n",
"<polygon fill=\"#000000\" stroke=\"#000000\" points=\"115,-338.2253 118.1501,-345.2252 115,-341.7253 115.0001,-345.2253 115.0001,-345.2253 115.0001,-345.2253 115,-341.7253 111.8501,-345.2253 115,-338.2253 115,-338.2253\"/>\n",
"<text text-anchor=\"start\" x=\"126.5\" y=\"-373.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">1</text>\n",
"<text text-anchor=\"start\" x=\"115\" y=\"-359.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">⓿</text>\n",
"<text text-anchor=\"start\" x=\"131\" y=\"-359.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#ff4da0\">❶</text>\n",
"<path fill=\"none\" stroke=\"#000000\" d=\"M115,-407.7644C115,-391.5192 115,-367.5825 115,-349.4527\"/>\n",
"<polygon fill=\"#000000\" stroke=\"#000000\" points=\"115,-342.0777 118.1501,-349.0776 115,-345.5777 115.0001,-349.0777 115.0001,-349.0777 115.0001,-349.0777 115,-345.5777 111.8501,-349.0777 115,-342.0777 115,-342.0777\"/>\n",
"<text text-anchor=\"start\" x=\"118.5\" y=\"-378.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">1</text>\n",
"<text text-anchor=\"start\" x=\"115\" y=\"-363.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">⓿</text>\n",
"</g>\n",
"<!-- 1&#45;&gt;1 -->\n",
"<g id=\"edge3\" class=\"edge\">\n",
"<title>1&#45;&gt;1</title>\n",
"<path fill=\"none\" stroke=\"#000000\" d=\"M138.6146,-329.1461C149.9731,-330.2753 160,-327.2266 160,-320 160,-314.3542 153.8801,-311.2585 145.7865,-310.7126\"/>\n",
"<polygon fill=\"#000000\" stroke=\"#000000\" points=\"138.6146,-310.8539 145.5512,-307.5666 142.1139,-310.7849 145.6132,-310.7159 145.6132,-310.7159 145.6132,-310.7159 142.1139,-310.7849 145.6753,-313.8653 138.6146,-310.8539 138.6146,-310.8539\"/>\n",
"<text text-anchor=\"start\" x=\"163.5\" y=\"-323.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">b</text>\n",
"<text text-anchor=\"start\" x=\"160\" y=\"-308.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">⓿</text>\n",
"<path fill=\"none\" stroke=\"#000000\" d=\"M138.6146,-333.1461C149.9731,-334.2753 160,-331.2266 160,-324 160,-318.3542 153.8801,-315.2585 145.7865,-314.7126\"/>\n",
"<polygon fill=\"#000000\" stroke=\"#000000\" points=\"138.6146,-314.8539 145.5512,-311.5666 142.1139,-314.7849 145.6132,-314.7159 145.6132,-314.7159 145.6132,-314.7159 142.1139,-314.7849 145.6753,-317.8653 138.6146,-314.8539 138.6146,-314.8539\"/>\n",
"<text text-anchor=\"start\" x=\"163.5\" y=\"-327.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">b</text>\n",
"<text text-anchor=\"start\" x=\"160\" y=\"-312.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">⓿</text>\n",
"</g>\n",
"<!-- 2 -->\n",
"<g id=\"node4\" class=\"node\">\n",
"<title>2</title>\n",
"<ellipse fill=\"#ffffaa\" stroke=\"#000000\" cx=\"27\" cy=\"-118\" rx=\"27\" ry=\"18\"/>\n",
"<text text-anchor=\"start\" x=\"17\" y=\"-114.3\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">1,4</text>\n",
"<ellipse fill=\"#ffffaa\" stroke=\"#000000\" cx=\"27\" cy=\"-120\" rx=\"27\" ry=\"18\"/>\n",
"<text text-anchor=\"start\" x=\"17\" y=\"-116.3\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">1,4</text>\n",
"</g>\n",
"<!-- 1&#45;&gt;2 -->\n",
"<g id=\"edge4\" class=\"edge\">\n",
"<title>1&#45;&gt;2</title>\n",
"<path fill=\"none\" stroke=\"#000000\" d=\"M97.59,-305.9683C80.0645,-290.7488 53.8424,-264.7467 41,-236 27.6548,-206.1278 25.4715,-167.9806 25.742,-143.2759\"/>\n",
"<polygon fill=\"#000000\" stroke=\"#000000\" points=\"25.8951,-136.0645 28.8957,-143.1298 25.8208,-139.5637 25.7464,-143.0629 25.7464,-143.0629 25.7464,-143.0629 25.8208,-139.5637 22.5971,-142.996 25.8951,-136.0645 25.8951,-136.0645\"/>\n",
"<text text-anchor=\"start\" x=\"41\" y=\"-221.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">a &amp; b</text>\n",
"<text text-anchor=\"start\" x=\"42\" y=\"-207.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">⓿</text>\n",
"<text text-anchor=\"start\" x=\"58\" y=\"-207.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#ff4da0\">❶</text>\n",
"<path fill=\"none\" stroke=\"#000000\" d=\"M97.5786,-309.9733C80.044,-294.758 53.8143,-268.7592 41,-240 27.403,-209.4843 25.306,-170.4884 25.6624,-145.3775\"/>\n",
"<polygon fill=\"#000000\" stroke=\"#000000\" points=\"25.831,-138.3686 28.8117,-145.4423 25.7468,-141.8676 25.6626,-145.3666 25.6626,-145.3666 25.6626,-145.3666 25.7468,-141.8676 22.5135,-145.2908 25.831,-138.3686 25.831,-138.3686\"/>\n",
"<text text-anchor=\"start\" x=\"41\" y=\"-225.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">a &amp; b</text>\n",
"<text text-anchor=\"start\" x=\"42\" y=\"-211.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">⓿</text>\n",
"<text text-anchor=\"start\" x=\"58\" y=\"-211.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#ff4da0\">❶</text>\n",
"</g>\n",
"<!-- 3 -->\n",
"<g id=\"node5\" class=\"node\">\n",
"<title>3</title>\n",
"<ellipse fill=\"#ffffaa\" stroke=\"#000000\" cx=\"115\" cy=\"-218\" rx=\"30.5947\" ry=\"18\"/>\n",
"<text text-anchor=\"start\" x=\"99.5\" y=\"-214.3\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">1,2,3</text>\n",
"<ellipse fill=\"#ffffaa\" stroke=\"#000000\" cx=\"115\" cy=\"-222\" rx=\"30.5947\" ry=\"18\"/>\n",
"<text text-anchor=\"start\" x=\"99.5\" y=\"-218.3\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">1,2,3</text>\n",
"</g>\n",
"<!-- 1&#45;&gt;3 -->\n",
"<g id=\"edge5\" class=\"edge\">\n",
"<title>1&#45;&gt;3</title>\n",
"<path fill=\"none\" stroke=\"#000000\" d=\"M105.0803,-302.978C102.2054,-297.1557 99.4518,-290.4746 98,-284 95.0826,-270.9898 95.0826,-267.0102 98,-254 98.9107,-249.9386 100.3336,-245.796 101.9774,-241.8351\"/>\n",
"<polygon fill=\"#000000\" stroke=\"#000000\" points=\"104.9008,-235.387 104.8792,-243.0631 103.4555,-238.5747 102.0103,-241.7624 102.0103,-241.7624 102.0103,-241.7624 103.4555,-238.5747 99.1414,-240.4617 104.9008,-235.387 104.9008,-235.387\"/>\n",
"<text text-anchor=\"start\" x=\"98\" y=\"-265.3\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">!b</text>\n",
"<path fill=\"none\" stroke=\"#000000\" d=\"M105.0803,-306.978C102.2054,-301.1557 99.4518,-294.4746 98,-288 95.0826,-274.9898 95.0826,-271.0102 98,-258 98.9107,-253.9386 100.3336,-249.796 101.9774,-245.8351\"/>\n",
"<polygon fill=\"#000000\" stroke=\"#000000\" points=\"104.9008,-239.387 104.8792,-247.0631 103.4555,-242.5747 102.0103,-245.7624 102.0103,-245.7624 102.0103,-245.7624 103.4555,-242.5747 99.1414,-244.4617 104.9008,-239.387 104.9008,-239.387\"/>\n",
"<text text-anchor=\"start\" x=\"98\" y=\"-269.3\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">!b</text>\n",
"</g>\n",
"<!-- 4 -->\n",
"<g id=\"node6\" class=\"node\">\n",
@ -2853,66 +2852,68 @@
"<!-- 1&#45;&gt;4 -->\n",
"<g id=\"edge6\" class=\"edge\">\n",
"<title>1&#45;&gt;4</title>\n",
"<path fill=\"none\" stroke=\"#000000\" d=\"M132.3877,-306.0906C149.76,-290.9709 175.3679,-265.0491 186,-236 196.6715,-206.8434 183.4964,-129.1265 173,-100 164.7809,-77.1929 148.5351,-54.8367 135.4831,-39.243\"/>\n",
"<polygon fill=\"#000000\" stroke=\"#000000\" points=\"130.8398,-33.8157 137.784,-37.0869 133.1151,-36.4752 135.3905,-39.1347 135.3905,-39.1347 135.3905,-39.1347 133.1151,-36.4752 132.9969,-41.1825 130.8398,-33.8157 130.8398,-33.8157\"/>\n",
"<text text-anchor=\"start\" x=\"188\" y=\"-164.3\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">a &amp; !b</text>\n",
"<path fill=\"none\" stroke=\"#000000\" d=\"M132.3877,-310.0906C149.76,-294.9709 175.3679,-269.0491 186,-240 196.7051,-210.7515 184.2203,-134.2183 173,-102 164.8436,-78.5795 148.4315,-55.526 135.3041,-39.5126\"/>\n",
"<polygon fill=\"#000000\" stroke=\"#000000\" points=\"130.6377,-33.9438 137.5481,-37.286 132.8857,-36.6265 135.1337,-39.3091 135.1337,-39.3091 135.1337,-39.3091 132.8857,-36.6265 132.7192,-41.3323 130.6377,-33.9438 130.6377,-33.9438\"/>\n",
"<text text-anchor=\"start\" x=\"189\" y=\"-174.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">a &amp; !b</text>\n",
"<text text-anchor=\"start\" x=\"199.5\" y=\"-159.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#ff4da0\">❶</text>\n",
"</g>\n",
"<!-- 2&#45;&gt;2 -->\n",
"<g id=\"edge7\" class=\"edge\">\n",
"<title>2&#45;&gt;2</title>\n",
"<path fill=\"none\" stroke=\"#000000\" d=\"M50.6146,-127.1461C61.9731,-128.2753 72,-125.2266 72,-118 72,-112.3542 65.8801,-109.2585 57.7865,-108.7126\"/>\n",
"<polygon fill=\"#000000\" stroke=\"#000000\" points=\"50.6146,-108.8539 57.5512,-105.5666 54.1139,-108.7849 57.6132,-108.7159 57.6132,-108.7159 57.6132,-108.7159 54.1139,-108.7849 57.6753,-111.8653 50.6146,-108.8539 50.6146,-108.8539\"/>\n",
"<text text-anchor=\"start\" x=\"72\" y=\"-121.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">a &amp; b</text>\n",
"<text text-anchor=\"start\" x=\"73\" y=\"-107.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">⓿</text>\n",
"<text text-anchor=\"start\" x=\"89\" y=\"-107.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#ff4da0\">❶</text>\n",
"<path fill=\"none\" stroke=\"#000000\" d=\"M50.6146,-129.1461C61.9731,-130.2753 72,-127.2266 72,-120 72,-114.3542 65.8801,-111.2585 57.7865,-110.7126\"/>\n",
"<polygon fill=\"#000000\" stroke=\"#000000\" points=\"50.6146,-110.8539 57.5512,-107.5666 54.1139,-110.7849 57.6132,-110.7159 57.6132,-110.7159 57.6132,-110.7159 54.1139,-110.7849 57.6753,-113.8653 50.6146,-110.8539 50.6146,-110.8539\"/>\n",
"<text text-anchor=\"start\" x=\"72\" y=\"-123.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">a &amp; b</text>\n",
"<text text-anchor=\"start\" x=\"73\" y=\"-109.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">⓿</text>\n",
"<text text-anchor=\"start\" x=\"89\" y=\"-109.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#ff4da0\">❶</text>\n",
"</g>\n",
"<!-- 2&#45;&gt;4 -->\n",
"<g id=\"edge8\" class=\"edge\">\n",
"<title>2&#45;&gt;4</title>\n",
"<path fill=\"none\" stroke=\"#000000\" d=\"M24.0726,-100.011C22.8274,-86.151 23.4336,-67.1893 33,-54 43.8935,-38.981 62.4057,-30.1574 79.1864,-25.0096\"/>\n",
"<polygon fill=\"#000000\" stroke=\"#000000\" points=\"86.2448,-23.021 80.3613,-27.9513 82.876,-23.9702 79.5071,-24.9193 79.5071,-24.9193 79.5071,-24.9193 82.876,-23.9702 78.6529,-21.8873 86.2448,-23.021 86.2448,-23.021\"/>\n",
"<text text-anchor=\"start\" x=\"33\" y=\"-64.3\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">a &amp; !b</text>\n",
"<path fill=\"none\" stroke=\"#000000\" d=\"M23.9747,-102.0388C22.5753,-87.7014 23.0216,-67.7983 33,-54 43.8723,-38.9657 62.3829,-30.1409 79.168,-24.9962\"/>\n",
"<polygon fill=\"#000000\" stroke=\"#000000\" points=\"86.2286,-23.0093 80.3437,-27.9378 82.8595,-23.9574 79.4903,-24.9056 79.4903,-24.9056 79.4903,-24.9056 82.8595,-23.9574 78.637,-21.8734 86.2286,-23.0093 86.2286,-23.0093\"/>\n",
"<text text-anchor=\"start\" x=\"33\" y=\"-72.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">a &amp; !b</text>\n",
"<text text-anchor=\"start\" x=\"43.5\" y=\"-57.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#ff4da0\">❶</text>\n",
"</g>\n",
"<!-- 3&#45;&gt;1 -->\n",
"<g id=\"edge9\" class=\"edge\">\n",
"<title>3&#45;&gt;1</title>\n",
"<path fill=\"none\" stroke=\"#000000\" d=\"M115,-236.0777C115,-252.2729 115,-276.2033 115,-294.3707\"/>\n",
"<polygon fill=\"#000000\" stroke=\"#000000\" points=\"115,-301.7644 111.8501,-294.7644 115,-298.2644 115.0001,-294.7644 115.0001,-294.7644 115.0001,-294.7644 115,-298.2644 118.1501,-294.7645 115,-301.7644 115,-301.7644\"/>\n",
"<text text-anchor=\"start\" x=\"118.5\" y=\"-272.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">b</text>\n",
"<text text-anchor=\"start\" x=\"115\" y=\"-257.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">⓿</text>\n",
"<path fill=\"none\" stroke=\"#000000\" d=\"M115,-240.0777C115,-256.2729 115,-280.2033 115,-298.3707\"/>\n",
"<polygon fill=\"#000000\" stroke=\"#000000\" points=\"115,-305.7644 111.8501,-298.7644 115,-302.2644 115.0001,-298.7644 115.0001,-298.7644 115.0001,-298.7644 115,-302.2644 118.1501,-298.7645 115,-305.7644 115,-305.7644\"/>\n",
"<text text-anchor=\"start\" x=\"118.5\" y=\"-276.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">b</text>\n",
"<text text-anchor=\"start\" x=\"115\" y=\"-261.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">⓿</text>\n",
"</g>\n",
"<!-- 3&#45;&gt;2 -->\n",
"<g id=\"edge10\" class=\"edge\">\n",
"<title>3&#45;&gt;2</title>\n",
"<path fill=\"none\" stroke=\"#000000\" d=\"M100.8613,-201.9333C85.891,-184.9216 62.1887,-157.9872 45.6862,-139.2343\"/>\n",
"<polygon fill=\"#000000\" stroke=\"#000000\" points=\"40.8135,-133.6972 47.8027,-136.8712 43.1257,-136.3247 45.4379,-138.9522 45.4379,-138.9522 45.4379,-138.9522 43.1257,-136.3247 43.0732,-141.0332 40.8135,-133.6972 40.8135,-133.6972\"/>\n",
"<text text-anchor=\"start\" x=\"82\" y=\"-171.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">a &amp; b</text>\n",
"<text text-anchor=\"start\" x=\"83\" y=\"-157.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">⓿</text>\n",
"<text text-anchor=\"start\" x=\"99\" y=\"-157.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#ff4da0\">❶</text>\n",
"<path fill=\"none\" stroke=\"#000000\" d=\"M100.8613,-205.6119C85.8029,-188.158 61.9096,-160.4634 45.3957,-141.3223\"/>\n",
"<polygon fill=\"#000000\" stroke=\"#000000\" points=\"40.5256,-135.6774 47.4833,-138.9198 42.8119,-138.3275 45.0983,-140.9775 45.0983,-140.9775 45.0983,-140.9775 42.8119,-138.3275 42.7132,-143.0352 40.5256,-135.6774 40.5256,-135.6774\"/>\n",
"<text text-anchor=\"start\" x=\"82\" y=\"-174.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">a &amp; b</text>\n",
"<text text-anchor=\"start\" x=\"83\" y=\"-160.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">⓿</text>\n",
"<text text-anchor=\"start\" x=\"99\" y=\"-160.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#ff4da0\">❶</text>\n",
"</g>\n",
"<!-- 3&#45;&gt;3 -->\n",
"<g id=\"edge11\" class=\"edge\">\n",
"<title>3&#45;&gt;3</title>\n",
"<path fill=\"none\" stroke=\"#000000\" d=\"M141.4663,-227.2285C153.3068,-228.1074 163.5473,-225.0313 163.5473,-218 163.5473,-212.4519 157.1714,-209.3663 148.6645,-208.7432\"/>\n",
"<polygon fill=\"#000000\" stroke=\"#000000\" points=\"141.4663,-208.7715 148.4539,-205.5939 144.9663,-208.7577 148.4663,-208.7439 148.4663,-208.7439 148.4663,-208.7439 144.9663,-208.7577 148.4787,-211.8939 141.4663,-208.7715 141.4663,-208.7715\"/>\n",
"<text text-anchor=\"start\" x=\"163.5473\" y=\"-214.3\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">!b</text>\n",
"<path fill=\"none\" stroke=\"#000000\" d=\"M141.4663,-231.2285C153.3068,-232.1074 163.5473,-229.0313 163.5473,-222 163.5473,-216.4519 157.1714,-213.3663 148.6645,-212.7432\"/>\n",
"<polygon fill=\"#000000\" stroke=\"#000000\" points=\"141.4663,-212.7715 148.4539,-209.5939 144.9663,-212.7577 148.4663,-212.7439 148.4663,-212.7439 148.4663,-212.7439 144.9663,-212.7577 148.4787,-215.8939 141.4663,-212.7715 141.4663,-212.7715\"/>\n",
"<text text-anchor=\"start\" x=\"163.5473\" y=\"-218.3\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">!b</text>\n",
"</g>\n",
"<!-- 3&#45;&gt;4 -->\n",
"<g id=\"edge12\" class=\"edge\">\n",
"<title>3&#45;&gt;4</title>\n",
"<path fill=\"none\" stroke=\"#000000\" d=\"M119.2931,-199.682C125.7911,-169.2518 136.5096,-106.4385 128,-54 127.38,-50.1795 126.4126,-46.2165 125.2899,-42.3777\"/>\n",
"<path fill=\"none\" stroke=\"#000000\" d=\"M119.2339,-203.7334C125.7871,-172.7507 136.7627,-107.9983 128,-54 127.38,-50.1795 126.4126,-46.2165 125.2899,-42.3777\"/>\n",
"<polygon fill=\"#000000\" stroke=\"#000000\" points=\"123.1427,-35.6595 128.2743,-41.3683 124.2082,-38.9934 125.2738,-42.3273 125.2738,-42.3273 125.2738,-42.3273 124.2082,-38.9934 122.2733,-43.2863 123.1427,-35.6595 123.1427,-35.6595\"/>\n",
"<text text-anchor=\"start\" x=\"132\" y=\"-121.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">a &amp; !b</text>\n",
"<text text-anchor=\"start\" x=\"142.5\" y=\"-106.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#ff4da0\">❶</text>\n",
"<text text-anchor=\"start\" x=\"132\" y=\"-123.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">a &amp; !b</text>\n",
"<text text-anchor=\"start\" x=\"142.5\" y=\"-108.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#ff4da0\">❶</text>\n",
"</g>\n",
"<!-- 4&#45;&gt;2 -->\n",
"<g id=\"edge13\" class=\"edge\">\n",
"<title>4&#45;&gt;2</title>\n",
"<path fill=\"none\" stroke=\"#000000\" d=\"M105.5283,-34.9116C96.8241,-48.3469 83.6886,-67.2617 70,-82 64.0989,-88.3536 57.0993,-94.6436 50.4798,-100.1453\"/>\n",
"<polygon fill=\"#000000\" stroke=\"#000000\" points=\"45.0413,-104.5653 48.4868,-97.7059 47.7574,-102.3579 50.4735,-100.1504 50.4735,-100.1504 50.4735,-100.1504 47.7574,-102.3579 52.4602,-102.5949 45.0413,-104.5653 45.0413,-104.5653\"/>\n",
"<text text-anchor=\"start\" x=\"92\" y=\"-71.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">a &amp; b</text>\n",
"<text text-anchor=\"start\" x=\"93\" y=\"-57.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">⓿</text>\n",
"<text text-anchor=\"start\" x=\"109\" y=\"-57.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#ff4da0\">❶</text>\n",
"<path fill=\"none\" stroke=\"#000000\" d=\"M105.7988,-35.1873C97.1507,-49.0758 83.9569,-68.7524 70,-84 64.1452,-90.3963 57.1597,-96.6992 50.5388,-102.1997\"/>\n",
"<polygon fill=\"#000000\" stroke=\"#000000\" points=\"45.0959,-106.6157 48.5471,-99.7592 47.8139,-104.4105 50.5318,-102.2053 50.5318,-102.2053 50.5318,-102.2053 47.8139,-104.4105 52.5165,-104.6515 45.0959,-106.6157 45.0959,-106.6157\"/>\n",
"<text text-anchor=\"start\" x=\"94\" y=\"-72.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">a &amp; b</text>\n",
"<text text-anchor=\"start\" x=\"95\" y=\"-58.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">⓿</text>\n",
"<text text-anchor=\"start\" x=\"111\" y=\"-58.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#ff4da0\">❶</text>\n",
"</g>\n",
"<!-- 4&#45;&gt;4 -->\n",
"<g id=\"edge14\" class=\"edge\">\n",
@ -3603,6 +3604,544 @@
"nba2, nba3, nba4, nba5 = [spot.scc_filter(spot.remove_alternation(a, True), True) for a in (aut2, aut3, aut4, aut5)]\n",
"display_inline(nba2, nba3, nba4, nba5)"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"The following demonstrate that very weak (non-alternating) Büchi automata can be complemented via alternation removal."
]
},
{
"cell_type": "code",
"execution_count": 9,
"metadata": {},
"outputs": [
{
"data": {
"text/html": [
"<div style='vertical-align:text-top;display:inline-block;'><?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n",
"<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n",
" \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n",
"<!-- Generated by graphviz version 2.40.1 (20161225.0304)\n",
" -->\n",
"<!-- Title: (a &amp; (Fa R XFb)) | (!a &amp; (G!a U\\nXG!b)) Pages: 1 -->\n",
"<svg width=\"309pt\" height=\"327pt\"\n",
" viewBox=\"0.00 0.00 308.74 327.48\" 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 323.4802)\">\n",
"<title>(a &amp; (Fa R XFb)) | (!a &amp; (G!a U\\nXG!b))</title>\n",
"<polygon fill=\"#ffffff\" stroke=\"transparent\" points=\"-4,4 -4,-323.4802 304.7401,-323.4802 304.7401,4 -4,4\"/>\n",
"<text text-anchor=\"start\" x=\"129.3701\" y=\"-305.2802\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">Inf(</text>\n",
"<text text-anchor=\"start\" x=\"151.3701\" y=\"-305.2802\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">⓿</text>\n",
"<text text-anchor=\"start\" x=\"167.3701\" y=\"-305.2802\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">)</text>\n",
"<text text-anchor=\"start\" x=\"127.3701\" y=\"-291.2802\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">[Büchi]</text>\n",
"<!-- I -->\n",
"<!-- 0 -->\n",
"<g id=\"node2\" class=\"node\">\n",
"<title>0</title>\n",
"<ellipse fill=\"#ffffaa\" stroke=\"#000000\" cx=\"120.8701\" cy=\"-227.4802\" rx=\"18\" ry=\"18\"/>\n",
"<text text-anchor=\"middle\" x=\"120.8701\" y=\"-223.7802\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">0</text>\n",
"</g>\n",
"<!-- I&#45;&gt;0 -->\n",
"<g id=\"edge1\" class=\"edge\">\n",
"<title>I&#45;&gt;0</title>\n",
"<path fill=\"none\" stroke=\"#000000\" d=\"M120.8701,-282.3569C120.8701,-279.3023 120.8701,-265.5354 120.8701,-252.5561\"/>\n",
"<polygon fill=\"#000000\" stroke=\"#000000\" points=\"120.8701,-245.4995 124.0202,-252.4994 120.8701,-248.9995 120.8702,-252.4995 120.8702,-252.4995 120.8702,-252.4995 120.8701,-248.9995 117.7202,-252.4995 120.8701,-245.4995 120.8701,-245.4995\"/>\n",
"</g>\n",
"<!-- 1 -->\n",
"<g id=\"node3\" class=\"node\">\n",
"<title>1</title>\n",
"<ellipse fill=\"#ffffaa\" stroke=\"#000000\" cx=\"26.8701\" cy=\"-131.6102\" rx=\"18\" ry=\"18\"/>\n",
"<text text-anchor=\"middle\" x=\"26.8701\" y=\"-127.9102\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">1</text>\n",
"</g>\n",
"<!-- 0&#45;&gt;1 -->\n",
"<g id=\"edge2\" class=\"edge\">\n",
"<title>0&#45;&gt;1</title>\n",
"<path fill=\"none\" stroke=\"#000000\" d=\"M108.1928,-214.5508C91.794,-197.8258 63.1379,-168.5995 44.5911,-149.6838\"/>\n",
"<polygon fill=\"#000000\" stroke=\"#000000\" points=\"39.6467,-144.641 46.7967,-147.4339 42.0971,-147.1401 44.5475,-149.6393 44.5475,-149.6393 44.5475,-149.6393 42.0971,-147.1401 42.2982,-151.8446 39.6467,-144.641 39.6467,-144.641\"/>\n",
"<text text-anchor=\"start\" x=\"85.8701\" y=\"-180.2802\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">a</text>\n",
"</g>\n",
"<!-- 2 -->\n",
"<g id=\"node4\" class=\"node\">\n",
"<title>2</title>\n",
"<ellipse fill=\"#ffffaa\" stroke=\"#000000\" cx=\"120.8701\" cy=\"-131.6102\" rx=\"26.7407\" ry=\"26.7407\"/>\n",
"<text text-anchor=\"start\" x=\"116.3701\" y=\"-135.4102\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">2</text>\n",
"<text text-anchor=\"start\" x=\"112.8701\" y=\"-120.4102\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">⓿</text>\n",
"</g>\n",
"<!-- 0&#45;&gt;2 -->\n",
"<g id=\"edge3\" class=\"edge\">\n",
"<title>0&#45;&gt;2</title>\n",
"<path fill=\"none\" stroke=\"#000000\" d=\"M120.8701,-209.4478C120.8701,-197.142 120.8701,-180.4584 120.8701,-165.6931\"/>\n",
"<polygon fill=\"#000000\" stroke=\"#000000\" points=\"120.8701,-158.6264 124.0202,-165.6263 120.8701,-162.1264 120.8702,-165.6264 120.8702,-165.6264 120.8702,-165.6264 120.8701,-162.1264 117.7202,-165.6264 120.8701,-158.6264 120.8701,-158.6264\"/>\n",
"<text text-anchor=\"start\" x=\"120.8701\" y=\"-180.2802\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">!a</text>\n",
"</g>\n",
"<!-- 3 -->\n",
"<g id=\"node5\" class=\"node\">\n",
"<title>3</title>\n",
"<ellipse fill=\"#ffffaa\" stroke=\"#000000\" cx=\"214.8701\" cy=\"-131.6102\" rx=\"18\" ry=\"18\"/>\n",
"<text text-anchor=\"middle\" x=\"214.8701\" y=\"-127.9102\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">3</text>\n",
"</g>\n",
"<!-- 0&#45;&gt;3 -->\n",
"<g id=\"edge4\" class=\"edge\">\n",
"<title>0&#45;&gt;3</title>\n",
"<path fill=\"none\" stroke=\"#000000\" d=\"M133.5473,-214.5508C149.9461,-197.8258 178.6022,-168.5995 197.149,-149.6838\"/>\n",
"<polygon fill=\"#000000\" stroke=\"#000000\" points=\"202.0934,-144.641 199.4419,-151.8446 199.643,-147.1401 197.1927,-149.6393 197.1927,-149.6393 197.1927,-149.6393 199.643,-147.1401 194.9434,-147.4339 202.0934,-144.641 202.0934,-144.641\"/>\n",
"<text text-anchor=\"start\" x=\"170.8701\" y=\"-180.2802\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">!a</text>\n",
"</g>\n",
"<!-- 1&#45;&gt;1 -->\n",
"<g id=\"edge5\" class=\"edge\">\n",
"<title>1&#45;&gt;1</title>\n",
"<path fill=\"none\" stroke=\"#000000\" d=\"M42.7861,-140.5889C53.0204,-142.9312 62.8701,-139.9383 62.8701,-131.6102 62.8701,-125.234 57.0964,-121.9851 49.7969,-121.8637\"/>\n",
"<polygon fill=\"#000000\" stroke=\"#000000\" points=\"42.7861,-122.6314 49.4016,-118.7381 46.2653,-122.2504 49.7445,-121.8694 49.7445,-121.8694 49.7445,-121.8694 46.2653,-122.2504 50.0874,-125.0006 42.7861,-122.6314 42.7861,-122.6314\"/>\n",
"<text text-anchor=\"start\" x=\"62.8701\" y=\"-127.9102\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">!b</text>\n",
"</g>\n",
"<!-- 4 -->\n",
"<g id=\"node6\" class=\"node\">\n",
"<title>4</title>\n",
"<ellipse fill=\"#ffffaa\" stroke=\"#000000\" cx=\"26.8701\" cy=\"-26.8701\" rx=\"26.7407\" ry=\"26.7407\"/>\n",
"<text text-anchor=\"start\" x=\"22.3701\" y=\"-30.6701\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">4</text>\n",
"<text text-anchor=\"start\" x=\"18.8701\" y=\"-15.6701\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">⓿</text>\n",
"</g>\n",
"<!-- 1&#45;&gt;4 -->\n",
"<g id=\"edge6\" class=\"edge\">\n",
"<title>1&#45;&gt;4</title>\n",
"<path fill=\"none\" stroke=\"#000000\" d=\"M26.8701,-113.3658C26.8701,-99.0062 26.8701,-78.5836 26.8701,-61.1885\"/>\n",
"<polygon fill=\"#000000\" stroke=\"#000000\" points=\"26.8701,-53.9454 30.0202,-60.9453 26.8701,-57.4454 26.8702,-60.9454 26.8702,-60.9454 26.8702,-60.9454 26.8701,-57.4454 23.7202,-60.9454 26.8701,-53.9454 26.8701,-53.9454\"/>\n",
"<text text-anchor=\"start\" x=\"26.8701\" y=\"-75.5401\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">b</text>\n",
"</g>\n",
"<!-- 2&#45;&gt;2 -->\n",
"<g id=\"edge7\" class=\"edge\">\n",
"<title>2&#45;&gt;2</title>\n",
"<path fill=\"none\" stroke=\"#000000\" d=\"M146.2401,-141.2745C156.7939,-141.941 165.7401,-138.7195 165.7401,-131.6102 165.7401,-126.1671 160.496,-123.003 153.3013,-122.1179\"/>\n",
"<polygon fill=\"#000000\" stroke=\"#000000\" points=\"146.2401,-121.9459 153.3148,-118.9674 149.739,-122.0312 153.238,-122.1165 153.238,-122.1165 153.238,-122.1165 149.739,-122.0312 153.1612,-125.2656 146.2401,-121.9459 146.2401,-121.9459\"/>\n",
"<text text-anchor=\"start\" x=\"165.7401\" y=\"-127.9102\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">!b</text>\n",
"</g>\n",
"<!-- 3&#45;&gt;3 -->\n",
"<g id=\"edge8\" class=\"edge\">\n",
"<title>3&#45;&gt;3</title>\n",
"<path fill=\"none\" stroke=\"#000000\" d=\"M230.7861,-140.5889C241.0204,-142.9312 250.8701,-139.9383 250.8701,-131.6102 250.8701,-125.234 245.0964,-121.9851 237.7969,-121.8637\"/>\n",
"<polygon fill=\"#000000\" stroke=\"#000000\" points=\"230.7861,-122.6314 237.4016,-118.7381 234.2653,-122.2504 237.7445,-121.8694 237.7445,-121.8694 237.7445,-121.8694 234.2653,-122.2504 238.0874,-125.0006 230.7861,-122.6314 230.7861,-122.6314\"/>\n",
"<text text-anchor=\"start\" x=\"250.8701\" y=\"-127.9102\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">!a</text>\n",
"</g>\n",
"<!-- 5 -->\n",
"<g id=\"node7\" class=\"node\">\n",
"<title>5</title>\n",
"<ellipse fill=\"#ffffaa\" stroke=\"#000000\" cx=\"214.8701\" cy=\"-26.8701\" rx=\"26.7407\" ry=\"26.7407\"/>\n",
"<text text-anchor=\"start\" x=\"210.3701\" y=\"-30.6701\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">5</text>\n",
"<text text-anchor=\"start\" x=\"206.8701\" y=\"-15.6701\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">⓿</text>\n",
"</g>\n",
"<!-- 3&#45;&gt;5 -->\n",
"<g id=\"edge9\" class=\"edge\">\n",
"<title>3&#45;&gt;5</title>\n",
"<path fill=\"none\" stroke=\"#000000\" d=\"M214.8701,-113.3658C214.8701,-99.0062 214.8701,-78.5836 214.8701,-61.1885\"/>\n",
"<polygon fill=\"#000000\" stroke=\"#000000\" points=\"214.8701,-53.9454 218.0202,-60.9453 214.8701,-57.4454 214.8702,-60.9454 214.8702,-60.9454 214.8702,-60.9454 214.8701,-57.4454 211.7202,-60.9454 214.8701,-53.9454 214.8701,-53.9454\"/>\n",
"<text text-anchor=\"start\" x=\"214.8701\" y=\"-75.5401\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">!a</text>\n",
"</g>\n",
"<!-- 4&#45;&gt;4 -->\n",
"<g id=\"edge10\" class=\"edge\">\n",
"<title>4&#45;&gt;4</title>\n",
"<path fill=\"none\" stroke=\"#000000\" d=\"M52.2401,-36.5344C62.7939,-37.2009 71.7401,-33.9794 71.7401,-26.8701 71.7401,-21.4269 66.496,-18.2629 59.3013,-17.3778\"/>\n",
"<polygon fill=\"#000000\" stroke=\"#000000\" points=\"52.2401,-17.2058 59.3148,-14.2273 55.739,-17.2911 59.238,-17.3764 59.238,-17.3764 59.238,-17.3764 55.739,-17.2911 59.1612,-20.5254 52.2401,-17.2058 52.2401,-17.2058\"/>\n",
"<text text-anchor=\"middle\" x=\"76.2401\" y=\"-23.1701\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">1</text>\n",
"</g>\n",
"<!-- 5&#45;&gt;5 -->\n",
"<g id=\"edge11\" class=\"edge\">\n",
"<title>5&#45;&gt;5</title>\n",
"<path fill=\"none\" stroke=\"#000000\" d=\"M240.2401,-36.5344C250.7939,-37.2009 259.7401,-33.9794 259.7401,-26.8701 259.7401,-21.4269 254.496,-18.2629 247.3013,-17.3778\"/>\n",
"<polygon fill=\"#000000\" stroke=\"#000000\" points=\"240.2401,-17.2058 247.3148,-14.2273 243.739,-17.2911 247.238,-17.3764 247.238,-17.3764 247.238,-17.3764 243.739,-17.2911 247.1612,-20.5254 240.2401,-17.2058 240.2401,-17.2058\"/>\n",
"<text text-anchor=\"start\" x=\"259.7401\" y=\"-23.1701\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">!a &amp; !b</text>\n",
"</g>\n",
"</g>\n",
"</svg>\n",
"</div><div style='vertical-align:text-top;display:inline-block;'><svg height=\"360pt\" viewBox=\"0.00 0.00 170.02 360.00\" width=\"170pt\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
"<g class=\"graph\" id=\"graph0\" transform=\"scale(.7301 .7301) rotate(0) translate(4 489.0802)\">\n",
"<polygon fill=\"#ffffff\" points=\"-4,4 -4,-489.0802 228.8701,-489.0802 228.8701,4 -4,4\" stroke=\"transparent\"/>\n",
"<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"89.935\" y=\"-470.8802\">Fin(</text>\n",
"<text fill=\"#1f78b4\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"114.935\" y=\"-470.8802\">⓿</text>\n",
"<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"130.935\" y=\"-470.8802\">)</text>\n",
"<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"79.935\" y=\"-456.8802\">[co-Büchi]</text>\n",
"<!-- I -->\n",
"<!-- 0 -->\n",
"<g class=\"node\" id=\"node2\">\n",
"<title>0</title>\n",
"<ellipse cx=\"52\" cy=\"-393.0802\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"#000000\"/>\n",
"<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"52\" y=\"-389.3802\">0</text>\n",
"</g>\n",
"<!-- I&#45;&gt;0 -->\n",
"<g class=\"edge\" id=\"edge1\">\n",
"<title>I-&gt;0</title>\n",
"<path d=\"M52,-447.9569C52,-444.9023 52,-431.1354 52,-418.1561\" fill=\"none\" stroke=\"#000000\"/>\n",
"<polygon fill=\"#000000\" points=\"52,-411.0995 55.1501,-418.0994 52,-414.5995 52.0001,-418.0995 52.0001,-418.0995 52.0001,-418.0995 52,-414.5995 48.8501,-418.0995 52,-411.0995 52,-411.0995\" stroke=\"#000000\"/>\n",
"</g>\n",
"<!-- 1 -->\n",
"<g class=\"node\" id=\"node3\">\n",
"<title>1</title>\n",
"<ellipse cx=\"18\" cy=\"-306.0802\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"#000000\"/>\n",
"<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"18\" y=\"-302.3802\">1</text>\n",
"</g>\n",
"<!-- 0&#45;&gt;1 -->\n",
"<g class=\"edge\" id=\"edge2\">\n",
"<title>0-&gt;1</title>\n",
"<path d=\"M45.4445,-376.3058C40.3036,-363.1513 33.0824,-344.6733 27.3375,-329.9732\" fill=\"none\" stroke=\"#000000\"/>\n",
"<polygon fill=\"#000000\" points=\"24.6514,-323.1001 30.1334,-328.4733 25.9254,-326.36 27.1995,-329.6199 27.1995,-329.6199 27.1995,-329.6199 25.9254,-326.36 24.2655,-330.7665 24.6514,-323.1001 24.6514,-323.1001\" stroke=\"#000000\"/>\n",
"<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"38\" y=\"-345.8802\">a</text>\n",
"</g>\n",
"<!-- &#45;1 -->\n",
"<g class=\"node\" id=\"node4\">\n",
"<title>-1</title>\n",
"<ellipse cx=\"87\" cy=\"-306.0802\" fill=\"#ffffaa\" rx=\"1.8\" ry=\"1.8\" stroke=\"#000000\"/>\n",
"</g>\n",
"<!-- 0&#45;&gt;&#45;1 -->\n",
"<g class=\"edge\" id=\"edge3\">\n",
"<title>0-&gt;-1</title>\n",
"<path d=\"M58.7484,-376.3058C66.1181,-357.9868 77.6412,-329.3435 83.429,-314.9566\" fill=\"none\" stroke=\"#000000\"/>\n",
"<polygon fill=\"none\" points=\"85.8635,-315.4694 86.2032,-308.0608 81.3176,-313.6406 85.8635,-315.4694\" stroke=\"#000000\"/>\n",
"<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"72\" y=\"-345.8802\">!a</text>\n",
"</g>\n",
"<!-- 1&#45;&gt;1 -->\n",
"<g class=\"edge\" id=\"edge6\">\n",
"<title>1-&gt;1</title>\n",
"<path d=\"M35.0373,-312.4594C44.8579,-313.7613 54,-311.6349 54,-306.0802 54,-301.9142 48.8576,-299.6766 42.1433,-299.3674\" fill=\"none\" stroke=\"#000000\"/>\n",
"<polygon fill=\"#000000\" points=\"35.0373,-299.701 41.8818,-296.2261 38.5335,-299.5368 42.0296,-299.3727 42.0296,-299.3727 42.0296,-299.3727 38.5335,-299.5368 42.1774,-302.5192 35.0373,-299.701 35.0373,-299.701\" stroke=\"#000000\"/>\n",
"<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"54\" y=\"-302.3802\">!b</text>\n",
"</g>\n",
"<!-- 2 -->\n",
"<g class=\"node\" id=\"node5\">\n",
"<title>2</title>\n",
"<ellipse cx=\"32\" cy=\"-224.2102\" fill=\"#ffffaa\" rx=\"26.7407\" ry=\"26.7407\" stroke=\"#000000\"/>\n",
"<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"27.5\" y=\"-228.0102\">2</text>\n",
"<text fill=\"#1f78b4\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"24\" y=\"-213.0102\">⓿</text>\n",
"</g>\n",
"<!-- &#45;1&#45;&gt;2 -->\n",
"<g class=\"edge\" id=\"edge4\">\n",
"<title>-1-&gt;2</title>\n",
"<path d=\"M85.9993,-304.3735C84.1022,-301.154 79.8293,-293.9777 76,-288.0802 68.2661,-276.1694 59.4365,-263.2319 51.7267,-252.1353\" fill=\"none\" stroke=\"#000000\"/>\n",
"<polygon fill=\"#000000\" points=\"47.5727,-246.1782 54.1605,-250.1183 49.5747,-249.0491 51.5766,-251.9201 51.5766,-251.9201 51.5766,-251.9201 49.5747,-249.0491 48.9927,-253.7218 47.5727,-246.1782 47.5727,-246.1782\" stroke=\"#000000\"/>\n",
"</g>\n",
"<!-- 3 -->\n",
"<g class=\"node\" id=\"node6\">\n",
"<title>3</title>\n",
"<ellipse cx=\"126\" cy=\"-224.2102\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"#000000\"/>\n",
"<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"126\" y=\"-220.5102\">3</text>\n",
"</g>\n",
"<!-- &#45;1&#45;&gt;3 -->\n",
"<g class=\"edge\" id=\"edge5\">\n",
"<title>-1-&gt;3</title>\n",
"<path d=\"M87.8146,-304.3703C91.2692,-297.1182 104.991,-268.3129 114.9992,-247.3034\" fill=\"none\" stroke=\"#000000\"/>\n",
"<polygon fill=\"#000000\" points=\"118.1004,-240.7932 117.9338,-248.4675 116.5952,-243.953 115.0899,-247.1128 115.0899,-247.1128 115.0899,-247.1128 116.5952,-243.953 112.2461,-245.7581 118.1004,-240.7932 118.1004,-240.7932\" stroke=\"#000000\"/>\n",
"</g>\n",
"<!-- 2&#45;&gt;2 -->\n",
"<g class=\"edge\" id=\"edge7\">\n",
"<title>2-&gt;2</title>\n",
"<path d=\"M57.8213,-232.4098C68.1776,-232.8731 76.8701,-230.1399 76.8701,-224.2102 76.8701,-219.7629 71.9805,-217.1137 65.1667,-216.2624\" fill=\"none\" stroke=\"#000000\"/>\n",
"<polygon fill=\"#000000\" points=\"57.8213,-216.0105 64.9252,-213.1024 61.3193,-216.1305 64.8172,-216.2505 64.8172,-216.2505 64.8172,-216.2505 61.3193,-216.1305 64.7092,-219.3987 57.8213,-216.0105 57.8213,-216.0105\" stroke=\"#000000\"/>\n",
"<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"76.8701\" y=\"-220.5102\">!b</text>\n",
"</g>\n",
"<!-- T5T2 -->\n",
"<!-- 2&#45;&gt;T5T2 -->\n",
"<g class=\"edge\" id=\"edge8\">\n",
"<title>2-&gt;T5T2</title>\n",
"<path d=\"M32,-197.2375C32,-181.528 32,-162.8287 32,-152.4613\" fill=\"none\" stroke=\"#000000\"/>\n",
"<polygon fill=\"#000000\" points=\"32,-145.2905 35.1501,-152.2904 32,-148.7905 32.0001,-152.2905 32.0001,-152.2905 32.0001,-152.2905 32,-148.7905 28.8501,-152.2905 32,-145.2905 32,-145.2905\" stroke=\"#000000\"/>\n",
"<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"32\" y=\"-168.1401\">b</text>\n",
"</g>\n",
"<!-- T5T3 -->\n",
"<!-- 3&#45;&gt;T5T3 -->\n",
"<g class=\"edge\" id=\"edge9\">\n",
"<title>3-&gt;T5T3</title>\n",
"<path d=\"M119.6378,-207.3142C113.1685,-190.1341 103.4477,-164.3187 98.7438,-151.8268\" fill=\"none\" stroke=\"#000000\"/>\n",
"<polygon fill=\"#000000\" points=\"96.2616,-145.2349 101.6764,-150.6758 97.4951,-148.5104 98.7285,-151.7859 98.7285,-151.7859 98.7285,-151.7859 97.4951,-148.5104 95.7805,-152.896 96.2616,-145.2349 96.2616,-145.2349\" stroke=\"#000000\"/>\n",
"<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"109\" y=\"-168.1401\">a</text>\n",
"</g>\n",
"<!-- &#45;4 -->\n",
"<g class=\"node\" id=\"node9\">\n",
"<title>-4</title>\n",
"<ellipse cx=\"139\" cy=\"-144.5401\" fill=\"#ffffaa\" rx=\"1.8\" ry=\"1.8\" stroke=\"#000000\"/>\n",
"</g>\n",
"<!-- 3&#45;&gt;&#45;4 -->\n",
"<g class=\"edge\" id=\"edge10\">\n",
"<title>3-&gt;-4</title>\n",
"<path d=\"M123.889,-206.2978C123.0446,-194.2084 123.0535,-178.0243 127,-164.3401 128.2698,-159.9373 130.7883,-155.5293 133.1916,-151.9939\" fill=\"none\" stroke=\"#000000\"/>\n",
"<polygon fill=\"none\" points=\"135.269,-153.3081 137.526,-146.2435 131.3561,-150.3587 135.269,-153.3081\" stroke=\"#000000\"/>\n",
"<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"127\" y=\"-168.1401\">!a</text>\n",
"</g>\n",
"<!-- &#45;4&#45;&gt;3 -->\n",
"<g class=\"edge\" id=\"edge11\">\n",
"<title>-4-&gt;3</title>\n",
"<path d=\"M139.0993,-146.4396C139.3415,-151.7017 139.8169,-166.9002 138,-179.3401 137.0073,-186.1373 135.3464,-193.3793 133.5721,-200.0174\" fill=\"none\" stroke=\"#000000\"/>\n",
"<polygon fill=\"#000000\" points=\"131.6284,-206.9338 130.4898,-199.3426 132.5754,-203.5644 133.5223,-200.1949 133.5223,-200.1949 133.5223,-200.1949 132.5754,-203.5644 136.5548,-201.0471 131.6284,-206.9338 131.6284,-206.9338\" stroke=\"#000000\"/>\n",
"</g>\n",
"<!-- 4 -->\n",
"<g class=\"node\" id=\"node10\">\n",
"<title>4</title>\n",
"<ellipse cx=\"139\" cy=\"-78.8701\" fill=\"#ffffaa\" rx=\"26.7407\" ry=\"26.7407\" stroke=\"#000000\"/>\n",
"<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"134.5\" y=\"-82.6701\">4</text>\n",
"<text fill=\"#1f78b4\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"131\" y=\"-67.6701\">⓿</text>\n",
"</g>\n",
"<!-- &#45;4&#45;&gt;4 -->\n",
"<g class=\"edge\" id=\"edge12\">\n",
"<title>-4-&gt;4</title>\n",
"<path d=\"M139,-142.6456C139,-138.0748 139,-125.8923 139,-113.3841\" fill=\"none\" stroke=\"#000000\"/>\n",
"<polygon fill=\"#000000\" points=\"139,-106.0368 142.1501,-113.0368 139,-109.5368 139.0001,-113.0368 139.0001,-113.0368 139.0001,-113.0368 139,-109.5368 135.8501,-113.0369 139,-106.0368 139,-106.0368\" stroke=\"#000000\"/>\n",
"</g>\n",
"<!-- 4&#45;&gt;4 -->\n",
"<g class=\"edge\" id=\"edge13\">\n",
"<title>4-&gt;4</title>\n",
"<path d=\"M164.8213,-87.0697C175.1776,-87.533 183.8701,-84.7997 183.8701,-78.8701 183.8701,-74.4228 178.9805,-71.7735 172.1667,-70.9223\" fill=\"none\" stroke=\"#000000\"/>\n",
"<polygon fill=\"#000000\" points=\"164.8213,-70.6704 171.9252,-67.7623 168.3193,-70.7904 171.8172,-70.9104 171.8172,-70.9104 171.8172,-70.9104 168.3193,-70.7904 171.7092,-74.0586 164.8213,-70.6704 164.8213,-70.6704\" stroke=\"#000000\"/>\n",
"<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"183.8701\" y=\"-75.1701\">!a &amp; !b</text>\n",
"</g>\n",
"<!-- T5T4 -->\n",
"<!-- 4&#45;&gt;T5T4 -->\n",
"<g class=\"edge\" id=\"edge14\">\n",
"<title>4-&gt;T5T4</title>\n",
"<path d=\"M139,-51.8995C139,-36.6517 139,-18.6623 139,-8.5175\" fill=\"none\" stroke=\"#000000\"/>\n",
"<polygon fill=\"#000000\" points=\"139,-1.2289 142.1501,-8.2288 139,-4.7289 139.0001,-8.2289 139.0001,-8.2289 139.0001,-8.2289 139,-4.7289 135.8501,-8.2289 139,-1.2289 139,-1.2289\" stroke=\"#000000\"/>\n",
"<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"139\" y=\"-22.8\">a | b</text>\n",
"</g>\n",
"</g>\n",
"</svg></div><div style='vertical-align:text-top;display:inline-block;'><?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n",
"<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n",
" \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n",
"<!-- Generated by graphviz version 2.40.1 (20161225.0304)\n",
" -->\n",
"<!-- Pages: 1 -->\n",
"<svg width=\"280pt\" height=\"360pt\"\n",
" viewBox=\"0.00 0.00 280.08 360.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
"<g id=\"graph0\" class=\"graph\" transform=\"scale(.7073 .7073) rotate(0) translate(4 505)\">\n",
"<polygon fill=\"#ffffff\" stroke=\"transparent\" points=\"-4,4 -4,-505 392,-505 392,4 -4,4\"/>\n",
"<text text-anchor=\"start\" x=\"147\" y=\"-486.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">Inf(</text>\n",
"<text text-anchor=\"start\" x=\"169\" y=\"-486.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">⓿</text>\n",
"<text text-anchor=\"start\" x=\"185\" y=\"-486.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">)&amp;Inf(</text>\n",
"<text text-anchor=\"start\" x=\"221\" y=\"-486.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#ff4da0\">❶</text>\n",
"<text text-anchor=\"start\" x=\"237\" y=\"-486.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">)</text>\n",
"<text text-anchor=\"start\" x=\"150\" y=\"-472.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">[gen. Büchi 2]</text>\n",
"<!-- I -->\n",
"<!-- 0 -->\n",
"<g id=\"node2\" class=\"node\">\n",
"<title>0</title>\n",
"<ellipse fill=\"#ffffaa\" stroke=\"#000000\" cx=\"69\" cy=\"-409\" rx=\"18\" ry=\"18\"/>\n",
"<text text-anchor=\"middle\" x=\"69\" y=\"-405.3\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">0</text>\n",
"</g>\n",
"<!-- I&#45;&gt;0 -->\n",
"<g id=\"edge1\" class=\"edge\">\n",
"<title>I&#45;&gt;0</title>\n",
"<path fill=\"none\" stroke=\"#000000\" d=\"M69,-463.8767C69,-460.822 69,-447.0552 69,-434.0759\"/>\n",
"<polygon fill=\"#000000\" stroke=\"#000000\" points=\"69,-427.0193 72.1501,-434.0192 69,-430.5193 69.0001,-434.0193 69.0001,-434.0193 69.0001,-434.0193 69,-430.5193 65.8501,-434.0193 69,-427.0193 69,-427.0193\"/>\n",
"</g>\n",
"<!-- 1 -->\n",
"<g id=\"node3\" class=\"node\">\n",
"<title>1</title>\n",
"<ellipse fill=\"#ffffaa\" stroke=\"#000000\" cx=\"18\" cy=\"-307\" rx=\"18\" ry=\"18\"/>\n",
"<text text-anchor=\"middle\" x=\"18\" y=\"-303.3\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">1</text>\n",
"</g>\n",
"<!-- 0&#45;&gt;1 -->\n",
"<g id=\"edge2\" class=\"edge\">\n",
"<title>0&#45;&gt;1</title>\n",
"<path fill=\"none\" stroke=\"#000000\" d=\"M60.806,-392.6119C52.3298,-375.6595 39.0233,-349.0465 29.4966,-329.9931\"/>\n",
"<polygon fill=\"#000000\" stroke=\"#000000\" points=\"26.1737,-323.3474 32.1217,-328.1996 27.739,-326.4779 29.3042,-329.6084 29.3042,-329.6084 29.3042,-329.6084 27.739,-326.4779 26.4868,-331.0171 26.1737,-323.3474 26.1737,-323.3474\"/>\n",
"<text text-anchor=\"start\" x=\"62.5\" y=\"-361.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">a</text>\n",
"<text text-anchor=\"start\" x=\"50\" y=\"-347.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">⓿</text>\n",
"<text text-anchor=\"start\" x=\"66\" y=\"-347.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#ff4da0\">❶</text>\n",
"</g>\n",
"<!-- 2 -->\n",
"<g id=\"node4\" class=\"node\">\n",
"<title>2</title>\n",
"<ellipse fill=\"#ffffaa\" stroke=\"#000000\" cx=\"122\" cy=\"-307\" rx=\"18\" ry=\"18\"/>\n",
"<text text-anchor=\"middle\" x=\"122\" y=\"-303.3\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">2</text>\n",
"</g>\n",
"<!-- 0&#45;&gt;2 -->\n",
"<g id=\"edge3\" class=\"edge\">\n",
"<title>0&#45;&gt;2</title>\n",
"<path fill=\"none\" stroke=\"#000000\" d=\"M77.5154,-392.6119C86.415,-375.4844 100.4385,-348.4957 110.3581,-329.4052\"/>\n",
"<polygon fill=\"#000000\" stroke=\"#000000\" points=\"113.6805,-323.0111 113.2481,-330.675 112.0667,-326.1169 110.4529,-329.2226 110.4529,-329.2226 110.4529,-329.2226 112.0667,-326.1169 107.6577,-327.7702 113.6805,-323.0111 113.6805,-323.0111\"/>\n",
"<text text-anchor=\"start\" x=\"103.5\" y=\"-361.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">!a</text>\n",
"<text text-anchor=\"start\" x=\"101\" y=\"-346.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#ff4da0\">❶</text>\n",
"</g>\n",
"<!-- 1&#45;&gt;1 -->\n",
"<g id=\"edge4\" class=\"edge\">\n",
"<title>1&#45;&gt;1</title>\n",
"<path fill=\"none\" stroke=\"#000000\" d=\"M34.6641,-314.3828C44.625,-316.0234 54,-313.5625 54,-307 54,-302.0781 48.7266,-299.4634 41.8876,-299.1558\"/>\n",
"<polygon fill=\"#000000\" stroke=\"#000000\" points=\"34.6641,-299.6172 41.449,-296.0273 38.1569,-299.394 41.6498,-299.1709 41.6498,-299.1709 41.6498,-299.1709 38.1569,-299.394 41.8507,-302.3145 34.6641,-299.6172 34.6641,-299.6172\"/>\n",
"<text text-anchor=\"start\" x=\"63.5\" y=\"-310.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">!b</text>\n",
"<text text-anchor=\"start\" x=\"54\" y=\"-296.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">⓿</text>\n",
"<text text-anchor=\"start\" x=\"70\" y=\"-296.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#ff4da0\">❶</text>\n",
"</g>\n",
"<!-- 3 -->\n",
"<g id=\"node5\" class=\"node\">\n",
"<title>3</title>\n",
"<ellipse fill=\"#ffffaa\" stroke=\"#000000\" cx=\"114\" cy=\"-18\" rx=\"18\" ry=\"18\"/>\n",
"<text text-anchor=\"middle\" x=\"114\" y=\"-14.3\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">3</text>\n",
"</g>\n",
"<!-- 2&#45;&gt;3 -->\n",
"<g id=\"edge5\" class=\"edge\">\n",
"<title>2&#45;&gt;3</title>\n",
"<path fill=\"none\" stroke=\"#000000\" d=\"M111.1321,-292.1353C106.9052,-285.848 102.2966,-278.3002 99,-271 82.4421,-234.3339 79.6104,-223.8383 74,-184 65.8176,-125.8982 77.7857,-109.4398 97,-54 98.5151,-49.6285 100.4001,-45.0818 102.3581,-40.7504\"/>\n",
"<polygon fill=\"#000000\" stroke=\"#000000\" points=\"105.4521,-34.1772 105.3209,-41.8522 103.9615,-37.3439 102.4709,-40.5106 102.4709,-40.5106 102.4709,-40.5106 103.9615,-37.3439 99.6208,-39.169 105.4521,-34.1772 105.4521,-34.1772\"/>\n",
"<text text-anchor=\"start\" x=\"74\" y=\"-172.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">a &amp; b</text>\n",
"<text text-anchor=\"start\" x=\"75\" y=\"-158.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">⓿</text>\n",
"<text text-anchor=\"start\" x=\"91\" y=\"-158.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#ff4da0\">❶</text>\n",
"</g>\n",
"<!-- 4 -->\n",
"<g id=\"node6\" class=\"node\">\n",
"<title>4</title>\n",
"<ellipse fill=\"#ffffaa\" stroke=\"#000000\" cx=\"168\" cy=\"-118\" rx=\"18\" ry=\"18\"/>\n",
"<text text-anchor=\"middle\" x=\"168\" y=\"-114.3\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">4</text>\n",
"</g>\n",
"<!-- 2&#45;&gt;4 -->\n",
"<g id=\"edge6\" class=\"edge\">\n",
"<title>2&#45;&gt;4</title>\n",
"<path fill=\"none\" stroke=\"#000000\" d=\"M114.3235,-290.6052C105.5847,-269.6095 93.7669,-232.316 104,-202 112.9556,-175.4686 134.0061,-150.6953 149.5316,-135.0263\"/>\n",
"<polygon fill=\"#000000\" stroke=\"#000000\" points=\"154.5595,-130.0721 151.7842,-137.229 152.0664,-132.5286 149.5733,-134.9852 149.5733,-134.9852 149.5733,-134.9852 152.0664,-132.5286 147.3625,-132.7414 154.5595,-130.0721 154.5595,-130.0721\"/>\n",
"<text text-anchor=\"start\" x=\"104\" y=\"-223.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">!a &amp; b</text>\n",
"<text text-anchor=\"start\" x=\"114.5\" y=\"-208.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">⓿</text>\n",
"</g>\n",
"<!-- 5 -->\n",
"<g id=\"node7\" class=\"node\">\n",
"<title>5</title>\n",
"<ellipse fill=\"#ffffaa\" stroke=\"#000000\" cx=\"336\" cy=\"-118\" rx=\"18\" ry=\"18\"/>\n",
"<text text-anchor=\"middle\" x=\"336\" y=\"-114.3\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">5</text>\n",
"</g>\n",
"<!-- 2&#45;&gt;5 -->\n",
"<g id=\"edge7\" class=\"edge\">\n",
"<title>2&#45;&gt;5</title>\n",
"<path fill=\"none\" stroke=\"#000000\" d=\"M139.3336,-300.9028C166.1019,-290.875 218.1497,-268.8882 254,-238 286.2495,-210.2142 311.605,-166.9367 325.1476,-140.6522\"/>\n",
"<polygon fill=\"#000000\" stroke=\"#000000\" points=\"328.3331,-134.3556 327.9839,-142.0238 326.7531,-137.4787 325.1731,-140.6018 325.1731,-140.6018 325.1731,-140.6018 326.7531,-137.4787 322.3623,-139.1797 328.3331,-134.3556 328.3331,-134.3556\"/>\n",
"<text text-anchor=\"start\" x=\"286\" y=\"-223.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">a &amp; !b</text>\n",
"<text text-anchor=\"start\" x=\"296.5\" y=\"-208.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#ff4da0\">❶</text>\n",
"</g>\n",
"<!-- 6 -->\n",
"<g id=\"node8\" class=\"node\">\n",
"<title>6</title>\n",
"<ellipse fill=\"#ffffaa\" stroke=\"#000000\" cx=\"168\" cy=\"-220\" rx=\"18\" ry=\"18\"/>\n",
"<text text-anchor=\"middle\" x=\"168\" y=\"-216.3\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">6</text>\n",
"</g>\n",
"<!-- 2&#45;&gt;6 -->\n",
"<g id=\"edge8\" class=\"edge\">\n",
"<title>2&#45;&gt;6</title>\n",
"<path fill=\"none\" stroke=\"#000000\" d=\"M130.4371,-291.0429C137.6541,-277.3933 148.1209,-257.5975 156.1737,-242.3671\"/>\n",
"<polygon fill=\"#000000\" stroke=\"#000000\" points=\"159.4606,-236.1506 158.9733,-243.8113 157.8246,-239.2447 156.1886,-242.3389 156.1886,-242.3389 156.1886,-242.3389 157.8246,-239.2447 153.4039,-240.8665 159.4606,-236.1506 159.4606,-236.1506\"/>\n",
"<text text-anchor=\"start\" x=\"147\" y=\"-259.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">!a &amp; !b</text>\n",
"</g>\n",
"<!-- 3&#45;&gt;3 -->\n",
"<g id=\"edge9\" class=\"edge\">\n",
"<title>3&#45;&gt;3</title>\n",
"<path fill=\"none\" stroke=\"#000000\" d=\"M129.916,-26.6334C140.1504,-28.8856 150,-26.0078 150,-18 150,-11.869 144.2263,-8.7452 136.9268,-8.6284\"/>\n",
"<polygon fill=\"#000000\" stroke=\"#000000\" points=\"129.916,-9.3666 136.5477,-5.5008 133.3968,-9 136.8775,-8.6335 136.8775,-8.6335 136.8775,-8.6335 133.3968,-9 137.2074,-11.7662 129.916,-9.3666 129.916,-9.3666\"/>\n",
"<text text-anchor=\"start\" x=\"161.5\" y=\"-21.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">1</text>\n",
"<text text-anchor=\"start\" x=\"150\" y=\"-7.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">⓿</text>\n",
"<text text-anchor=\"start\" x=\"166\" y=\"-7.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#ff4da0\">❶</text>\n",
"</g>\n",
"<!-- 4&#45;&gt;3 -->\n",
"<g id=\"edge10\" class=\"edge\">\n",
"<title>4&#45;&gt;3</title>\n",
"<path fill=\"none\" stroke=\"#000000\" d=\"M159.324,-101.9333C150.3491,-85.3132 136.2599,-59.2221 126.1728,-40.5423\"/>\n",
"<polygon fill=\"#000000\" stroke=\"#000000\" points=\"122.6545,-34.0269 128.7523,-38.6895 124.3175,-37.1065 125.9806,-40.1862 125.9806,-40.1862 125.9806,-40.1862 124.3175,-37.1065 123.2089,-41.6829 122.6545,-34.0269 122.6545,-34.0269\"/>\n",
"<text text-anchor=\"start\" x=\"159.5\" y=\"-71.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">a</text>\n",
"<text text-anchor=\"start\" x=\"147\" y=\"-57.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">⓿</text>\n",
"<text text-anchor=\"start\" x=\"163\" y=\"-57.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#ff4da0\">❶</text>\n",
"</g>\n",
"<!-- 4&#45;&gt;4 -->\n",
"<g id=\"edge11\" class=\"edge\">\n",
"<title>4&#45;&gt;4</title>\n",
"<path fill=\"none\" stroke=\"#000000\" d=\"M185.7817,-122.4941C195.3149,-123.2578 204,-121.7598 204,-118 204,-115.2389 199.3161,-113.6976 193.0521,-113.3761\"/>\n",
"<polygon fill=\"#000000\" stroke=\"#000000\" points=\"185.7817,-113.5059 192.7243,-110.2313 189.2812,-113.4434 192.7806,-113.3808 192.7806,-113.3808 192.7806,-113.3808 189.2812,-113.4434 192.8369,-116.5303 185.7817,-113.5059 185.7817,-113.5059\"/>\n",
"<text text-anchor=\"start\" x=\"204\" y=\"-121.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">!a &amp; !b</text>\n",
"<text text-anchor=\"start\" x=\"216.5\" y=\"-106.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">⓿</text>\n",
"</g>\n",
"<!-- 4&#45;&gt;4 -->\n",
"<g id=\"edge12\" class=\"edge\">\n",
"<title>4&#45;&gt;4</title>\n",
"<path fill=\"none\" stroke=\"#000000\" d=\"M185.0174,-124.4905C209.3485,-129.8803 245,-127.7168 245,-118 245,-109.1942 215.7198,-106.5917 192.1203,-110.1928\"/>\n",
"<polygon fill=\"#000000\" stroke=\"#000000\" points=\"185.0174,-111.5095 191.326,-107.1363 188.4588,-110.8715 191.9002,-110.2335 191.9002,-110.2335 191.9002,-110.2335 188.4588,-110.8715 192.4744,-113.3307 185.0174,-111.5095 185.0174,-111.5095\"/>\n",
"<text text-anchor=\"start\" x=\"245\" y=\"-121.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">!a &amp; b</text>\n",
"<text text-anchor=\"start\" x=\"247.5\" y=\"-107.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">⓿</text>\n",
"<text text-anchor=\"start\" x=\"263.5\" y=\"-107.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#ff4da0\">❶</text>\n",
"</g>\n",
"<!-- 5&#45;&gt;3 -->\n",
"<g id=\"edge13\" class=\"edge\">\n",
"<title>5&#45;&gt;3</title>\n",
"<path fill=\"none\" stroke=\"#000000\" d=\"M321.1759,-107.3876C317.3021,-104.819 313.0694,-102.1865 309,-100 249.8571,-68.2231 175.7422,-40.0144 138.1989,-26.4825\"/>\n",
"<polygon fill=\"#000000\" stroke=\"#000000\" points=\"131.1931,-23.9751 138.8452,-23.3682 134.4884,-25.1545 137.7837,-26.3339 137.7837,-26.3339 137.7837,-26.3339 134.4884,-25.1545 136.7222,-29.2997 131.1931,-23.9751 131.1931,-23.9751\"/>\n",
"<text text-anchor=\"start\" x=\"283.5\" y=\"-71.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">b</text>\n",
"<text text-anchor=\"start\" x=\"272\" y=\"-57.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">⓿</text>\n",
"<text text-anchor=\"start\" x=\"288\" y=\"-57.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#ff4da0\">❶</text>\n",
"</g>\n",
"<!-- 5&#45;&gt;5 -->\n",
"<g id=\"edge14\" class=\"edge\">\n",
"<title>5&#45;&gt;5</title>\n",
"<path fill=\"none\" stroke=\"#000000\" d=\"M351.916,-126.6334C362.1504,-128.8856 372,-126.0078 372,-118 372,-111.869 366.2263,-108.7452 358.9268,-108.6284\"/>\n",
"<polygon fill=\"#000000\" stroke=\"#000000\" points=\"351.916,-109.3666 358.5477,-105.5008 355.3968,-109 358.8775,-108.6335 358.8775,-108.6335 358.8775,-108.6335 355.3968,-109 359.2074,-111.7662 351.916,-109.3666 351.916,-109.3666\"/>\n",
"<text text-anchor=\"start\" x=\"373.5\" y=\"-121.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">!b</text>\n",
"<text text-anchor=\"start\" x=\"372\" y=\"-106.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#ff4da0\">❶</text>\n",
"</g>\n",
"<!-- 6&#45;&gt;3 -->\n",
"<g id=\"edge15\" class=\"edge\">\n",
"<title>6&#45;&gt;3</title>\n",
"<path fill=\"none\" stroke=\"#000000\" d=\"M154.9131,-207.5268C139.9793,-192.2977 116.409,-164.9691 107,-136 96.946,-105.045 102.0356,-67.1566 107.3642,-42.8056\"/>\n",
"<polygon fill=\"#000000\" stroke=\"#000000\" points=\"109.0091,-35.7056 110.4979,-43.236 108.2192,-39.1153 107.4292,-42.525 107.4292,-42.525 107.4292,-42.525 108.2192,-39.1153 104.3604,-41.814 109.0091,-35.7056 109.0091,-35.7056\"/>\n",
"<text text-anchor=\"start\" x=\"107\" y=\"-121.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">a &amp; b</text>\n",
"<text text-anchor=\"start\" x=\"108\" y=\"-107.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">⓿</text>\n",
"<text text-anchor=\"start\" x=\"124\" y=\"-107.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#ff4da0\">❶</text>\n",
"</g>\n",
"<!-- 6&#45;&gt;4 -->\n",
"<g id=\"edge16\" class=\"edge\">\n",
"<title>6&#45;&gt;4</title>\n",
"<path fill=\"none\" stroke=\"#000000\" d=\"M168,-201.7644C168,-185.5192 168,-161.5825 168,-143.4527\"/>\n",
"<polygon fill=\"#000000\" stroke=\"#000000\" points=\"168,-136.0777 171.1501,-143.0776 168,-139.5777 168.0001,-143.0777 168.0001,-143.0777 168.0001,-143.0777 168,-139.5777 164.8501,-143.0777 168,-136.0777 168,-136.0777\"/>\n",
"<text text-anchor=\"start\" x=\"168\" y=\"-172.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">!a &amp; b</text>\n",
"<text text-anchor=\"start\" x=\"170.5\" y=\"-158.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">⓿</text>\n",
"<text text-anchor=\"start\" x=\"186.5\" y=\"-158.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#ff4da0\">❶</text>\n",
"</g>\n",
"<!-- 6&#45;&gt;5 -->\n",
"<g id=\"edge17\" class=\"edge\">\n",
"<title>6&#45;&gt;5</title>\n",
"<path fill=\"none\" stroke=\"#000000\" d=\"M181.5924,-207.8275C198.322,-193.3609 228.0796,-169.2651 257,-154 278.6285,-142.5838 287.0924,-146.8711 309,-136 311.0691,-134.9733 313.1679,-133.8137 315.234,-132.5902\"/>\n",
"<polygon fill=\"#000000\" stroke=\"#000000\" points=\"321.2711,-128.7968 317.02,-135.1883 318.3076,-130.6589 315.344,-132.5211 315.344,-132.5211 315.344,-132.5211 318.3076,-130.6589 313.6681,-129.8539 321.2711,-128.7968 321.2711,-128.7968\"/>\n",
"<text text-anchor=\"start\" x=\"257\" y=\"-172.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">a &amp; !b</text>\n",
"<text text-anchor=\"start\" x=\"267.5\" y=\"-157.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#ff4da0\">❶</text>\n",
"</g>\n",
"<!-- 6&#45;&gt;6 -->\n",
"<g id=\"edge18\" class=\"edge\">\n",
"<title>6&#45;&gt;6</title>\n",
"<path fill=\"none\" stroke=\"#000000\" d=\"M184.6641,-227.3828C194.625,-229.0234 204,-226.5625 204,-220 204,-215.0781 198.7266,-212.4634 191.8876,-212.1558\"/>\n",
"<polygon fill=\"#000000\" stroke=\"#000000\" points=\"184.6641,-212.6172 191.449,-209.0273 188.1569,-212.394 191.6498,-212.1709 191.6498,-212.1709 191.6498,-212.1709 188.1569,-212.394 191.8507,-215.3145 184.6641,-212.6172 184.6641,-212.6172\"/>\n",
"<text text-anchor=\"start\" x=\"204\" y=\"-216.3\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">!a &amp; !b</text>\n",
"</g>\n",
"</g>\n",
"</svg>\n",
"</div>"
],
"text/plain": [
"<IPython.core.display.HTML object>"
]
},
"metadata": {},
"output_type": "display_data"
}
],
"source": [
"pos = spot.automaton(\"\"\"HOA: v1 name: \"(a & (Fa R XFb)) | (!a & (G!a U\n",
"XG!b))\" States: 6 Start: 0 AP: 2 \"a\" \"b\" acc-name: Buchi Acceptance: 1\n",
"Inf(0) properties: trans-labels explicit-labels state-acc\n",
"semi-deterministic --BODY-- State: 0 [0] 1 [!0] 2 [!0] 3 State: 1 [!1]\n",
"1 [1] 4 State: 2 {0} [!1] 2 State: 3 [!0] 3 [!0] 5 State: 4 {0} [t] 4\n",
"State: 5 {0} [!0&!1] 5 --END--\"\"\")\n",
"altneg = spot.dualize(pos)\n",
"neg = spot.remove_alternation(altneg)\n",
"display_inline(pos, altneg.show('.bvu'), neg)"
]
},
{
"cell_type": "code",
"execution_count": 10,
"metadata": {},
"outputs": [],
"source": [
"# Issue #382.\n",
"w = spot.parse_word('cycle{!a&b}').as_automaton()\n",
"assert pos.intersects(w) != neg.intersects(w)"
]
}
],
"metadata": {
@ -3621,7 +4160,7 @@
"name": "python",
"nbconvert_exporter": "python",
"pygments_lexer": "ipython3",
"version": "3.6.5"
"version": "3.7.3rc1"
}
},
"nbformat": 4,