From 0c4b701630624fa811fb1ee2353a0f42d229688a Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Tue, 28 Jul 2020 22:09:33 +0200 Subject: [PATCH] improve acceptance simplifications using useless colors This fixes issue #418. * spot/twa/acc.cc, spot/twa/acc.hh (acc_cond::acc_code::useless_colors_patterns): New method to detect patterns of colors allowing other colors to be added or removed at will. * spot/twaalgos/cleanacc.cc (simplify_acceptance_here): Use the above patterns to remove some useless colors from transitions and hope that this can help simplify the acceptance condition. * spot/twaalgos/degen.cc (propagate_marks_vector): Use the pattern to add more colors. * tests/core/ltl2tgba2.test: Add the test case from issue #418. * tests/core/ltl2dstar4.test, tests/core/satmin3.test, tests/core/sccdot.test, tests/core/sim3.test, tests/python/automata.ipynb, tests/python/decompose.ipynb, tests/python/merge.py, tests/python/pdegen.py, tests/python/remfin.py, tests/python/toparity.py, tests/python/tra2tba.py: Adjust all test cases. * NEWS: Mention this new feature. --- NEWS | 7 ++ spot/twa/acc.cc | 75 ++++++++++++++ spot/twa/acc.hh | 14 +++ spot/twaalgos/cleanacc.cc | 30 +++++- spot/twaalgos/degen.cc | 12 ++- tests/core/ltl2dstar4.test | 2 +- tests/core/ltl2tgba2.test | 4 +- tests/core/satmin3.test | 53 +++++----- tests/core/sccdot.test | 22 ++-- tests/core/sim3.test | 29 ++---- tests/python/automata.ipynb | 190 ++++++++++++++++------------------- tests/python/decompose.ipynb | 166 +++++++++++++++--------------- tests/python/merge.py | 69 +++++++------ tests/python/pdegen.py | 2 +- tests/python/remfin.py | 2 +- tests/python/toparity.py | 10 +- tests/python/tra2tba.py | 12 ++- 17 files changed, 412 insertions(+), 287 deletions(-) diff --git a/NEWS b/NEWS index 818797506..9e7c0c22e 100644 --- a/NEWS +++ b/NEWS @@ -56,6 +56,13 @@ New in spot 2.9.3.dev (not yet released) the form Inf(x)&Inf(y) or Fin(x)|Fin(y) when the presence of x always implies that of y. (Issue #406.) + - simplifiy_acceptance_here() and propagate_marks_here() learned to + use some patterns of the acceptance condition to remove or add + (depending on the function) colors on edges. As an example, with + a condition such as Inf(0) | Fin(1), an edge labeled by {0,1} can + be simplied to {0}, but the oppose rewriting can be useful as + well. (Issue #418.) + Bugs fixed: - Handle xor and <-> in a more natural way when translating diff --git a/spot/twa/acc.cc b/spot/twa/acc.cc index 0a7fde252..852a4a10d 100644 --- a/spot/twa/acc.cc +++ b/spot/twa/acc.cc @@ -1326,6 +1326,81 @@ namespace spot return rescode; } + namespace + { + static acc_cond::mark_t + gather_used_colors(const acc_cond::acc_word* pos) + { + acc_cond::mark_t res{}; + auto start = pos - pos->sub.size; + do + { + switch (pos->sub.op) + { + case acc_cond::acc_op::And: + case acc_cond::acc_op::Or: + --pos; + break; + case acc_cond::acc_op::Fin: + case acc_cond::acc_op::Inf: + case acc_cond::acc_op::FinNeg: + case acc_cond::acc_op::InfNeg: + res |= pos[-1].mark; + pos -= 2; + break; + } + } + while (pos > start); + return res; + } + } + + std::vector> + acc_cond::acc_code::useless_colors_patterns() const + { + // [({y₁,y₂,...,yₙ},{x₁,x₂,...,xₙ}),...] + std::vector> + patterns; + acc_cond::mark_t used_once = used_once_sets(); + if (!used_once) + return patterns; + auto pos = &back(); + auto end = &front(); + while (pos > end) + { + switch (pos->sub.op) + { + case acc_cond::acc_op::And: + case acc_cond::acc_op::Or: + { + auto expect = pos->sub.op == acc_cond::acc_op::Or ? + acc_cond::acc_op::Inf : acc_cond::acc_op::Fin; + for (auto p = pos - 1, pe = pos - pos->sub.size; + p >= pe; p -= p->sub.size + 1) + if (p->sub.op == expect) + { + acc_cond::mark_t rem{}; + for (auto q = pos - 1; q >= pe; q -= q->sub.size + 1) + if (p != q) + rem |= gather_used_colors(q); + rem &= used_once; + if (rem) + patterns.emplace_back(p[-1].mark, rem); + } + --pos; + break; + } + case acc_cond::acc_op::Fin: + case acc_cond::acc_op::Inf: + case acc_cond::acc_op::FinNeg: + case acc_cond::acc_op::InfNeg: + pos -= 2; + break; + } + } + return patterns; + } + bool acc_cond::acc_code::is_parity_max_equiv(std::vector& permut, unsigned new_color, diff --git a/spot/twa/acc.hh b/spot/twa/acc.hh index 7ca440fd0..c04e46d99 100644 --- a/spot/twa/acc.hh +++ b/spot/twa/acc.hh @@ -1330,6 +1330,20 @@ namespace spot /// \brief Return the set of sets appearing in the condition. acc_cond::mark_t used_sets() const; + /// \brief Find patterns of useless colors. + /// + /// If any subformula of the acceptance condition looks like + /// (Inf(y₁)&Inf(y₂)&...&Inf(yₙ)) | f(x₁,...,xₙ) + /// or (Fin(y₁)|Fin(y₂)|...|Fin(yₙ)) & f(x₁,...,xₙ) + /// then for each transition with all colors {y₁,y₂,...,yₙ} we + /// can add or remove all the xᵢ that are used only once in + /// the formula. + /// + /// This method returns a vector of pairs: + /// [({y₁,y₂,...,yₙ},{x₁,x₂,...,xₙ}),...] + std::vector> + useless_colors_patterns() const; + /// \brief Return the sets that appears only once in the /// acceptance. /// diff --git a/spot/twaalgos/cleanacc.cc b/spot/twaalgos/cleanacc.cc index 93064a408..e1cfed932 100644 --- a/spot/twaalgos/cleanacc.cc +++ b/spot/twaalgos/cleanacc.cc @@ -617,6 +617,33 @@ namespace spot } return aut; } + + + // If any subformula of the acceptance condition looks like + // (Inf(y₁)&Inf(y₂)&...&Inf(yₙ)) | f(x₁,...,xₙ) + // then for each transition with all colors {y₁,y₂,...,yₙ} we + // can remove all the xᵢ that are used only once in the formula. + // + // See also issue #418. + static bool + remove_useless_colors_from_edges_here(twa_graph_ptr aut) + { + // [({y₁,y₂,...,yₙ},{x₁,x₂,...,xₙ}),...] + auto patterns = aut->get_acceptance().useless_colors_patterns(); + if (patterns.empty()) + return false; + + bool changed = false; + for (auto& e: aut->edges()) + for (auto& p: patterns) + if (p.first.subset(e.acc)) + if (auto nacc = e.acc - p.second; nacc != e.acc) + { + e.acc = nacc; + changed = true; + } + return changed; + } } @@ -632,7 +659,8 @@ namespace spot aut->set_acceptance(aut->acc().unit_propagation()); simplify_complementary_marks_here(aut); fuse_marks_here(aut); - if (old == aut->get_acceptance()) + bool changed = remove_useless_colors_from_edges_here(aut); + if (!changed && old == aut->get_acceptance()) break; } cleanup_acceptance_here(aut, true); diff --git a/spot/twaalgos/degen.cc b/spot/twaalgos/degen.cc index 1a594b9c7..a2fa0ce26 100644 --- a/spot/twaalgos/degen.cc +++ b/spot/twaalgos/degen.cc @@ -1108,13 +1108,23 @@ namespace spot else si = new scc_info(aut); + unsigned ns = aut->num_states(); acc_cond::mark_t allm = aut->acc().all_sets(); unsigned es = aut->edge_vector().size(); + + auto patterns = aut->get_acceptance().useless_colors_patterns(); std::vector marks(es, acc_cond::mark_t{}); const auto& edges = aut->edge_vector(); for (unsigned e = 1; e < es; ++e) - marks[e] = edges[e].acc; + { + acc_cond::mark_t m = edges[e].acc; + // Add as many useless colors as possible. + for (auto& p: patterns) + if (p.first.subset(m)) + m |= p.second; + marks[e] = m; + } std::vector common_in(ns, allm); std::vector common_out(ns, allm); diff --git a/tests/core/ltl2dstar4.test b/tests/core/ltl2dstar4.test index dfa004805..55eaf6dbb 100755 --- a/tests/core/ltl2dstar4.test +++ b/tests/core/ltl2dstar4.test @@ -34,7 +34,7 @@ ltlfilt -f '(GFa -> GFb) & (GFc -> GFd)' -l | ltl2dstar --ltl2nba=spin:ltl2tgba@-s $STR - - | autfilt --tgba --stats '%S %E %A %s %e %t %a %d' | tee out -test "`cat out`" = '9 144 4 18 98 202 2 0' +test "`cat out`" = '9 144 4 16 92 186 2 0' ltlfilt -f '(GFa -> GFb) & (GFc -> GFd)' -l | ltl2dstar --ltl2nba=spin:ltl2tgba@-s $STR - - | diff --git a/tests/core/ltl2tgba2.test b/tests/core/ltl2tgba2.test index 227ee5b99..32ac32823 100755 --- a/tests/core/ltl2tgba2.test +++ b/tests/core/ltl2tgba2.test @@ -471,4 +471,6 @@ test "4,1" = `ltl2tgba -D -x wdba-minimize=2 "$f" --stats=%s,%d` test "4,0" = `ltl2tgba -D -x wdba-minimize=0 "$f" --stats=%s,%d` test "4,1" = `ltl2tgba -D --med "$f" --stats=%s,%d` -: +# Issue #418. +f='(G!a | G!b | G!c) & (FG!a2 | GFb2 | GFc2) & (GFc2 | FG!b2 | GFa2)' +test 28 = `ltl2tgba -D -G -S --stats=%s "$f"` diff --git a/tests/core/satmin3.test b/tests/core/satmin3.test index 2a0a9c95a..f9fcb4403 100755 --- a/tests/core/satmin3.test +++ b/tests/core/satmin3.test @@ -1,6 +1,6 @@ #!/bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2017, 2019 Laboratoire de Recherche et Développement +# Copyright (C) 2017, 2019, 2020 Laboratoire de Recherche et Développement # de l'Epita (LRDE). # # This file is part of Spot, a model checking library. @@ -24,37 +24,36 @@ set -e # Make sure the SPOT_SATSOLVER envar works. -# DRA produced by ltl2dstar for GFp0 -> GFp1, but manually modified -# so that simulation-based reduction do not reduce it to 1 state right away. +# DRA for GFp0 -> GFp1 produced using the SAT-based synthesis (i.e., +# "minimization with fixed number of states"). We used to take the +# output of ltl2dstar, unfortunately our preprocessing reduced that to +# one state right away, even after some manual touches. + cat >test.hoa <output -test `cat output` = 4 +test `cat output` = 3 SPOT_SATSOLVER='this-does-not-exist %I %O' \ autfilt --sat-minimize test.hoa --stats=%s 2>err && exit diff --git a/tests/core/sccdot.test b/tests/core/sccdot.test index 96e75dbe6..1c3049cd7 100755 --- a/tests/core/sccdot.test +++ b/tests/core/sccdot.test @@ -156,7 +156,7 @@ HOA: v1 States: 8 Start: 0 AP: 2 "a" "b" -Acceptance: 3 (Inf(0)&Inf(1)) & Fin(2) +Acceptance: 2 Inf(0) & Fin(1) properties: trans-labels explicit-labels trans-acc --BODY-- State: 0 @@ -165,24 +165,24 @@ State: 0 State: 1 [1] 4 State: 2 -[0&1] 0 {0 1} +[0&1] 0 {0} State: 3 [1] 1 -[!1] 3 {2} +[!1] 3 {1} State: 4 -[!0&1] 4 {0 1} -[0&1] 4 {0 2} +[!0&1] 4 {0} +[0&1] 4 {1} [t] 5 State: 5 -[0&1] 5 {0 1} -[!0&1] 5 {0 2} +[0&1] 5 {0} +[!0&1] 5 {1} [t] 6 State: 6 -[!0&1] 6 {0 2} -[0&1] 7 {0 1} +[!0&1] 6 {1} +[0&1] 7 {0} State: 7 -[!0&1] 6 {0 1} -[0&1] 7 {0 2} +[!0&1] 6 {0} +[0&1] 7 {1} --END-- EOF diff expected.hoa out.hoa diff --git a/tests/core/sim3.test b/tests/core/sim3.test index c4375c646..57959174a 100755 --- a/tests/core/sim3.test +++ b/tests/core/sim3.test @@ -1,6 +1,6 @@ #! /bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2015, 2018, 2019 Laboratoire de Recherche et Développement +# Copyright (C) 2015, 2018, 2019, 2020 Laboratoire de Recherche et Développement # de l'Epita (LRDE). # # This file is part of Spot, a model checking library. @@ -52,7 +52,7 @@ test "`autfilt --small input --stats=%S,%s`" = 7,1 autfilt -S --high --small input -H > out cat >expected <\n" ], "text/plain": [ - " *' at 0x7f65f48a3f90> >" + " *' at 0x7f33f419a180> >" ] }, "execution_count": 2, @@ -657,7 +657,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f65f4901f90> >" + " *' at 0x7f33f419adb0> >" ] }, "execution_count": 6, @@ -733,7 +733,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f65f48b2540> >" + " *' at 0x7f33f41614b0> >" ] }, "execution_count": 7, @@ -816,7 +816,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f65f60e46c0> >" + " *' at 0x7f33f41613f0> >" ] }, "execution_count": 8, @@ -1349,7 +1349,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f65f48b2660> >" + " *' at 0x7f33f4161ba0> >" ] }, "execution_count": 12, @@ -1463,7 +1463,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f65f48c1180> >" + " *' at 0x7f33f416c300> >" ] }, "execution_count": 13, @@ -1594,7 +1594,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f65f48c15d0> >" + " *' at 0x7f33f416c5d0> >" ] }, "execution_count": 14, @@ -1816,7 +1816,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f65f48c66f0> >" + " *' at 0x7f33f41747b0> >" ] }, "metadata": {}, @@ -1831,164 +1831,150 @@ "\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", + "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", + "!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", + "b\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "a & b\n", + "\n", + "\n", + "a & b\n", "\n", "\n", "\n", "1->2\n", - "\n", - "\n", - "!a & b\n", - "⓿\n", - "\n", - "\n", - "\n", - "1->3\n", - "\n", - "\n", - "b\n", + "\n", + "\n", + "!a & b\n", + "⓿\n", "\n", "\n", "\n", "4\n", - "\n", - "4\n", + "\n", + "4\n", "\n", "\n", - "\n", + "\n", "1->4\n", - "\n", - "\n", - "a & b\n", + "\n", + "\n", + "a & 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", + "\n", "2->2\n", - "\n", - "\n", - "!a & !b\n", + "\n", + "\n", + "!a & !b\n", "\n", "\n", - "\n", + "\n", "3->3\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "\n", - "4->3\n", - "\n", - "\n", - "b\n", + "\n", + "\n", + "1\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 0x7f65f48c6660> >" + " *' at 0x7f33f4174720> >" ] }, "metadata": {}, @@ -2146,7 +2132,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f65f48c6a20> >" + " *' at 0x7f33f4174c30> >" ] }, "metadata": {}, @@ -2294,7 +2280,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f65f48c6960> >" + " *' at 0x7f33f4174b10> >" ] }, "metadata": {}, @@ -2483,7 +2469,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f65f48c6cc0> >" + " *' at 0x7f33f41748a0> >" ] }, "execution_count": 19, @@ -2559,7 +2545,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f65f48ca1b0> >" + " *' at 0x7f33f4179450> >" ] }, "execution_count": 20, @@ -3109,7 +3095,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f65f48c1060> >" + " *' at 0x7f33f416c9f0> >" ] }, "metadata": {}, @@ -3209,7 +3195,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f65f48c1900> >" + " *' at 0x7f33f4174300> >" ] }, "execution_count": 24, @@ -3282,7 +3268,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f65f4901900> >" + " *' at 0x7f33f416c510> >" ] }, "execution_count": 25, @@ -3453,7 +3439,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f65f48c6060> >" + " *' at 0x7f33f416ccf0> >" ] }, "execution_count": 27, @@ -3536,7 +3522,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f65f48c1060> >" + " *' at 0x7f33f416c9f0> >" ] }, "metadata": {}, @@ -3601,7 +3587,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f65f48c1060> >" + " *' at 0x7f33f416c9f0> >" ] }, "metadata": {}, @@ -3688,7 +3674,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f65f48c1060> >" + " *' at 0x7f33f416c9f0> >" ] }, "execution_count": 29, diff --git a/tests/python/decompose.ipynb b/tests/python/decompose.ipynb index 15c98ec7a..e827ff3f2 100644 --- a/tests/python/decompose.ipynb +++ b/tests/python/decompose.ipynb @@ -200,7 +200,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f2568c8f9f0> >" + " *' at 0x7fbb000ab150> >" ] }, "execution_count": 2, @@ -330,7 +330,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f2568c93360> >" + " *' at 0x7fbb015474e0> >" ] }, "execution_count": 3, @@ -489,7 +489,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f2568c9a9c0> >" + " *' at 0x7fbb000ab360> >" ] }, "execution_count": 4, @@ -587,7 +587,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f2568c9ac00> >" + " *' at 0x7fbb000ab840> >" ] }, "execution_count": 5, @@ -669,7 +669,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f2569d3d270> >" + " *' at 0x7fbb000abb40> >" ] }, "execution_count": 6, @@ -796,7 +796,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f2568c9ae40> >" + " *' at 0x7fbb000abd50> >" ] }, "metadata": {}, @@ -941,7 +941,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f2569d3d9c0> >" + " *' at 0x7fbb000abf00> >" ] }, "metadata": {}, @@ -1109,7 +1109,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f2568c9a7e0> >" + " *' at 0x7fbb00d0fd80> >" ] }, "metadata": {}, @@ -1512,7 +1512,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f2568c93990> >" + " *' at 0x7fbb000ab390> >" ] }, "execution_count": 8, @@ -1942,7 +1942,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f2568ca0030> >" + " *' at 0x7fbb00064e40> >" ] }, "metadata": {}, @@ -2174,7 +2174,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f25694cf6f0> >" + " *' at 0x7fbb00064e10> >" ] }, "metadata": {}, @@ -2384,7 +2384,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f2568c93240> >" + " *' at 0x7fbb000abed0> >" ] }, "metadata": {}, @@ -2772,7 +2772,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f2568c9aa80> >" + " *' at 0x7fbb00cd01e0> >" ] }, "execution_count": 10, @@ -2793,7 +2793,7 @@ }, { "cell_type": "code", - "execution_count": 11, + "execution_count": 12, "metadata": {}, "outputs": [ { @@ -2933,7 +2933,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f2568ca7cf0> >" + " *' at 0x7fbb000798a0> >" ] }, "metadata": {}, @@ -3072,7 +3072,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f2568c9adb0> >" + " *' at 0x7fbb00079660> >" ] }, "metadata": {}, @@ -3103,7 +3103,7 @@ "[parity min even 3]\n", "\n", "cluster_0\n", - "\n", + "\n", "\n", "\n", "cluster_1\n", @@ -3139,23 +3139,22 @@ "\n", "\n", "1\n", - "\n", - "1\n", - "⓿\n", - "❶\n", + "\n", + "1\n", + "⓿\n", "\n", "\n", "\n", "0->1\n", - "\n", - "\n", + "\n", + "\n", "a & b & !c\n", "\n", "\n", "\n", "0->1\n", - "\n", - "\n", + "\n", + "\n", "!a & !c\n", "\n", "\n", @@ -3168,64 +3167,64 @@ "\n", "\n", "2->1\n", - "\n", - "\n", + "\n", + "\n", "!a & !c\n", "\n", "\n", "\n", "1->2\n", - "\n", - "\n", + "\n", + "\n", "a & !b & !c\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", + "\n", + "\n", "!a & !c\n", "\n", "\n", "\n", "3\n", - "\n", - "3\n", - "❷\n", + "\n", + "3\n", + "❷\n", "\n", "\n", "\n", "1->3\n", - "\n", - "\n", - "a & b & !c\n", + "\n", + "\n", + "a & b & !c\n", "\n", "\n", "\n", "3->2\n", - "\n", + "\n", "\n", "a & !b & !c\n", "\n", "\n", "\n", "3->1\n", - "\n", - "\n", - "!a & !c\n", + "\n", + "\n", + "!a & !c\n", "\n", "\n", "\n", "3->3\n", - "\n", - "\n", - "a & b & !c\n", + "\n", + "\n", + "a & b & !c\n", "\n", "\n", "\n" ], "text/plain": [ - " *' at 0x7f2568ca70f0> >" + " *' at 0x7fbb00079750> >" ] }, "metadata": {}, @@ -3253,7 +3252,7 @@ }, { "cell_type": "code", - "execution_count": 12, + "execution_count": 13, "metadata": {}, "outputs": [ { @@ -3578,10 +3577,10 @@ "\n" ], "text/plain": [ - " *' at 0x7f2568ca7ea0> >" + " *' at 0x7fbb00d0f0f0> >" ] }, - "execution_count": 12, + "execution_count": 13, "metadata": {}, "output_type": "execute_result" } @@ -3642,7 +3641,7 @@ }, { "cell_type": "code", - "execution_count": 13, + "execution_count": 14, "metadata": {}, "outputs": [ { @@ -3961,7 +3960,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f2568cae210> >" + " *' at 0x7fbb00079420> >" ] }, "metadata": {}, @@ -4138,7 +4137,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f2568ca09c0> >" + " *' at 0x7fbb01538de0> >" ] }, "metadata": {}, @@ -4296,7 +4295,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f2568ca0d50> >" + " *' at 0x7fbb00d0f360> >" ] }, "metadata": {}, @@ -4321,7 +4320,7 @@ }, { "cell_type": "code", - "execution_count": 14, + "execution_count": 15, "metadata": {}, "outputs": [ { @@ -4645,10 +4644,10 @@ "\n" ], "text/plain": [ - " *' at 0x7f2568ca0a20> >" + " *' at 0x7fbb000abd50> >" ] }, - "execution_count": 14, + "execution_count": 15, "metadata": {}, "output_type": "execute_result" } @@ -4674,7 +4673,7 @@ }, { "cell_type": "code", - "execution_count": 15, + "execution_count": 16, "metadata": {}, "outputs": [ { @@ -4768,10 +4767,10 @@ "\n" ], "text/plain": [ - " *' at 0x7f2568cae690> >" + " *' at 0x7fbb00079330> >" ] }, - "execution_count": 15, + "execution_count": 16, "metadata": {}, "output_type": "execute_result" } @@ -4782,7 +4781,7 @@ }, { "cell_type": "code", - "execution_count": 16, + "execution_count": 17, "metadata": {}, "outputs": [], "source": [ @@ -4792,7 +4791,7 @@ }, { "cell_type": "code", - "execution_count": 17, + "execution_count": 18, "metadata": {}, "outputs": [ { @@ -4866,7 +4865,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f2568ca7db0> >" + " *' at 0x7fbb00079660> >" ] }, "metadata": {}, @@ -4942,7 +4941,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f2568ca7cc0> >" + " *' at 0x7fbb000abea0> >" ] }, "metadata": {}, @@ -4963,7 +4962,7 @@ }, { "cell_type": "code", - "execution_count": 18, + "execution_count": 19, "metadata": {}, "outputs": [ { @@ -5036,10 +5035,10 @@ "\n" ], "text/plain": [ - " *' at 0x7f2568cb4780> >" + " *' at 0x7fbb000791b0> >" ] }, - "execution_count": 18, + "execution_count": 19, "metadata": {}, "output_type": "execute_result" } @@ -5066,7 +5065,7 @@ }, { "cell_type": "code", - "execution_count": 19, + "execution_count": 20, "metadata": {}, "outputs": [ { @@ -5186,10 +5185,10 @@ "\n" ], "text/plain": [ - " *' at 0x7f2568cb4c00> >" + " *' at 0x7fbb00079300> >" ] }, - "execution_count": 19, + "execution_count": 20, "metadata": {}, "output_type": "execute_result" } @@ -5227,7 +5226,7 @@ }, { "cell_type": "code", - "execution_count": 20, + "execution_count": 21, "metadata": {}, "outputs": [ { @@ -5346,7 +5345,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f2568cc5c00> >" + " *' at 0x7fbb00079d50> >" ] }, "metadata": {}, @@ -5448,7 +5447,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f2568ca7030> >" + " *' at 0x7fbb000abcf0> >" ] }, "metadata": {}, @@ -5583,7 +5582,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f2568cc5b40> >" + " *' at 0x7fbb000abe70> >" ] }, "metadata": {}, @@ -5612,7 +5611,7 @@ }, { "cell_type": "code", - "execution_count": 21, + "execution_count": 22, "metadata": {}, "outputs": [ { @@ -5787,7 +5786,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f2568cc56c0> >" + " *' at 0x7fbb000ab930> >" ] }, "metadata": {}, @@ -5928,10 +5927,10 @@ "\n" ], "text/plain": [ - " *' at 0x7f2568cc5a20> >" + " *' at 0x7fbb00079db0> >" ] }, - "execution_count": 21, + "execution_count": 22, "metadata": {}, "output_type": "execute_result" } @@ -5954,7 +5953,7 @@ }, { "cell_type": "code", - "execution_count": 22, + "execution_count": 23, "metadata": {}, "outputs": [ { @@ -6031,10 +6030,10 @@ "\n" ], "text/plain": [ - " *' at 0x7f2568cba9f0> >" + " *' at 0x7fbb000792d0> >" ] }, - "execution_count": 22, + "execution_count": 23, "metadata": {}, "output_type": "execute_result" } @@ -6042,6 +6041,13 @@ "source": [ "spot.decompose_scc(si, 'a2')" ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [] } ], "metadata": { @@ -6060,7 +6066,7 @@ "name": "python", "nbconvert_exporter": "python", "pygments_lexer": "ipython3", - "version": "3.8.2" + "version": "3.8.5" } }, "nbformat": 4, diff --git a/tests/python/merge.py b/tests/python/merge.py index c69ec4028..c56d8f309 100644 --- a/tests/python/merge.py +++ b/tests/python/merge.py @@ -36,28 +36,28 @@ State: 1 State: 2 [1] 0 {2 3} --END--""") -spot.simplify_acceptance_here(aut) -hoa = aut.to_str('hoa') +out = spot.simplify_acceptance(aut) +hoa = out.to_str('hoa') assert hoa == """HOA: v1 States: 3 Start: 0 AP: 2 "a" "b" -acc-name: parity min even 2 -Acceptance: 2 Inf(0) | Fin(1) +acc-name: Buchi +Acceptance: 1 Inf(0) properties: trans-labels explicit-labels trans-acc --BODY-- State: 0 [0] 1 {0} State: 1 -[0] 1 {1} -[1] 2 {0 1} +[0] 1 +[1] 2 {0} State: 2 -[1] 0 {1} +[1] 0 --END--""" +assert spot.are_equivalent(out, aut) -aut = spot.automaton(""" -HOA: v1 +aut = spot.automaton("""HOA: v1 States: 3 Start: 0 AP: 2 "a" "b" @@ -79,17 +79,17 @@ assert hoa == """HOA: v1 States: 3 Start: 0 AP: 2 "a" "b" -acc-name: parity min even 2 -Acceptance: 2 Inf(0) | Fin(1) +acc-name: Buchi +Acceptance: 1 Inf(0) properties: trans-labels explicit-labels trans-acc --BODY-- State: 0 [0] 1 {0} State: 1 -[0] 1 {1} -[1] 2 {0 1} +[0] 1 +[1] 2 {0} State: 2 -[1] 0 {1} +[1] 0 --END--""" aut = spot.automaton(""" @@ -128,8 +128,7 @@ State: 2 [1] 0 --END--""" -aut = spot.automaton(""" -HOA: v1 +aut = spot.automaton("""HOA: v1 States: 3 Start: 0 AP: 2 "a" "b" @@ -158,10 +157,10 @@ properties: trans-labels explicit-labels trans-acc State: 0 [0] 1 State: 1 -[0] 1 {0 1} +[0] 1 {0} [1] 2 {1} State: 2 -[1] 0 {0 1} +[1] 0 {0} --END--""" aut = spot.automaton(""" @@ -355,7 +354,7 @@ State: 1 [0&!1] 0 [!0&1] 3 [0&1] 2 -State: 2 {0 1} +State: 2 {1} [!0&!1] 1 [0&!1] 0 [!0&1] 3 @@ -386,27 +385,29 @@ State: 2 [0] 2 {0 1 2} [!0] 1 {0} --END--""") -spot.simplify_acceptance_here(aut) -hoa = aut.to_str('hoa') +out = spot.simplify_acceptance(aut) +hoa = out.to_str('hoa') assert hoa == """HOA: v1 States: 3 Start: 0 AP: 2 "p0" "p1" -Acceptance: 3 (Fin(0) | Inf(1)) & Fin(2) +acc-name: co-Buchi +Acceptance: 1 Fin(0) properties: trans-labels explicit-labels trans-acc complete properties: deterministic --BODY-- State: 0 [0] 1 -[!0] 0 {2} +[!0] 0 {0} State: 1 -[0] 1 {1 2} +[0] 1 {0} [!0] 2 State: 2 -[0] 2 {0 1 2} +[0] 2 {0} [!0] 1 {0} --END--""" +assert spot.are_equivalent(out, aut) aut = spot.automaton("""HOA: v1 States: 4 @@ -448,14 +449,14 @@ State: 0 [!0&!1] 0 {0} [0] 3 State: 1 -[0] 0 {1 2 3} +[0] 0 {1 3} [!0] 3 {0 2} State: 2 [t] 1 {1 2} State: 3 [0&1] 0 {1} [0&!1] 3 {1 2} -[!0] 1 {2 3} +[!0] 1 {3} --END--""" aut = spot.automaton("""HOA: v1 @@ -668,24 +669,26 @@ State: 2 {1 2 3} [t] 1 --END-- """) -spot.simplify_acceptance_here(aut) -hoa = aut.to_str('hoa') +out = spot.simplify_acceptance(aut) +hoa = out.to_str('hoa') assert hoa == """HOA: v1 States: 3 Start: 0 AP: 2 "p0" "p1" -Acceptance: 3 (Fin(0) | Inf(1)) & (Fin(1) | Inf(2)) +acc-name: generalized-Buchi 2 +Acceptance: 2 Inf(0)&Inf(1) properties: trans-labels explicit-labels state-acc complete properties: deterministic --BODY-- -State: 0 {0 1} +State: 0 {0} [t] 2 -State: 1 {0 2} +State: 1 {1} [t] 2 -State: 2 {1 2} +State: 2 {0 1} [t] 1 --END--""" +assert spot.are_equivalent(out, aut) aut = spot.automaton("""HOA: v1 States: 2 diff --git a/tests/python/pdegen.py b/tests/python/pdegen.py index 760e30508..66c89b117 100644 --- a/tests/python/pdegen.py +++ b/tests/python/pdegen.py @@ -322,7 +322,7 @@ assert aut12c.num_states() == 9 aut12d = spot.partial_degeneralize(aut12, [0,1,3]) aut12e = spot.partial_degeneralize(aut12d, [0,1]) assert aut12e.equivalent_to(aut12) -assert aut12e.num_states() == 11 +assert aut12e.num_states() == 9 aut12f = spot.partial_degeneralize(aut12) assert aut12f.equivalent_to(aut12) diff --git a/tests/python/remfin.py b/tests/python/remfin.py index 4cede285c..20115a14f 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, 13); diff --git a/tests/python/toparity.py b/tests/python/toparity.py index 091292ffb..f8ce7dc1a 100644 --- a/tests/python/toparity.py +++ b/tests/python/toparity.py @@ -200,7 +200,7 @@ State: 13 [0&1] 5 [!0&!1] 10 {0 1 3 5} [0&!1] 13 {1 3} ---END--"""), [35, 28, 23, 30, 29, 25, 22]) +--END--"""), [35, 30, 23, 32, 31, 28, 22]) test(spot.automaton(""" HOA: v1 @@ -259,7 +259,7 @@ State: 3 [!0&1] 2 {1 4} [0&1] 3 {0} --END-- -"""), [80, 22, 80, 80, 80, 17, 10]) +"""), [80, 47, 104, 104, 102, 29, 6]) test(spot.automaton(""" HOA: v1 @@ -315,7 +315,7 @@ State: 1 [0&!1] 1 {2 3} [0&1] 1 {1 2 4} --END-- -"""), [11, 6, 3, 7, 7, 4, 3]) +"""), [11, 3, 2, 3, 3, 3, 2]) # Tests both the old and new version of to_parity @@ -346,7 +346,7 @@ explicit-labels trans-acc --BODY-- State: 0 [0&1] 2 {4 5} [0&1] 4 {0 4} p = spot.to_parity_old(a, True) assert p.num_states() == 22 assert spot.are_equivalent(a, p) -test(a, [8, 7, 8, 8, 6, 7, 6]) +test(a, [8, 6, 6, 6, 6, 6, 6]) # Force a few edges to false, to make sure to_parity() is OK with that. for e in a.out(2): @@ -360,7 +360,7 @@ for e in a.out(3): p = spot.to_parity_old(a, True) assert p.num_states() == 22 assert spot.are_equivalent(a, p) -test(a, [7, 6, 7, 7, 6, 6, 6]) +test(a, [7, 6, 6, 6, 6, 6, 6]) for f in spot.randltl(4, 400): d = spot.translate(f, "det", "G") diff --git a/tests/python/tra2tba.py b/tests/python/tra2tba.py index 59ce3ab63..c0efd6f0f 100644 --- a/tests/python/tra2tba.py +++ b/tests/python/tra2tba.py @@ -578,11 +578,15 @@ properties: trans-labels explicit-labels trans-acc complete properties: deterministic --BODY-- State: 0 -[!1] 0 {0} -[1] 1 +[0&1] 1 {0} +[0&!1] 0 {0} +[!0&1] 1 +[!0&!1] 0 {0} State: 1 -[!1] 0 {0} -[1] 1 {0} +[0&1] 1 {0} +[0&!1] 0 {0} +[!0&1] 1 {0} +[!0&!1] 0 {0} --END--""" res = spot.remove_fin(aut)