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 645935f796
commit 260a141b1c
5 changed files with 87 additions and 70 deletions
Download patch file Download diff file Expand all files Collapse all files

6
NEWS
View file

@ -42,6 +42,12 @@ New in spot 2.9.0.dev (not yet released)
bits. This affects the output of "ltlcross --csv" and
"--stats=%t" for many tools.
- simplify_acceptance() missed some patterns it should have been
able to simplify. For instance Fin(0)&(Fin(1)|Fin(2)|Fin(4))
should simplify to Fin(1)|Fin(2)|Fin(4) adter adding {1,2,4} to
every place where 0 occur, and then the acceptance would be
renumbered to Fin(0)|Fin(1)|Fin(2). This is now fixed.
New in spot 2.9 (2020-04-30)
Command-line tools:

24
spot/twaalgos/cleanacc.cc
View file

@ -390,7 +390,7 @@ namespace spot
case acc_cond::acc_op::FinNeg:
{
auto m = pos[-1].mark;
if (op == wanted && m.is_singleton())
if (op == wanted)
{
res |= m;
}
@ -427,7 +427,7 @@ namespace spot
if (op == wanted)
{
auto m = pos[-1].mark;
if (!seen && m.is_singleton())
if (!seen)
{
seen = true;
res |= m;
@ -512,9 +512,9 @@ namespace spot
case acc_cond::acc_op::Inf:
case acc_cond::acc_op::Fin:
{
auto m = pos[-1].mark;
if (op == wanted && m.is_singleton())
singletons.emplace_back(m, pos);
if (op == wanted)
singletons.emplace_back(pos[-1].mark,
pos);
pos -= 2;
}
break;
@ -526,20 +526,20 @@ namespace spot
// {b,d} can receive {a} if they
// (b and d) are both used once.
if (auto m = find_interm_rec(pos))
{
singletons.emplace_back(m, pos);
// move this to the front, to
// be sure it is the first
// recipient tried.
swap(singletons.front(),
singletons.back());
}
pos -= pos->sub.size + 1;
break;
}
}
while (pos > rend);
// sort the singletons vector: we want
// those that are not really singleton to
// be first to they can become recipient
std::partition(singletons.begin(), singletons.end(),
[&] (auto s)
{ return !s.first.is_singleton(); });
acc_cond::mark_t can_receive = {};
for (auto p: singletons)
if ((p.first & once) == p.first)

37
tests/core/remfin.test
View file

@ -292,8 +292,6 @@ State: 1
--END--
EOF
acctwelve='Inf(0)&Inf(1)&Inf(2)&Inf(3)&Inf(4)&Inf(5)'
acctwelve=$acctwelve'&Inf(6)&Inf(7)&Inf(8)&Inf(9)&Inf(10)&Inf(11)'
cat >expected <<EOF
HOA: v1
States: 3
@ -339,21 +337,22 @@ HOA: v1
States: 3
Start: 0
AP: 2 "a" "b"
Acceptance: 3 (Inf(1)&Inf(2)) | Inf(0)
acc-name: generalized-Buchi 2
Acceptance: 2 Inf(0)&Inf(1)
properties: trans-labels explicit-labels trans-acc
--BODY--
State: 0
[t] 0 {2}
[0] 1 {2}
[!0] 2 {0 2}
[t] 0 {1}
[0] 1 {1}
[!0] 2 {0 1}
State: 1
[1] 0 {2}
[0&1] 1 {0 2}
[!0&1] 2 {1 2}
[1] 0 {1}
[0&1] 1 {0 1}
[!0&1] 2 {0 1}
State: 2
[!1] 0
[0&!1] 1 {0}
[!0&!1] 2 {0}
[0&!1] 1 {0 1}
[!0&!1] 2 {0 1}
--END--
HOA: v1
States: 1
@ -867,7 +866,7 @@ HOA: v1
States: 6
Start: 0
AP: 3 "a" "b" "c"
Acceptance: 4 (Inf(0)&Inf(2)&Inf(3)) | (Inf(0)&Inf(1)&Inf(3))
Acceptance: 3 (Inf(1)&Inf(2)) | (Inf(0)&Inf(2))
properties: trans-labels explicit-labels trans-acc
--BODY--
State: 0
@ -883,16 +882,16 @@ State: 1
[2] 4
[!2] 5
State: 2
[0] 2 {0 1 3}
[0] 2 {0 2}
State: 3
[0&2] 2 {0 1 3}
[0&!2] 3 {0 1}
[0&2] 2 {0 2}
[0&!2] 3 {0}
State: 4
[1 | 2] 4 {0 2 3}
[!1&!2] 5 {0 2}
[1 | 2] 4 {1 2}
[!1&!2] 5 {1}
State: 5
[2] 4 {0 2 3}
[!2] 5 {0 2}
[2] 4 {1 2}
[!2] 5 {1}
--END--
EOF

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,

14
tests/python/simplacc.py
View file

@ -50,6 +50,16 @@ State: 5 [!0&1] 4 {3 5} [!0&1] 3 {2 4} [!0&1] 2 {2 3} [!0&!1] 0 {0}
[!0&1] 7 {0 4 5} [0&1] 5 {2} State: 6 [0&!1] 7 [0&!1] 1 {1 4} [0&1]
4 {1 4} State: 7 [0&1] 3 {2 3} [0&1] 0 [!0&!1] 6 [0&1] 1 State: 8 [0&1]
3 [!0&!1] 0 [0&1] 9 State: 9 [0&!1] 7 {4 5} [!0&1] 8 {0} [0&1] 9 --END--
/* Derived from issue #405. */
HOA: v1 States: 2 Start: 0 AP: 2 "p0" "p1" Acceptance: 4 Fin(0) &
(Fin(1)|Fin(2)|Fin(3)) properties: trans-labels explicit-labels trans-acc
--BODY-- State: 0 [!0&!1] 0 {0 1 3} [0&1] 1 {0 2} [0&!1] 0 {2} State:
1 [0&1] 0 {0 2} [0&1] 1 {1} [0&!1] 1 --END--
/* More complex version of the previous automaton */
HOA: v1 States: 2 Start: 0 AP: 2 "p0" "p1" Acceptance: 5 Fin(0) &
(((Fin(1)|Fin(2)|Fin(3))&Inf(4)|Fin(3))) properties: trans-labels
explicit-labels trans-acc --BODY-- State: 0 [!0&!1] 0 {0 1 3} [0&1] 1
{0 2} [0&!1] 0 {2} State: 1 [0&1] 0 {0 2} [0&1] 1 {1} [0&!1] 1 {4} --END--
"""))
res = []
@ -80,4 +90,8 @@ assert res == [
'((Inf(1) & Fin(2)) | Fin(5)) & (Inf(0) | (Inf(1) & (Inf(3) | Fin(4))))',
'Inf(0)',
'Fin(0)',
'Fin(0)|Fin(1)|Fin(2)',
'Inf(0)&Inf(1)&Inf(2)',
'((Fin(0)|Fin(1)) & Inf(3)) | Fin(2)',
'((Inf(0)&Inf(1)) | Fin(3)) & Inf(2)',
]