diff --git a/NEWS b/NEWS index 93dfdd42e..d025625a3 100644 --- a/NEWS +++ b/NEWS @@ -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: diff --git a/spot/twaalgos/cleanacc.cc b/spot/twaalgos/cleanacc.cc index ee47edc84..667f2e59e 100644 --- a/spot/twaalgos/cleanacc.cc +++ b/spot/twaalgos/cleanacc.cc @@ -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()); - } + singletons.emplace_back(m, pos); 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) diff --git a/tests/core/remfin.test b/tests/core/remfin.test index 73d7eec28..52ca43b89 100755 --- a/tests/core/remfin.test +++ b/tests/core/remfin.test @@ -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 <\n" ], "text/plain": [ - " *' at 0x7fbc2c2c2bd0> >" + " *' at 0x7f9f5d7cbd50> >" ] }, "execution_count": 2, @@ -657,7 +657,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fbc2c2c9270> >" + " *' at 0x7f9f5d7cf480> >" ] }, "execution_count": 6, @@ -733,7 +733,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fbc2c2c9a20> >" + " *' at 0x7f9f5d7cfc00> >" ] }, "execution_count": 7, @@ -816,7 +816,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fbc2c2ce600> >" + " *' at 0x7f9f5d7cf3f0> >" ] }, "execution_count": 8, @@ -1349,7 +1349,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fbc2c2de5d0> >" + " *' at 0x7f9f5d7d4930> >" ] }, "execution_count": 12, @@ -1463,7 +1463,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fbc2c2defc0> >" + " *' at 0x7f9f5d7d4cc0> >" ] }, "execution_count": 13, @@ -1594,7 +1594,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fbc2c2e4270> >" + " *' at 0x7f9f5d7d4990> >" ] }, "execution_count": 14, @@ -1816,7 +1816,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fbc2c2e4180> >" + " *' 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", "\n", "\n", - "Inf(\n", - "⓿\n", - ") | Inf(\n", - "❶\n", - ") | (Inf(\n", - "❷\n", - ")&Inf(\n", - "❸\n", - "))\n", - "[Fin-less 4]\n", + "Inf(\n", + "⓿\n", + ") | (Inf(\n", + "❶\n", + ")&Inf(\n", + "❷\n", + "))\n", + "[Fin-less 3]\n", "\n", "\n", "\n", @@ -1864,7 +1862,7 @@ "\n", "\n", "1\n", - "❸\n", + "❷\n", "\n", "\n", "\n", @@ -1879,7 +1877,7 @@ "\n", "a\n", "❶\n", - "❸\n", + "❷\n", "\n", "\n", "\n", @@ -1893,7 +1891,7 @@ "\n", "\n", "!a\n", - "❸\n", + "❷\n", "\n", "\n", "\n", @@ -1914,7 +1912,7 @@ "\n", "\n", "b\n", - "❸\n", + "❷\n", "\n", "\n", "\n", @@ -1922,7 +1920,7 @@ "\n", "\n", "a & b\n", - "❸\n", + "❷\n", "\n", "\n", "\n", @@ -1930,8 +1928,8 @@ "\n", "\n", "!a & b\n", - "❷\n", - "❸\n", + "❶\n", + "❷\n", "\n", "\n", "\n", @@ -2014,7 +2012,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fbc2c2e94e0> >" + " *' at 0x7f9f5d7d4e40> >" ] }, "metadata": {}, @@ -2193,7 +2191,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fbc2c2e4300> >" + " *' at 0x7f9f5d7d4c00> >" ] }, "metadata": {}, @@ -2341,7 +2339,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fbc2c2e9ed0> >" + " *' at 0x7f9f658bbc90> >" ] }, "metadata": {}, @@ -2530,7 +2528,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fbc2c2f4060> >" + " *' at 0x7f9f5d7d4c00> >" ] }, "execution_count": 19, @@ -2606,7 +2604,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fbc2c2f4de0> >" + " *' at 0x7f9f5d7e2f90> >" ] }, "execution_count": 20, @@ -3156,7 +3154,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fbc2c2f4840> >" + " *' at 0x7f9f5d7f18d0> >" ] }, "metadata": {}, @@ -3256,7 +3254,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fbc2c279390> >" + " *' at 0x7f9f5d7d4b70> >" ] }, "execution_count": 24, @@ -3329,7 +3327,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fbc2c280c60> >" + " *' at 0x7f9f5d7f1330> >" ] }, "execution_count": 25, @@ -3500,7 +3498,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fbc2c287cc0> >" + " *' at 0x7f9f5d7f1450> >" ] }, "execution_count": 27, @@ -3583,7 +3581,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fbc2c2f4840> >" + " *' at 0x7f9f5d7f18d0> >" ] }, "metadata": {}, @@ -3648,7 +3646,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fbc2c2f4840> >" + " *' at 0x7f9f5d7f18d0> >" ] }, "metadata": {}, @@ -3735,7 +3733,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fbc2c2f4840> >" + " *' 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, diff --git a/tests/python/simplacc.py b/tests/python/simplacc.py index e4e902dbd..a6bcc29ae 100644 --- a/tests/python/simplacc.py +++ b/tests/python/simplacc.py @@ -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)', ]