From 5ec9d55fea6651e4cd8627bf451eedc55ab07b4a Mon Sep 17 00:00:00 2001 From: Florian Renkin Date: Sat, 25 Jul 2020 19:15:17 +0200 Subject: [PATCH] simplify_acceptance: Use color inclusions to simplify a condition This fixes #406. * spot/twaalgos/cleanacc.cc: Add the simplification. * tests/core/remfin.test, tests/python/automata.ipynb, tests/python/remfin.py: Update tests. * tests/python/simplacc.py: Update and add tests. --- spot/twaalgos/cleanacc.cc | 99 +++++++- tests/core/remfin.test | 73 +++--- tests/python/automata.ipynb | 479 +++++++++++++++++++----------------- tests/python/remfin.py | 2 +- tests/python/simplacc.py | 15 +- 5 files changed, 395 insertions(+), 273 deletions(-) diff --git a/spot/twaalgos/cleanacc.cc b/spot/twaalgos/cleanacc.cc index 5a59dad6d..89d77af1d 100644 --- a/spot/twaalgos/cleanacc.cc +++ b/spot/twaalgos/cleanacc.cc @@ -613,6 +613,100 @@ namespace spot } } + static + acc_cond::mark_t merge_marks(acc_cond::mark_t colors, + std::vector inclusions) + { + bool changed; + do + { + changed = false; + for (unsigned c : colors.sets()) + { + if ((inclusions[c] & colors) != acc_cond::mark_t {}) + { + auto new_colors = (colors - inclusions[c]); + if (new_colors != colors) + changed = true; + colors = new_colors; + break; + } + } + } while (changed); + return colors; + } + + static + acc_cond::acc_code merge_colors(acc_cond::acc_code code, + std::vector inclusions) + { + if (code.empty()) + return {}; + int pos = code.size() - 1; + acc_cond::acc_code result; + do + { + switch (code[pos].sub.op) + { + case acc_cond::acc_op::And: + { + result = acc_cond::acc_code::t(); + --pos; + while (pos > 0) + { + result = merge_colors(acc_cond::acc_code(&code[pos]), inclusions) + & result; + pos -= (code[pos].sub.size + 1); + } + return result; + } + case acc_cond::acc_op::Or: + { + result = acc_cond::acc_code::f(); + --pos; + while (pos > 0) + { + result = merge_colors(acc_cond::acc_code(&code[pos]), inclusions) + | result; + pos -= (code[pos].sub.size + 1); + } + return result; + } + case acc_cond::acc_op::Fin: + { + auto res = acc_cond::acc_code::fin(merge_marks(code[pos - 1].mark, + inclusions)); + + return res; + } + case acc_cond::acc_op::Inf: + { + auto res = acc_cond::acc_code::inf(merge_marks(code[pos - 1].mark, + inclusions)); + return res; + } + default: + SPOT_UNREACHABLE(); + } + } while (pos > 0); + SPOT_UNREACHABLE(); + } + + // Create a vector of marks such that for every color c, result[c] contains + // all the colors that are on every transitions that also contain c + // (c is excluded). + static std::vector included_marks(twa_graph_ptr aut) + { + std::vector result(SPOT_MAX_ACCSETS, + acc_cond::mark_t::all()); + for (unsigned i = 0; i < SPOT_MAX_ACCSETS; ++i) + result[i]^= acc_cond::mark_t {i}; + for (auto& e: aut->edges()) + for (auto c : e.acc.sets()) + result[c] &= e.acc; + return result; + } + twa_graph_ptr simplify_acceptance_here(twa_graph_ptr aut) { for (;;) @@ -621,7 +715,10 @@ namespace spot merge_identical_marks_here(aut); if (aut->acc().is_generalized_buchi()) break; - acc_cond::acc_code old = aut->get_acceptance(); + auto inc = included_marks(aut); + auto new_code = merge_colors(aut->get_acceptance(), inc); + aut->set_acceptance(acc_cond(aut->num_sets(), new_code)); + acc_cond::acc_code old = new_code; aut->set_acceptance(aut->acc().unit_propagation()); simplify_complementary_marks_here(aut); fuse_marks_here(aut); diff --git a/tests/core/remfin.test b/tests/core/remfin.test index 928820e6d..441fb21ea 100755 --- a/tests/core/remfin.test +++ b/tests/core/remfin.test @@ -311,48 +311,46 @@ State: 2 {0} [!1] 2 --END-- HOA: v1 -States: 4 +States: 3 Start: 0 AP: 2 "a" "b" -Acceptance: 4 Inf(0) | Inf(3) | (Inf(1)&Inf(2)) +acc-name: Buchi +Acceptance: 1 Inf(0) properties: trans-labels explicit-labels trans-acc --BODY-- State: 0 -[t] 0 {1 3} -[0] 1 {1 3} -[!0] 2 {1 3} +[t] 0 {0} +[0] 1 {0} +[!0] 2 {0} State: 1 -[1] 0 {1} -[0&1] 1 {1} -[!0&1] 2 {1 2} +[1] 0 +[0&1] 1 +[!0&1] 2 {0} State: 2 [!1] 0 [0&!1] 1 -[!0&!1] 2 -[!0&!1] 3 -State: 3 -[!0&!1] 3 {0} +[!0&!1] 2 {0} --END-- HOA: v1 States: 3 Start: 0 AP: 2 "a" "b" -acc-name: generalized-Buchi 2 -Acceptance: 2 Inf(0)&Inf(1) +acc-name: Buchi +Acceptance: 1 Inf(0) properties: trans-labels explicit-labels trans-acc --BODY-- State: 0 -[t] 0 {1} -[0] 1 {1} -[!0] 2 {0 1} +[t] 0 +[0] 1 +[!0] 2 {0} State: 1 -[1] 0 {1} -[0&1] 1 {0 1} -[!0&1] 2 {0 1} +[1] 0 +[0&1] 1 {0} +[!0&1] 2 {0} State: 2 [!1] 0 -[0&!1] 1 {0 1} -[!0&!1] 2 {0 1} +[0&!1] 1 {0} +[!0&!1] 2 {0} --END-- HOA: v1 States: 1 @@ -842,25 +840,23 @@ HOA: v1 States: 4 Start: 0 AP: 2 "b" "c" -acc-name: generalized-Buchi 2 -Acceptance: 2 Inf(0)&Inf(1) +acc-name: Buchi +Acceptance: 1 Inf(0) properties: trans-labels explicit-labels trans-acc --BODY-- State: 0 -[!0] 0 -[!0] 1 -[0] 0 -[0] 1 -[0&!1] 2 -[0&1] 3 +[t] 0 +[0&!1] 1 +[0&1] 2 +[!0] 3 State: 1 -[!0] 1 {0 1} +[!0 | !1] 1 {0} +[0&1] 2 State: 2 -[!0 | !1] 2 {0 1} -[0&1] 3 {0} +[!1] 1 {0} +[1] 2 State: 3 -[!1] 2 {0 1} -[1] 3 {0} +[!0] 3 {0} --END-- HOA: v1 States: 6 @@ -912,7 +908,7 @@ State: 2 {0} [!1] 2 --END-- HOA: v1 -States: 4 +States: 3 Start: 0 AP: 2 "a" "b" acc-name: Buchi @@ -930,10 +926,7 @@ State: 1 State: 2 [!1] 0 [0&!1] 1 -[!0&!1] 2 -[!0&!1] 3 -State: 3 -[!0&!1] 3 {0} +[!0&!1] 2 {0} --END-- HOA: v1 States: 3 diff --git a/tests/python/automata.ipynb b/tests/python/automata.ipynb index ded6bcc4e..f0b95a995 100644 --- a/tests/python/automata.ipynb +++ b/tests/python/automata.ipynb @@ -178,7 +178,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f5bd494e1b0> >" + " *' at 0x7f1940090f00> >" ] }, "execution_count": 2, @@ -657,7 +657,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f5bd494e090> >" + " *' at 0x7f1940108e10> >" ] }, "execution_count": 6, @@ -733,7 +733,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f5bd494e7e0> >" + " *' at 0x7f1940108870> >" ] }, "execution_count": 7, @@ -816,7 +816,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f5bd494eae0> >" + " *' at 0x7f1940108ab0> >" ] }, "execution_count": 8, @@ -1349,7 +1349,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f5bd494ede0> >" + " *' at 0x7f194009f600> >" ] }, "execution_count": 12, @@ -1463,7 +1463,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f5bd494e630> >" + " *' at 0x7f19401080f0> >" ] }, "execution_count": 13, @@ -1594,7 +1594,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f5bd49052d0> >" + " *' at 0x7f19400ad270> >" ] }, "execution_count": 14, @@ -1816,7 +1816,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f5bd4905cf0> >" + " *' at 0x7f19400b1480> >" ] }, "metadata": {}, @@ -1831,174 +1831,178 @@ "\n", "\n", - "\n", - "\n", - "\n", - "Inf(\n", - "⓿\n", - ") | (Inf(\n", - "❶\n", - ")&Inf(\n", - "❷\n", - "))\n", - "[Fin-less 3]\n", + "\n", + "\n", + "\n", + "Inf(\n", + "⓿\n", + ")\n", + "[Büchi]\n", "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "1\n", - "❷\n", + "\n", + "\n", + "1\n", "\n", "\n", "\n", "1\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "a\n", - "❶\n", - "❷\n", + "\n", + "\n", + "a\n", + "⓿\n", "\n", "\n", "\n", "2\n", - "\n", - "2\n", + "\n", + "2\n", "\n", "\n", "\n", "0->2\n", - "\n", - "\n", - "!a\n", - "❷\n", + "\n", + "\n", + "!a\n", "\n", "\n", "\n", "3\n", - "\n", - "3\n", + "\n", + "3\n", "\n", "\n", "\n", "0->3\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "1\n", "\n", "\n", "\n", "1->0\n", - "\n", - "\n", - "b\n", - "❷\n", + "\n", + "\n", + "b\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "a & b\n", - "❷\n", + "\n", + "\n", + "a & b\n", "\n", "\n", "\n", "1->2\n", - "\n", - "\n", - "!a & b\n", - "❶\n", - "❷\n", + "\n", + "\n", + "!a & b\n", + "⓿\n", "\n", "\n", "\n", "1->3\n", - "\n", - "\n", - "b\n", + "\n", + "\n", + "b\n", "\n", "\n", "\n", "4\n", - "\n", - "4\n", + "\n", + "4\n", "\n", "\n", "\n", "1->4\n", - "\n", - "\n", - "a & b\n", + "\n", + "\n", + "a & b\n", "\n", "\n", "\n", "2->0\n", - "\n", - "\n", - "!b\n", + "\n", + "\n", + "!b\n", "\n", "\n", "\n", "2->1\n", - "\n", - "\n", - "a & !b\n", + "\n", + "\n", + "a & !b\n", "\n", "\n", "\n", "2->2\n", - "\n", - "\n", - "!a & !b\n", + "\n", + "\n", + "!a & !b\n", + "\n", + "\n", + "\n", + "2->3\n", + "\n", + "\n", + "!b\n", + "\n", + "\n", + "\n", + "2->4\n", + "\n", + "\n", + "a & !b\n", "\n", "\n", - "\n", + "\n", "3->3\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "1\n", "\n", "\n", - "\n", + "\n", "4->3\n", - "\n", - "\n", - "b\n", + "\n", + "\n", + "b\n", "\n", "\n", - "\n", + "\n", "4->4\n", - "\n", - "\n", - "a & b\n", - "⓿\n", + "\n", + "\n", + "a & b\n", + "⓿\n", "\n", "\n", "\n" ], "text/plain": [ - " *' at 0x7f5bd4905cc0> >" + " *' at 0x7f19400b13f0> >" ] }, "metadata": {}, @@ -2013,150 +2017,171 @@ "\n", "\n", - "\n", - "\n", - "\n", - "Inf(\n", - "⓿\n", - ")\n", - "[Büchi]\n", + "\n", + "\n", + "\n", + "Inf(\n", + "⓿\n", + ")\n", + "[Büchi]\n", "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "1\n", "\n", "\n", "\n", "1\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "a\n", - "⓿\n", - "\n", - "\n", - "\n", - "1->0\n", - "\n", - "\n", - "b\n", - "\n", - "\n", - "\n", - "1->1\n", - "\n", - "\n", - "a & b\n", + "\n", + "\n", + "a\n", + "⓿\n", "\n", "\n", "\n", "2\n", - "\n", - "2\n", + "\n", + "2\n", + "\n", + "\n", + "\n", + "0->2\n", + "\n", + "\n", + "!a\n", + "\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + "b\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "a & b\n", "\n", "\n", - "\n", + "\n", "1->2\n", - "\n", - "\n", - "!a & b\n", - "⓿\n", + "\n", + "\n", + "!a & b\n", + "⓿\n", "\n", "\n", "\n", "3\n", - "\n", - "3\n", + "\n", + "3\n", "\n", "\n", - "\n", + "\n", "1->3\n", - "\n", - "\n", - "a & b\n", + "\n", + "\n", + "a & b\n", "\n", "\n", "\n", "4\n", - "\n", - "4\n", + "\n", + "4\n", "\n", "\n", - "\n", + "\n", "1->4\n", - "\n", - "\n", - "!b\n", + "\n", + "\n", + "!b\n", "\n", "\n", - "\n", + "\n", "2->0\n", - "\n", - "\n", - "!b\n", + "\n", + "\n", + "!b\n", "\n", "\n", - "\n", + "\n", "2->1\n", - "\n", - "\n", - "a & !b\n", + "\n", + "\n", + "a & !b\n", + "\n", + "\n", + "\n", + "2->2\n", + "\n", + "\n", + "!a & !b\n", + "\n", + "\n", + "\n", + "2->3\n", + "\n", + "\n", + "a & !b\n", "\n", "\n", - "\n", + "\n", "2->4\n", - "\n", - "\n", - "b\n", + "\n", + "\n", + "b\n", "\n", "\n", - "\n", + "\n", "3->3\n", - "\n", - "\n", - "a & b\n", - "⓿\n", + "\n", + "\n", + "a & b\n", + "⓿\n", "\n", "\n", - "\n", + "\n", "3->4\n", - "\n", - "\n", - "!a | !b\n", + "\n", + "\n", + "!a | !b\n", "\n", "\n", - "\n", + "\n", "4->4\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "1\n", "\n", "\n", "\n" ], "text/plain": [ - " *' at 0x7f5bd4905f90> >" + " *' at 0x7f19400b16f0> >" ] }, "metadata": {}, @@ -2171,11 +2196,11 @@ "\n", "\n", - "\n", - "\n", - "\n", - "[Büchi]\n", + "\n", + "\n", + "\n", + "[Büchi]\n", "\n", "\n", "\n", @@ -2220,91 +2245,91 @@ "\n", "\n", "2\n", - "\n", - "2\n", + "\n", + "2\n", "\n", "\n", "\n", "1->2\n", - "\n", - "\n", - "a & b\n", + "\n", + "\n", + "a & b\n", "\n", "\n", "\n", "3\n", - "\n", - "\n", - "3\n", + "\n", + "\n", + "3\n", "\n", "\n", "\n", "1->3\n", - "\n", - "\n", - "!a & b\n", + "\n", + "\n", + "!a & b\n", "\n", "\n", "\n", "4\n", - "\n", - "\n", - "4\n", + "\n", + "\n", + "4\n", "\n", "\n", "\n", "1->4\n", - "\n", - "\n", - "a & b\n", + "\n", + "\n", + "a & b\n", "\n", "\n", "\n", "2->2\n", - "\n", - "\n", - "a & b\n", + "\n", + "\n", + "a & b\n", "\n", "\n", "\n", "2->3\n", - "\n", - "\n", - "!a & b\n", - "\n", - "\n", - "\n", - "2->4\n", - "\n", - "\n", - "a & b\n", + "\n", + "\n", + "!a & b\n", "\n", "\n", - "\n", + "\n", "3->0\n", - "\n", + "\n", "\n", - "!b\n", + "!b\n", "\n", "\n", - "\n", + "\n", "3->2\n", - "\n", - "\n", - "a & !b\n", + "\n", + "\n", + "a & !b\n", + "\n", + "\n", + "\n", + "3->4\n", + "\n", + "\n", + "a & !b\n", "\n", "\n", "\n", "4->4\n", - "\n", - "\n", - "a & b\n", + "\n", + "\n", + "a & b\n", "\n", "\n", "\n" ], "text/plain": [ - " *' at 0x7f5bd4905ae0> >" + " *' at 0x7f19400b1420> >" ] }, "metadata": {}, @@ -2493,7 +2518,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f5bd4905720> >" + " *' at 0x7f19400b18a0> >" ] }, "execution_count": 19, @@ -2569,7 +2594,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f5bd4905a80> >" + " *' at 0x7f19400b1e70> >" ] }, "execution_count": 20, @@ -3119,7 +3144,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f5bd49055d0> >" + " *' at 0x7f19402232a0> >" ] }, "metadata": {}, @@ -3219,7 +3244,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f5bd4905ed0> >" + " *' at 0x7f1940108f60> >" ] }, "execution_count": 24, @@ -3292,7 +3317,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f5bd4905420> >" + " *' at 0x7f19400b1bd0> >" ] }, "execution_count": 25, @@ -3463,7 +3488,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f5bd494e990> >" + " *' at 0x7f19400b8b40> >" ] }, "execution_count": 27, @@ -3546,7 +3571,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f5bd49055d0> >" + " *' at 0x7f19402232a0> >" ] }, "metadata": {}, @@ -3611,7 +3636,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f5bd49055d0> >" + " *' at 0x7f19402232a0> >" ] }, "metadata": {}, @@ -3698,7 +3723,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f5bd49055d0> >" + " *' at 0x7f19402232a0> >" ] }, "execution_count": 29, @@ -3731,9 +3756,9 @@ "name": "python", "nbconvert_exporter": "python", "pygments_lexer": "ipython3", - "version": "3.8.5" + "version": "3.8.2" } }, "nbformat": 4, - "nbformat_minor": 2 + "nbformat_minor": 4 } diff --git a/tests/python/remfin.py b/tests/python/remfin.py index 4cede285c..7eb9ab4d2 100644 --- a/tests/python/remfin.py +++ b/tests/python/remfin.py @@ -92,4 +92,4 @@ State: 2 """) b = spot.remove_fin(a) size = (b.num_states(), b.num_edges()) -assert size == (5, 15); +assert size == (5, 17); diff --git a/tests/python/simplacc.py b/tests/python/simplacc.py index a6bcc29ae..e742d69a4 100644 --- a/tests/python/simplacc.py +++ b/tests/python/simplacc.py @@ -60,6 +60,11 @@ 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-- +/* Issue #406 */ +HOA: v1 States: 2 Start: 0 AP: 2 "p0" "p1" Acceptance: 4 +(Fin(3) & (Inf(1) | Fin(0))) | (Inf(0)&Inf(2)&Inf(3)) properties: trans-labels +explicit-labels trans-acc deterministic --BODY-- State: 0 [0&!1] 0 {2 3} +[!0&!1] 1 {0 1} State: 1 [!0&!1] 0 {0 1} [0&1] 1 {1 2} --END-- """)) res = [] @@ -90,8 +95,10 @@ 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)', + 'Fin(0)', + 'Inf(0)', + '(Fin(0) & Inf(2)) | Fin(1)', + '(Inf(0) | Fin(2)) & Inf(1)', + '(Fin(2) & (Inf(1) | Fin(0))) | (Inf(0)&Inf(2))', + '(Inf(2) | (Fin(1) & Inf(0))) & (Fin(0)|Fin(2))', ]