From b0b431a5a4281b1a3e1753d4b9dd2a9547661406 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 3 May 2018 17:35:02 +0200 Subject: [PATCH] improve gf_guarantee_to_ba * spot/twaalgos/gfguarantee.cc: Combine the last letter read with the first one of the next pass when doing transition-based acceptance. Also move the initial states to the source of any accepting transition if the input is deterministic. * tests/core/ltl2tgba2.test, tests/core/satmin.test, tests/python/stutter-inv.ipynb: Reduce expected sizes of a few automata. --- spot/twaalgos/gfguarantee.cc | 74 ++++++++++++++++++++++++++++++---- tests/core/ltl2tgba2.test | 4 +- tests/core/satmin.test | 4 +- tests/python/stutter-inv.ipynb | 31 ++++++-------- 4 files changed, 83 insertions(+), 30 deletions(-) diff --git a/spot/twaalgos/gfguarantee.cc b/spot/twaalgos/gfguarantee.cc index c4296d41f..137d513b4 100644 --- a/spot/twaalgos/gfguarantee.cc +++ b/spot/twaalgos/gfguarantee.cc @@ -26,6 +26,7 @@ #include #include #include +#include namespace spot { @@ -73,16 +74,75 @@ namespace spot if (!state_based) { + bool is_det = is_deterministic(aut); + bool initial_state_reachable = false; for (auto& e: aut->edges()) - if (term[si.scc_of(e.dst)]) + if (e.dst == init) { - e.dst = init; - e.acc = {0}; - } - else - { - e.acc = {}; + initial_state_reachable = true; + break; } + unsigned nedges = aut->num_edges(); + unsigned new_init = -1U; + // The loop might add new edges, but we just want to iterate + // on the initial ones. + for (unsigned edge = 1; edge <= nedges; ++edge) + { + auto& e = aut->edge_storage(edge); + if (term[si.scc_of(e.dst)]) + { + if (initial_state_reachable + // If the source state is the initial state, we + // should not try to combine it with itself... + || e.src == init) + { + e.dst = init; + e.acc = {0}; + new_init = init; + continue; + } + // If initial state cannot be reached from another + // state of the automaton, we can get rid of it by + // combining the edge reaching the terminal state + // with the edges leaving the initial state. + bdd econd = e.cond; + bool first = true; + // Combine this edge with any compatible edge from + // the initial state. + for (auto& ei: aut->out(init)) + { + bdd cond = ei.cond & econd; + if (cond != bddfalse) + { + if (first) + { + e.dst = ei.dst; + e.acc = {0}; + e.cond = cond; + first = false; + if (new_init == -1U) + new_init = e.src; + } + else + { + aut->new_edge(e.src, ei.dst, cond, {0}); + } + + } + } + } + else + { + e.acc = {}; + } + } + // In a deterministic and suspendable automaton, all states + // recognize the same language, so we can freely move the + // initial state. We decide to use the source of any + // accepting transition, in the hope that it will make the + // original initial state unreachable. + if (is_det && new_init != -1U) + aut->set_init_state(new_init); } else { diff --git a/tests/core/ltl2tgba2.test b/tests/core/ltl2tgba2.test index e249d228e..18cd9b31d 100755 --- a/tests/core/ltl2tgba2.test +++ b/tests/core/ltl2tgba2.test @@ -132,8 +132,8 @@ sb-patterns,26, 1,1, 1,1, 1,1, 1,1 sb-patterns,27, 2,7, 2,7, 2,7, 2,7 hkrss-patterns,1, 1,2, 1,2, 3,6, 3,6 hkrss-patterns,2, 1,2, 1,2, 3,6, 3,6 -hkrss-patterns,3, 5,20, 5,20, 5,20, 5,20 -hkrss-patterns,4, 9,400, 17,272, 9,400, 17,272 +hkrss-patterns,3, 4,16, 4,16, 5,20, 5,20 +hkrss-patterns,4, 9,400, 16,256, 9,400, 17,272 hkrss-patterns,6, 1,2, 1,2, 3,6, 3,6 hkrss-patterns,7, 2,8, 2,8, 2,8, 2,8 hkrss-patterns,8, 1,1, 1,1, 1,1, 1,1 diff --git a/tests/core/satmin.test b/tests/core/satmin.test index 4a5b75247..564106186 100755 --- a/tests/core/satmin.test +++ b/tests/core/satmin.test @@ -660,8 +660,8 @@ cat >expected <<'EOF' "!(G((p0) -> ((p1) U (p2))))","15",3 "!(G((p0) -> ((p1) U (p2))))","16",3 "!(G((p0) -> ((p1) U (p2))))","17",3 -"G(F((p0) <-> (X(X(p1)))))","1",7 -"G(F((p0) <-> (X(X(p1)))))","2",7 +"G(F((p0) <-> (X(X(p1)))))","1",6 +"G(F((p0) <-> (X(X(p1)))))","2",6 "G(F((p0) <-> (X(X(p1)))))","3",4 "G(F((p0) <-> (X(X(p1)))))","4",4 "G(F((p0) <-> (X(X(p1)))))","6",4 diff --git a/tests/python/stutter-inv.ipynb b/tests/python/stutter-inv.ipynb index c5bcddacb..4229be2f4 100644 --- a/tests/python/stutter-inv.ipynb +++ b/tests/python/stutter-inv.ipynb @@ -302,7 +302,7 @@ "\n" ], "text/plain": [ - " *' at 0x7ff49441fc30> >" + " *' at 0x7f6b5c32c720> >" ] }, "metadata": {}, @@ -595,7 +595,7 @@ "\n" ], "text/plain": [ - " *' at 0x7ff4943ae090> >" + " *' at 0x7f6b5c358f90> >" ] }, "metadata": {}, @@ -804,7 +804,7 @@ "\n" ], "text/plain": [ - " *' at 0x7ff4943ae090> >" + " *' at 0x7f6b5c358f90> >" ] }, "metadata": {}, @@ -963,7 +963,7 @@ "\n" ], "text/plain": [ - " *' at 0x7ff49441f810> >" + " *' at 0x7f6b5c358ea0> >" ] }, "metadata": {}, @@ -1062,7 +1062,7 @@ "\n" ], "text/plain": [ - " *' at 0x7ff4943bf6c0> >" + " *' at 0x7f6b5c32c750> >" ] }, "metadata": {}, @@ -1279,7 +1279,7 @@ "\n" ], "text/plain": [ - " *' at 0x7ff4943bf690> >" + " *' at 0x7f6b5c2cb360> >" ] }, "metadata": {}, @@ -1446,7 +1446,7 @@ "\n" ], "text/plain": [ - " *' at 0x7ff494457060> >" + " *' at 0x7f6b5c2cb480> >" ] }, "metadata": {}, @@ -1577,7 +1577,7 @@ "\n" ], "text/plain": [ - " *' at 0x7ff4943bfea0> >" + " *' at 0x7f6b5c2cbd50> >" ] }, "metadata": {}, @@ -1837,7 +1837,7 @@ "\n" ], "text/plain": [ - " *' at 0x7ff4943d02d0> >" + " *' at 0x7f6b5c2dd570> >" ] }, "metadata": {}, @@ -2151,7 +2151,7 @@ "\n" ], "text/plain": [ - " *' at 0x7ff4943d02d0> >" + " *' at 0x7f6b5c2dd570> >" ] }, "metadata": {}, @@ -2258,7 +2258,7 @@ "F(p0 & X(p1 & XFp2)) 4 2 1\n", "F(p0 & X(p1 U p2)) 3 1 1\n", "G(p0 & Fp1 & Fp2 & Fp3) 1 1 1\n", - "GF((!p0 & Xp0) | (p0 & X!p0) | (!p1 & Xp 5 5 1\n", + "GF((!p0 & Xp0) | (p0 & X!p0) | (!p1 & Xp 4 4 1\n", "GF((!p0 & Xp0) | (p0 & X!p0) | (!p1 & Xp 9 9 1\n", "G(!p0 | !p1 | p2 | X(!p2 | p3 | X(!p1 | 3 0 1\n", "G(!p0 | !p1 | p2 | X(!p2 | (p2 U (!p2 U 5 5 1\n", @@ -2362,7 +2362,7 @@ { "data": { "text/plain": [ - "55.90277777777778" + "55.749128919860624" ] }, "execution_count": 31, @@ -2373,13 +2373,6 @@ "source": [ "100*sum(sistates_size)/sum(aut_size)" ] - }, - { - "cell_type": "code", - "execution_count": null, - "metadata": {}, - "outputs": [], - "source": [] } ], "metadata": {