diff --git a/spot/twaalgos/remfin.cc b/spot/twaalgos/remfin.cc index 646db08e5..0b9bb3cc9 100644 --- a/spot/twaalgos/remfin.cc +++ b/spot/twaalgos/remfin.cc @@ -273,7 +273,8 @@ namespace spot state_map[s] = base++; for (const auto& e: si.inner_edges_of(scc)) { - if (e.acc.has(r) || accedge[aut->edge_number(e)]) + unsigned en = aut->edge_number(e); + if ((e.acc | propmarks[en]).has(r) || accedge[en]) continue; auto src = state_map[e.src]; auto dst = state_map[e.dst]; diff --git a/tests/core/det.test b/tests/core/det.test index e30f2b873..7f4fe1eea 100755 --- a/tests/core/det.test +++ b/tests/core/det.test @@ -1,6 +1,6 @@ #!/bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2013-2019 Laboratoire de Recherche et Développement de +# Copyright (C) 2013-2020 Laboratoire de Recherche et Développement de # l'Epita (LRDE). # # This file is part of Spot, a model checking library. @@ -94,16 +94,13 @@ State: 0 State: 1 [!0] 0 [0] 2 -[!0] 3 State: 2 [!0] 0 [0] 2 -[!0] 3 [0] 4 State: 3 {0} [!0] 3 State: 4 {0} -[!0] 3 [0] 4 --END-- EOF diff --git a/tests/core/remfin.test b/tests/core/remfin.test index 441fb21ea..6de24007d 100755 --- a/tests/core/remfin.test +++ b/tests/core/remfin.test @@ -752,7 +752,7 @@ State: 1 {0} [!0] 0 --END-- HOA: v1 -States: 21 +States: 19 Start: 0 AP: 2 "p0" "p1" acc-name: Buchi @@ -768,20 +768,19 @@ State: 1 [0&!1] 6 [0&1] 9 [!0&1] 14 -[!0&1] 20 +[!0&1] 18 State: 2 [!0&!1] 1 [!0&1] 8 -[!0&!1] 20 +[!0&!1] 18 State: 3 [0&1] 2 [!0&1] 5 -[0&1] 18 State: 4 [0&!1] 4 [0&1] 5 [0&1] 6 -[0&!1] 17 +[0&!1] 16 State: 5 [0&1] 9 State: 6 @@ -789,7 +788,6 @@ State: 6 [0&1] 5 [!0&1] 9 [!0&1] 12 -[!0&1] 17 State: 7 {0} [0&!1] 3 [!0&1] 5 @@ -799,15 +797,12 @@ State: 8 [!0&!1] 3 [!0&1] 4 [!0&1] 8 -[!0&1] 12 [!0&1] 13 -[!0&1] 17 -[!0&!1] 19 State: 9 [!0&1] 2 [0&!1] 6 [0&!1] 11 -[!0&1] 18 +[!0&1] 17 State: 10 {0} [0&!1] 11 State: 11 {0} @@ -816,25 +811,18 @@ State: 11 {0} State: 12 {0} [0&1] 11 State: 13 {0} -[!0&1] 12 [!0&1] 13 State: 14 {0} [!0&1] 14 State: 15 {0} -[0&1] 16 +[!0&1] 17 State: 16 {0} -[!0&1] 18 +[0&!1] 16 State: 17 {0} -[0&1] 15 -[0&!1] 17 +[!0&!1] 18 State: 18 {0} -[!0&!1] 20 -State: 19 {0} -[!0&1] 15 -[0&1] 18 -State: 20 {0} -[0&1] 16 -[!0&1] 20 +[0&1] 15 +[!0&1] 18 --END-- HOA: v1 States: 4 @@ -1341,7 +1329,7 @@ State: 1 {0} [0] 1 --END-- HOA: v1 -States: 21 +States: 19 Start: 0 AP: 2 "p0" "p1" acc-name: Buchi @@ -1357,20 +1345,19 @@ State: 1 [0&!1] 6 [0&1] 9 [!0&1] 14 -[!0&1] 20 +[!0&1] 18 State: 2 [!0&!1] 1 [!0&1] 8 -[!0&!1] 20 +[!0&!1] 18 State: 3 [0&1] 2 [!0&1] 5 -[0&1] 18 State: 4 [0&!1] 4 [0&1] 5 [0&1] 6 -[0&!1] 17 +[0&!1] 16 State: 5 [0&1] 9 State: 6 @@ -1378,7 +1365,6 @@ State: 6 [0&1] 5 [!0&1] 9 [!0&1] 12 -[!0&1] 17 State: 7 [0&!1] 3 [!0&1] 5 @@ -1388,15 +1374,12 @@ State: 8 [!0&!1] 3 [!0&1] 4 [!0&1] 8 -[!0&1] 12 [!0&1] 13 -[!0&1] 17 -[!0&!1] 19 State: 9 [!0&1] 2 [0&!1] 6 [0&!1] 11 -[!0&1] 18 +[!0&1] 17 State: 10 [0&!1] 11 {0} State: 11 @@ -1405,25 +1388,18 @@ State: 11 State: 12 [0&1] 11 {0} State: 13 -[!0&1] 12 [!0&1] 13 {0} State: 14 [!0&1] 14 {0} State: 15 -[0&1] 16 +[!0&1] 17 {0} State: 16 -[!0&1] 18 {0} +[0&!1] 16 {0} State: 17 -[0&1] 15 -[0&!1] 17 {0} +[!0&!1] 18 {0} State: 18 -[!0&!1] 20 {0} -State: 19 -[!0&1] 15 -[0&1] 18 -State: 20 -[0&1] 16 {0} -[!0&1] 20 {0} +[0&1] 15 {0} +[!0&1] 18 {0} --END-- HOA: v1 States: 4 diff --git a/tests/python/automata.ipynb b/tests/python/automata.ipynb index f0b95a995..061ab1838 100644 --- a/tests/python/automata.ipynb +++ b/tests/python/automata.ipynb @@ -178,7 +178,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f1940090f00> >" + " *' at 0x7f65f48a3f90> >" ] }, "execution_count": 2, @@ -657,7 +657,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f1940108e10> >" + " *' at 0x7f65f4901f90> >" ] }, "execution_count": 6, @@ -733,7 +733,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f1940108870> >" + " *' at 0x7f65f48b2540> >" ] }, "execution_count": 7, @@ -816,7 +816,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f1940108ab0> >" + " *' at 0x7f65f60e46c0> >" ] }, "execution_count": 8, @@ -1349,7 +1349,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f194009f600> >" + " *' at 0x7f65f48b2660> >" ] }, "execution_count": 12, @@ -1463,7 +1463,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f19401080f0> >" + " *' at 0x7f65f48c1180> >" ] }, "execution_count": 13, @@ -1594,7 +1594,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f19400ad270> >" + " *' at 0x7f65f48c15d0> >" ] }, "execution_count": 14, @@ -1816,7 +1816,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f19400b1480> >" + " *' at 0x7f65f48c66f0> >" ] }, "metadata": {}, @@ -1831,178 +1831,164 @@ "\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", + "!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", - "\n", - "2->3\n", - "\n", - "\n", - "!b\n", - "\n", - "\n", - "\n", - "2->4\n", - "\n", - "\n", - "a & !b\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 0x7f19400b13f0> >" + " *' at 0x7f65f48c6660> >" ] }, "metadata": {}, @@ -2017,171 +2003,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", + "1->0\n", + "\n", + "\n", + "b\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "a & b\n", "\n", "\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", + "2\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", - "\n", - "2->2\n", - "\n", - "\n", - "!a & !b\n", - "\n", - "\n", - "\n", - "2->3\n", - "\n", - "\n", - "a & !b\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 0x7f19400b16f0> >" + " *' at 0x7f65f48c6a20> >" ] }, "metadata": {}, @@ -2196,11 +2161,11 @@ "\n", "\n", - "\n", - "\n", - "\n", - "[Büchi]\n", + "\n", + "\n", + "\n", + "[Büchi]\n", "\n", "\n", "\n", @@ -2245,91 +2210,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", + "!a & b\n", + "\n", + "\n", + "\n", + "2->4\n", + "\n", + "\n", + "a & b\n", "\n", "\n", - "\n", + "\n", "3->0\n", - "\n", + "\n", "\n", - "!b\n", + "!b\n", "\n", "\n", - "\n", - "3->2\n", - "\n", - "\n", - "a & !b\n", - "\n", - "\n", "\n", - "3->4\n", - "\n", - "\n", - "a & !b\n", + "3->2\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 0x7f19400b1420> >" + " *' at 0x7f65f48c6960> >" ] }, "metadata": {}, @@ -2518,7 +2483,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f19400b18a0> >" + " *' at 0x7f65f48c6cc0> >" ] }, "execution_count": 19, @@ -2594,7 +2559,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f19400b1e70> >" + " *' at 0x7f65f48ca1b0> >" ] }, "execution_count": 20, @@ -3144,7 +3109,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f19402232a0> >" + " *' at 0x7f65f48c1060> >" ] }, "metadata": {}, @@ -3244,7 +3209,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f1940108f60> >" + " *' at 0x7f65f48c1900> >" ] }, "execution_count": 24, @@ -3317,7 +3282,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f19400b1bd0> >" + " *' at 0x7f65f4901900> >" ] }, "execution_count": 25, @@ -3488,7 +3453,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f19400b8b40> >" + " *' at 0x7f65f48c6060> >" ] }, "execution_count": 27, @@ -3571,7 +3536,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f19402232a0> >" + " *' at 0x7f65f48c1060> >" ] }, "metadata": {}, @@ -3636,7 +3601,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f19402232a0> >" + " *' at 0x7f65f48c1060> >" ] }, "metadata": {}, @@ -3723,7 +3688,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f19402232a0> >" + " *' at 0x7f65f48c1060> >" ] }, "execution_count": 29, @@ -3756,7 +3721,7 @@ "name": "python", "nbconvert_exporter": "python", "pygments_lexer": "ipython3", - "version": "3.8.2" + "version": "3.8.5" } }, "nbformat": 4, diff --git a/tests/python/remfin.py b/tests/python/remfin.py index 7eb9ab4d2..4cede285c 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, 17); +assert size == (5, 15); diff --git a/tests/python/tra2tba.py b/tests/python/tra2tba.py index 2cb1bfb5c..59ce3ab63 100644 --- a/tests/python/tra2tba.py +++ b/tests/python/tra2tba.py @@ -536,7 +536,6 @@ State: 0 State: 1 [!0] 0 [0] 1 -[!0] 3 State: 2 {0} [!0] 2 State: 3 {0}