From fca6513604bc45b6d99f360d5a99f1659f892b68 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Mon, 19 Apr 2021 23:38:50 +0200 Subject: [PATCH] simulation: fix merging transiant SCCs This fixes #452, and also fix a bug related to transiant SCCs incorrectly merged in cosimulation: the source of the edges was updated without fixing the chaining of the edges. * spot/twaalgos/simulation.cc: Fix all the above. * tests/python/simstate.py: Add test case from issue #452. * tests/core/det.test, tests/core/ltlsynt.test, tests/core/satmin.test: Lower expected sizes. * tests/python/decompose.ipynb: Adjust for changed order. --- spot/twaalgos/simulation.cc | 49 +++++-- tests/core/det.test | 4 +- tests/core/ltlsynt.test | 4 +- tests/core/satmin.test | 8 +- tests/python/decompose.ipynb | 242 +++++++++++++++++------------------ tests/python/simstate.py | 38 ++++++ 6 files changed, 203 insertions(+), 142 deletions(-) diff --git a/spot/twaalgos/simulation.cc b/spot/twaalgos/simulation.cc index 9ed9739c3..066536638 100644 --- a/spot/twaalgos/simulation.cc +++ b/spot/twaalgos/simulation.cc @@ -550,16 +550,16 @@ namespace spot // All states in p.second have the same class, so just // pick the class of the first one first one. bdd src = previous_class_[p->second.front()]; + assert(gb->get_state(src.id()) == srcst); // Get the signature to derive successors. bdd sig = compute_sig(p->second.front()); + assert(signatures.size() == srcst); + signatures.push_back(sig); if (Cosimulation) sig = bdd_compose(sig, bddfalse, bdd_var(bdd_initial)); - assert(gb->get_state(src.id()) == srcst); - assert(signatures.size() == srcst); - signatures.push_back(bdd_exist(sig, all_proms_)); // Get all the variables in the signature. bdd sup_sig = bdd_support(sig); @@ -656,6 +656,7 @@ namespace spot } } + bool need_another_pass = false; // Attempt to merge trivial SCCs if (!record_implications_ && res->num_states() > 1) { @@ -664,7 +665,10 @@ namespace spot unsigned nstates = res->num_states(); std::vector redirect(nstates); std::iota(redirect.begin(), redirect.end(), 0); + for (unsigned s = 0; s < nstates; ++s) + signatures[s] = bdd_exist(signatures[s], all_proms_); bool changed = false; + bool unchanged = false; for (unsigned scc = 0; scc < nscc; ++scc) if (si.is_trivial(scc)) { @@ -676,8 +680,10 @@ namespace spot { changed = true; redirect[s] = i; - break; + goto if_changed; } + unchanged = true; + if_changed:; } if (changed) { @@ -688,16 +694,28 @@ namespace spot for (auto& e: res->edges()) e.dst = redirect[e.dst]; res->set_init_state(redirect[res->get_init_state_number()]); + if (Cosimulation) + // Fix chaining of edges with changed sources. + res->merge_edges(); + if (unchanged) + need_another_pass = true; } - } - // If we recorded implications for the determinization - // procedure, we should not remove unreachable states, as that - // will invalidate the contents of the IMPLICATIONS vector. - // It's OK not to purge the result, as the determinization - // will only explore the reachable part anyway. - if (!record_implications_) - res->purge_unreachable_states(); + // Remove unreachable states. + // In the case of co-simulation, changing the sources + // of edges, might have created dead states. + // + // If we recorded implications for the determinization + // procedure, we should not remove unreachable states, as + // that will invalidate the contents of the IMPLICATIONS + // vector. It's OK not to purge the result in that case, + // as the determinization will only explore the reachable + // part anyway. + if (Cosimulation) + res->purge_dead_states(); + else + res->purge_unreachable_states(); + } // Push the common incoming sets to the outgoing edges. // Doing so cancels the preprocessing we did in the other @@ -751,7 +769,12 @@ namespace spot res->prop_universal(true); if (Sba) res->prop_state_acc(true); - return res; + + if (!need_another_pass) + return res; + + direct_simulation sim(res); + return sim.run(); } diff --git a/tests/core/det.test b/tests/core/det.test index 7f4fe1eea..4c24b14b6 100755 --- a/tests/core/det.test +++ b/tests/core/det.test @@ -1,6 +1,6 @@ #!/bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2013-2020 Laboratoire de Recherche et Développement de +# Copyright (C) 2013-2021 Laboratoire de Recherche et Développement de # l'Epita (LRDE). # # This file is part of Spot, a model checking library. @@ -42,7 +42,7 @@ cat >formulas <<'EOF' 1,9,X(a R ((!b & F!c) M X!a)) 1,2,XG!a R Fb 1,4,GFc | (a & Fb) -1,6,X(a R (Fb R F!b)) +1,4,X(a R (Fb R F!b)) 1,1,G(Xa M Fa) 1,3,X(Gb | GFa) 1,9,X(Gc | XG((b & Ga) | (!b & F!a))) diff --git a/tests/core/ltlsynt.test b/tests/core/ltlsynt.test index 9fd0c9a4d..4cd48ce90 100644 --- a/tests/core/ltlsynt.test +++ b/tests/core/ltlsynt.test @@ -1,6 +1,6 @@ #! /bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2017, 2019, 2020 Laboratoire de Recherche et +# Copyright (C) 2017, 2019-2021 Laboratoire de Recherche et # Développement de l'Epita (LRDE). # # This file is part of Spot, a model checking library. @@ -376,6 +376,6 @@ diff out exp f='Fp0 U XX((p0 & F!p1) | (!p0 & Gp1))' ltlsynt --verbose --algo=ps --outs=p1 --ins=p0 -f "$f" 2>err -grep 'DPA has 14 states' err +grep 'DPA has 13 states' err ltlsynt --verbose -x wdba-minimize=1 --algo=ps --outs=p1 --ins=p0 -f "$f" 2>err grep 'DPA has 12 states' err diff --git a/tests/core/satmin.test b/tests/core/satmin.test index 71ca9ee54..325d2ef63 100755 --- a/tests/core/satmin.test +++ b/tests/core/satmin.test @@ -1,7 +1,7 @@ #!/bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2013, 2017, 2018, 2019 Laboratoire de Recherche et Développement -# de l'Epita (LRDE). +# Copyright (C) 2013, 2017-2019, 2021 Laboratoire de Recherche et +# Développement de l'Epita (LRDE). # # This file is part of Spot, a model checking library. # @@ -1300,8 +1300,8 @@ cat >expected <<'EOF' "!((G(F(p0))) | ((p1) & (F(p2))))","15",5 "!((G(F(p0))) | ((p1) & (F(p2))))","16",5 "!((G(F(p0))) | ((p1) & (F(p2))))","17",5 -"X((p0) R ((F(p1)) R (F(!(p1)))))","1",6 -"X((p0) R ((F(p1)) R (F(!(p1)))))","2",6 +"X((p0) R ((F(p1)) R (F(!(p1)))))","1",4 +"X((p0) R ((F(p1)) R (F(!(p1)))))","2",4 "X((p0) R ((F(p1)) R (F(!(p1)))))","3",4 "X((p0) R ((F(p1)) R (F(!(p1)))))","4",4 "X((p0) R ((F(p1)) R (F(!(p1)))))","6",4 diff --git a/tests/python/decompose.ipynb b/tests/python/decompose.ipynb index 091dead91..7f23b1777 100644 --- a/tests/python/decompose.ipynb +++ b/tests/python/decompose.ipynb @@ -200,7 +200,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f1aa01ba3c0> >" + " *' at 0x7f56404b14b0> >" ] }, "execution_count": 2, @@ -330,7 +330,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f1aa01ba2a0> >" + " *' at 0x7f56404b11b0> >" ] }, "execution_count": 3, @@ -489,7 +489,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f1aa01ba1b0> >" + " *' at 0x7f56404b1270> >" ] }, "execution_count": 4, @@ -587,7 +587,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f1aa01ba9c0> >" + " *' at 0x7f56404b18d0> >" ] }, "execution_count": 5, @@ -669,7 +669,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f1aa00b6240> >" + " *' at 0x7f56404b1c00> >" ] }, "execution_count": 6, @@ -796,7 +796,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f1aa00b6120> >" + " *' at 0x7f56404b1f60> >" ] }, "metadata": {}, @@ -941,7 +941,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f1aa01bae40> >" + " *' at 0x7f56404b1d80> >" ] }, "metadata": {}, @@ -1109,7 +1109,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f1aa01baea0> >" + " *' at 0x7f56404b1f90> >" ] }, "metadata": {}, @@ -1512,7 +1512,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f1aa00b6c60> >" + " *' at 0x7f56404b1ed0> >" ] }, "execution_count": 8, @@ -1898,7 +1898,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f1aa00b6510> >" + " *' at 0x7f56404b1b70> >" ] }, "metadata": {}, @@ -2130,7 +2130,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f1aa01baea0> >" + " *' at 0x7f56404b1f60> >" ] }, "metadata": {}, @@ -2340,7 +2340,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f1aa01bad80> >" + " *' at 0x7f56404b1ab0> >" ] }, "metadata": {}, @@ -2728,7 +2728,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f1aa00b6570> >" + " *' at 0x7f56404b1c90> >" ] }, "execution_count": 10, @@ -2889,7 +2889,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f1aa00b6e70> >" + " *' at 0x7f5640045330> >" ] }, "metadata": {}, @@ -3028,7 +3028,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f1aa01baf00> >" + " *' at 0x7f5640d27930> >" ] }, "metadata": {}, @@ -3043,23 +3043,23 @@ "\n", "\n", - "\n", - "\n", + "\n", + "\n", "strong\n", - "\n", - "strong\n", - "Inf(\n", - "⓿\n", - ") | (Fin(\n", - "❶\n", - ") & Inf(\n", - "❷\n", - "))\n", - "[parity min even 3]\n", + "\n", + "strong\n", + "Inf(\n", + "⓿\n", + ") | (Fin(\n", + "❶\n", + ") & Inf(\n", + "❷\n", + "))\n", + "[parity min even 3]\n", "\n", "cluster_0\n", - "\n", + "\n", "\n", "\n", "cluster_1\n", @@ -3078,109 +3078,102 @@ "\n", "\n", "\n", - "\n", + "\n", "\n", + "1\n", + "\n", + "1\n", + "⓿\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "(b & !c) | (!a & !c)\n", + "\n", + "\n", + "\n", "2\n", - "\n", - "2\n", - "❶\n", + "\n", + "2\n", + "❶\n", "\n", "\n", - "\n", - "0->2\n", - "\n", - "\n", - "a & !b & !c\n", - "\n", - "\n", - "\n", - "1\n", - "\n", - "1\n", - "⓿\n", - "\n", - "\n", "\n", - "0->1\n", - "\n", - "\n", - "a & b & !c\n", - "\n", - "\n", - "\n", - "0->1\n", - "\n", - "\n", - "!a & !c\n", - "\n", - "\n", - "\n", - "2->2\n", - "\n", - "\n", - "a & !c\n", - "\n", - "\n", - "\n", - "2->1\n", - "\n", - "\n", - "!a & !c\n", - "\n", - "\n", - "\n", - "1->2\n", - "\n", - "\n", - "a & !b & !c\n", + "0->2\n", + "\n", + "\n", + "a & !b & !c\n", "\n", "\n", - "\n", + "\n", "1->1\n", - "\n", - "\n", - "!a & !c\n", + "\n", + "\n", + "!a & !c\n", + "\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "a & !b & !c\n", "\n", "\n", "\n", "3\n", - "\n", - "3\n", - "❷\n", + "\n", + "3\n", + "❷\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", - "a & !b & !c\n", + "\n", + "\n", + "2->1\n", + "\n", + "\n", + "!a & !c\n", + "\n", + "\n", + "\n", + "2->2\n", + "\n", + "\n", + "a & !c\n", "\n", "\n", - "\n", + "\n", "3->1\n", - "\n", - "\n", - "!a & !c\n", + "\n", + "\n", + "!a & !c\n", + "\n", + "\n", + "\n", + "3->2\n", + "\n", + "\n", + "a & !b & !c\n", "\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 0x7f1aa00b6a20> >" + " *' at 0x7f56400456f0> >" ] }, "metadata": {}, @@ -3533,7 +3526,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f1aa00b6120> >" + " *' at 0x7f5640045450> >" ] }, "execution_count": 12, @@ -3876,7 +3869,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f1aa00c01b0> >" + " *' at 0x7f5640045540> >" ] }, "metadata": {}, @@ -4053,7 +4046,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f1aa00b6f60> >" + " *' at 0x7f5640d3abd0> >" ] }, "metadata": {}, @@ -4211,7 +4204,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f1aa029e660> >" + " *' at 0x7f5640d3a8a0> >" ] }, "metadata": {}, @@ -4560,7 +4553,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f1aa00c0a80> >" + " *' at 0x7f5640d3ae10> >" ] }, "execution_count": 14, @@ -4683,7 +4676,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f1aa00c0540> >" + " *' at 0x7f5640045930> >" ] }, "execution_count": 15, @@ -4781,7 +4774,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f1aa00c8090> >" + " *' at 0x7f56400452a0> >" ] }, "metadata": {}, @@ -4857,7 +4850,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f1aa00c0270> >" + " *' at 0x7f5640d3a930> >" ] }, "metadata": {}, @@ -4951,7 +4944,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f1aa00c8090> >" + " *' at 0x7f5640045090> >" ] }, "execution_count": 18, @@ -5101,7 +5094,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f1aa00c8a50> >" + " *' at 0x7f5640045b70> >" ] }, "execution_count": 19, @@ -5261,7 +5254,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f1aa00d0cc0> >" + " *' at 0x7f5640052300> >" ] }, "metadata": {}, @@ -5363,7 +5356,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f1aa00b6780> >" + " *' at 0x7f5640d34a80> >" ] }, "metadata": {}, @@ -5498,7 +5491,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f1aa00c0570> >" + " *' at 0x7f5640052360> >" ] }, "metadata": {}, @@ -5702,7 +5695,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f1aa00c85d0> >" + " *' at 0x7f5640045f00> >" ] }, "metadata": {}, @@ -5843,7 +5836,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f1aa00c8cf0> >" + " *' at 0x7f5640d34ae0> >" ] }, "execution_count": 21, @@ -5946,7 +5939,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f1aa00c8b10> >" + " *' at 0x7f5640045e40> >" ] }, "execution_count": 22, @@ -5957,6 +5950,13 @@ "source": [ "spot.decompose_scc(si, 'a2')" ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [] } ], "metadata": { diff --git a/tests/python/simstate.py b/tests/python/simstate.py index 3a639b094..278e05045 100644 --- a/tests/python/simstate.py +++ b/tests/python/simstate.py @@ -649,3 +649,41 @@ State: 7 [0&1] 5 [1] 7 --END--''' + + +# issue #452 +aut = spot.automaton("""HOA: v1 +States: 9 +Start: 0 +AP: 4 "p0" "p1" "p2" "p3" +Acceptance: 2 Fin(0)&Fin(1) +Alias: @p 0&1&!2&3 +--BODY-- +State: 0 +[@p] 1 {0 1} +State: 1 +[@p] 2 {0 1} +State: 2 +[@p] 0 {0 1} +[@p] 2 +[@p] 3 {0} +[@p] 4 {1} +State: 3 +[@p] 5 {0 1} +[@p] 6 {0} +State: 4 +[@p] 7 {0 1} +[@p] 8 {1} +State: 5 +[@p] 8 {0 1} +State: 6 +[@p] 2 {0} +[@p] 4 {0 1} +State: 7 +[@p] 6 {0 1} +State: 8 +[@p] 2 {1} +[@p] 3 {0 1} +--END--""") +aut = spot.simulation(aut) +assert aut.num_states() == 1