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

improve fuse_marks_here by detecting more patterns

Browse source 
This remove some restrictions that prevented fuse_marks_here from
simplifying certain patterns, as noted in the first comment of
issue #405.

* spot/twaalgos/cleanacc.cc (find_interm_rec, find_fusable): Remove
some unnecessary restrictions to singleton marks, and replace the hack
put one non-singleton mark at the beginning of the singleton list by a
sort.
* tests/python/simplacc.py: Add two test cases.
* tests/python/automata.ipynb, tests/core/remfin.test: Improve
expected results.
* NEWS: Mention the bug.
This commit is contained in:
Alexandre Duret-Lutz 2020-05-22 16:09:26 +02:00
parent ce695e67f9
commit c005041e53
5 changed files with 87 additions and 70 deletions
Download patch file Download diff file Expand all files Collapse all files

74
tests/python/automata.ipynb
View file

@ -178,7 +178,7 @@
"</svg>\n"
],
"text/plain": [
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fbc2c2c2bd0> >"
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f9f5d7cbd50> >"
]
},
"execution_count": 2,
@ -657,7 +657,7 @@
"</svg>\n"
],
"text/plain": [
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fbc2c2c9270> >"
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f9f5d7cf480> >"
]
},
"execution_count": 6,
@ -733,7 +733,7 @@
"</svg>\n"
],
"text/plain": [
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fbc2c2c9a20> >"
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f9f5d7cfc00> >"
]
},
"execution_count": 7,
@ -816,7 +816,7 @@
"</svg>\n"
],
"text/plain": [
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fbc2c2ce600> >"
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f9f5d7cf3f0> >"
]
},
"execution_count": 8,
@ -1349,7 +1349,7 @@
"</svg>\n"
],
"text/plain": [
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fbc2c2de5d0> >"
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f9f5d7d4930> >"
]
},
"execution_count": 12,
@ -1463,7 +1463,7 @@
"</svg>\n"
],
"text/plain": [
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fbc2c2defc0> >"
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f9f5d7d4cc0> >"
]
},
"execution_count": 13,
@ -1594,7 +1594,7 @@
"</svg>\n"
],
"text/plain": [
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fbc2c2e4270> >"
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f9f5d7d4990> >"
]
},
"execution_count": 14,
@ -1816,7 +1816,7 @@
"</svg>\n"
],
"text/plain": [
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fbc2c2e4180> >"
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f9f5d7d4b70> >"
]
},
"metadata": {},
@ -1835,16 +1835,14 @@
" viewBox=\"0.00 0.00 482.00 315.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
"<g id=\"graph0\" class=\"graph\" transform=\"scale(1.0 1.0) rotate(0) translate(4 311)\">\n",
"<polygon fill=\"white\" stroke=\"transparent\" points=\"-4,4 -4,-311 478,-311 478,4 -4,4\"/>\n",
"<text text-anchor=\"start\" x=\"135.5\" y=\"-292.8\" font-family=\"Lato\" font-size=\"14.00\">Inf(</text>\n",
"<text text-anchor=\"start\" x=\"156.5\" y=\"-292.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">⓿</text>\n",
"<text text-anchor=\"start\" x=\"172.5\" y=\"-292.8\" font-family=\"Lato\" font-size=\"14.00\">) | Inf(</text>\n",
"<text text-anchor=\"start\" x=\"208.5\" y=\"-292.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#ff4da0\">❶</text>\n",
"<text text-anchor=\"start\" x=\"224.5\" y=\"-292.8\" font-family=\"Lato\" font-size=\"14.00\">) | (Inf(</text>\n",
"<text text-anchor=\"start\" x=\"264.5\" y=\"-292.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#ff7f00\">❷</text>\n",
"<text text-anchor=\"start\" x=\"280.5\" y=\"-292.8\" font-family=\"Lato\" font-size=\"14.00\">)&amp;Inf(</text>\n",
"<text text-anchor=\"start\" x=\"314.5\" y=\"-292.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#6a3d9a\">❸</text>\n",
"<text text-anchor=\"start\" x=\"330.5\" y=\"-292.8\" font-family=\"Lato\" font-size=\"14.00\">))</text>\n",
"<text text-anchor=\"start\" x=\"203\" y=\"-278.8\" font-family=\"Lato\" font-size=\"14.00\">[Fin&#45;less 4]</text>\n",
"<text text-anchor=\"start\" x=\"161.5\" y=\"-292.8\" font-family=\"Lato\" font-size=\"14.00\">Inf(</text>\n",
"<text text-anchor=\"start\" x=\"182.5\" y=\"-292.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">⓿</text>\n",
"<text text-anchor=\"start\" x=\"198.5\" y=\"-292.8\" font-family=\"Lato\" font-size=\"14.00\">) | (Inf(</text>\n",
"<text text-anchor=\"start\" x=\"238.5\" y=\"-292.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#ff4da0\">❶</text>\n",
"<text text-anchor=\"start\" x=\"254.5\" y=\"-292.8\" font-family=\"Lato\" font-size=\"14.00\">)&amp;Inf(</text>\n",
"<text text-anchor=\"start\" x=\"288.5\" y=\"-292.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#ff7f00\">❷</text>\n",
"<text text-anchor=\"start\" x=\"304.5\" y=\"-292.8\" font-family=\"Lato\" font-size=\"14.00\">))</text>\n",
"<text text-anchor=\"start\" x=\"203\" y=\"-278.8\" font-family=\"Lato\" font-size=\"14.00\">[Fin&#45;less 3]</text>\n",
"<!-- I -->\n",
"<!-- 0 -->\n",
"<g id=\"node2\" class=\"node\">\n",
@ -1864,7 +1862,7 @@
"<path fill=\"none\" stroke=\"black\" d=\"M49.62,-114.04C48.32,-123.86 50.45,-133 56,-133 60.17,-133 62.4,-127.86 62.71,-121.14\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"62.38,-114.04 65.85,-120.88 62.54,-117.53 62.71,-121.03 62.71,-121.03 62.71,-121.03 62.54,-117.53 59.56,-121.18 62.38,-114.04 62.38,-114.04\"/>\n",
"<text text-anchor=\"start\" x=\"51.5\" y=\"-151.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
"<text text-anchor=\"start\" x=\"48\" y=\"-136.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#6a3d9a\">❸</text>\n",
"<text text-anchor=\"start\" x=\"48\" y=\"-136.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#ff7f00\">❷</text>\n",
"</g>\n",
"<!-- 1 -->\n",
"<g id=\"node3\" class=\"node\">\n",
@ -1879,7 +1877,7 @@
"<polygon fill=\"black\" stroke=\"black\" points=\"149.28,-159.12 142.59,-155.36 147.2,-156.31 145.12,-153.49 145.12,-153.49 145.12,-153.49 147.2,-156.31 147.66,-151.62 149.28,-159.12 149.28,-159.12\"/>\n",
"<text text-anchor=\"start\" x=\"104.5\" y=\"-148.8\" font-family=\"Lato\" font-size=\"14.00\">a</text>\n",
"<text text-anchor=\"start\" x=\"92\" y=\"-134.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#ff4da0\">❶</text>\n",
"<text text-anchor=\"start\" x=\"108\" y=\"-134.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#6a3d9a\">❸</text>\n",
"<text text-anchor=\"start\" x=\"108\" y=\"-134.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#ff7f00\">❷</text>\n",
"</g>\n",
"<!-- 2 -->\n",
"<g id=\"node4\" class=\"node\">\n",
@ -1893,7 +1891,7 @@
"<path fill=\"none\" stroke=\"black\" d=\"M74.42,-98.17C105.92,-100.35 174.44,-105.43 232,-112 235.48,-112.4 239.14,-112.87 242.73,-113.35\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"249.93,-114.37 242.56,-116.51 246.47,-113.88 243,-113.39 243,-113.39 243,-113.39 246.47,-113.88 243.44,-110.27 249.93,-114.37 249.93,-114.37\"/>\n",
"<text text-anchor=\"start\" x=\"154.5\" y=\"-124.8\" font-family=\"Lato\" font-size=\"14.00\">!a</text>\n",
"<text text-anchor=\"start\" x=\"152\" y=\"-109.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#6a3d9a\">❸</text>\n",
"<text text-anchor=\"start\" x=\"152\" y=\"-109.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#ff7f00\">❷</text>\n",
"</g>\n",
"<!-- 3 -->\n",
"<g id=\"node5\" class=\"node\">\n",
@ -1914,7 +1912,7 @@
"<path fill=\"none\" stroke=\"black\" d=\"M141.73,-173.91C127.17,-173.02 106.45,-169.73 92,-159 79.24,-149.53 70.47,-133.93 64.9,-120.75\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"62.27,-114.12 67.78,-119.47 63.56,-117.37 64.85,-120.63 64.85,-120.63 64.85,-120.63 63.56,-117.37 61.92,-121.79 62.27,-114.12 62.27,-114.12\"/>\n",
"<text text-anchor=\"start\" x=\"104\" y=\"-189.8\" font-family=\"Lato\" font-size=\"14.00\">b</text>\n",
"<text text-anchor=\"start\" x=\"100\" y=\"-174.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#6a3d9a\">❸</text>\n",
"<text text-anchor=\"start\" x=\"100\" y=\"-174.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#ff7f00\">❷</text>\n",
"</g>\n",
"<!-- 1&#45;&gt;1 -->\n",
"<g id=\"edge7\" class=\"edge\">\n",
@ -1922,7 +1920,7 @@
"<path fill=\"none\" stroke=\"black\" d=\"M151.02,-189.92C148.68,-200.15 151.67,-210 160,-210 166.38,-210 169.63,-204.23 169.75,-196.93\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"168.98,-189.92 172.87,-196.53 169.36,-193.4 169.74,-196.87 169.74,-196.87 169.74,-196.87 169.36,-193.4 166.61,-197.22 168.98,-189.92 168.98,-189.92\"/>\n",
"<text text-anchor=\"start\" x=\"144\" y=\"-228.8\" font-family=\"Lato\" font-size=\"14.00\">a &amp; b</text>\n",
"<text text-anchor=\"start\" x=\"152\" y=\"-213.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#6a3d9a\">❸</text>\n",
"<text text-anchor=\"start\" x=\"152\" y=\"-213.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#ff7f00\">❷</text>\n",
"</g>\n",
"<!-- 1&#45;&gt;2 -->\n",
"<g id=\"edge8\" class=\"edge\">\n",
@ -1930,8 +1928,8 @@
"<path fill=\"none\" stroke=\"black\" d=\"M177.47,-169.15C192.31,-164.41 214.43,-156.38 232,-146 237.89,-142.52 243.8,-138.07 249.04,-133.71\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"254.44,-129.07 251.19,-136.02 251.79,-131.35 249.14,-133.63 249.14,-133.63 249.14,-133.63 251.79,-131.35 247.08,-131.25 254.44,-129.07 254.44,-129.07\"/>\n",
"<text text-anchor=\"start\" x=\"196\" y=\"-179.8\" font-family=\"Lato\" font-size=\"14.00\">!a &amp; b</text>\n",
"<text text-anchor=\"start\" x=\"198\" y=\"-165.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#ff7f00\">❷</text>\n",
"<text text-anchor=\"start\" x=\"214\" y=\"-165.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#6a3d9a\">❸</text>\n",
"<text text-anchor=\"start\" x=\"198\" y=\"-165.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#ff4da0\">❶</text>\n",
"<text text-anchor=\"start\" x=\"214\" y=\"-165.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#ff7f00\">❷</text>\n",
"</g>\n",
"<!-- 1&#45;&gt;3 -->\n",
"<g id=\"edge9\" class=\"edge\">\n",
@ -2014,7 +2012,7 @@
"</svg>\n"
],
"text/plain": [
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fbc2c2e94e0> >"
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f9f5d7d4e40> >"
]
},
"metadata": {},
@ -2193,7 +2191,7 @@
"</svg>\n"
],
"text/plain": [
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fbc2c2e4300> >"
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f9f5d7d4c00> >"
]
},
"metadata": {},
@ -2341,7 +2339,7 @@
"</svg>\n"
],
"text/plain": [
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fbc2c2e9ed0> >"
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f9f658bbc90> >"
]
},
"metadata": {},
@ -2530,7 +2528,7 @@
"</svg>\n"
],
"text/plain": [
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fbc2c2f4060> >"
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f9f5d7d4c00> >"
]
},
"execution_count": 19,
@ -2606,7 +2604,7 @@
"</svg>\n"
],
"text/plain": [
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fbc2c2f4de0> >"
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f9f5d7e2f90> >"
]
},
"execution_count": 20,
@ -3156,7 +3154,7 @@
"</svg>\n"
],
"text/plain": [
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fbc2c2f4840> >"
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f9f5d7f18d0> >"
]
},
"metadata": {},
@ -3256,7 +3254,7 @@
"</svg>\n"
],
"text/plain": [
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fbc2c279390> >"
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f9f5d7d4b70> >"
]
},
"execution_count": 24,
@ -3329,7 +3327,7 @@
"</svg>\n"
],
"text/plain": [
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fbc2c280c60> >"
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f9f5d7f1330> >"
]
},
"execution_count": 25,
@ -3500,7 +3498,7 @@
"</svg>\n"
],
"text/plain": [
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fbc2c287cc0> >"
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f9f5d7f1450> >"
]
},
"execution_count": 27,
@ -3583,7 +3581,7 @@
"</svg>\n"
],
"text/plain": [
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fbc2c2f4840> >"
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f9f5d7f18d0> >"
]
},
"metadata": {},
@ -3648,7 +3646,7 @@
"</svg>\n"
],
"text/plain": [
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fbc2c2f4840> >"
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f9f5d7f18d0> >"
]
},
"metadata": {},
@ -3735,7 +3733,7 @@
"</svg>\n"
],
"text/plain": [
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fbc2c2f4840> >"
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f9f5d7f18d0> >"
]
},
"execution_count": 29,
@ -3768,7 +3766,7 @@
"name": "python",
"nbconvert_exporter": "python",
"pygments_lexer": "ipython3",
"version": "3.8.2"
"version": "3.8.3"
}
},
"nbformat": 4,