diff --git a/NEWS b/NEWS index d025625a3..fed67a1ca 100644 --- a/NEWS +++ b/NEWS @@ -32,6 +32,9 @@ New in spot 2.9.0.dev (not yet released) spot::translator class when creating deterministic automata with generic acceptance. + - remove_fin() learned a trick to remove some superfluous + transitions. + Bugs fixed: - Work around undefined behavior reported by clang 10.0.0's UBsan. diff --git a/spot/twaalgos/remfin.cc b/spot/twaalgos/remfin.cc index d34110e62..38774f60b 100644 --- a/spot/twaalgos/remfin.cc +++ b/spot/twaalgos/remfin.cc @@ -667,6 +667,20 @@ namespace spot trace << "main_sets " << main_sets << "\nmain_add " << main_add << '\n'; + // If the SCC is rejecting, there is no need for clone. + // Pretend we don't interesect any Fin. + if (si.is_rejecting_scc(n)) + intersects_fin = false; + + // Edges that are already satisfying the acceptance of the + // main copy do not need to be duplicated in the clones, so + // we fill allacc_edge to remember those. Of course this is + // only needed if the main copy can be accepting and if we + // will create clones. + std::vector allacc_edge(aut->edge_vector().size(), false); + auto main_acc = res->acc().restrict_to(main_sets | main_add); + bool check_main_acc = intersects_fin && !main_acc.is_f(); + // Create the main copy for (auto s: states) for (auto& t: aut->out(s)) @@ -675,11 +689,14 @@ namespace spot if (sbacc || SPOT_LIKELY(si.scc_of(t.dst) == n)) a = (t.acc & main_sets) | main_add; res->new_edge(s, t.dst, t.cond, a); + // remember edges that are completely accepting + if (check_main_acc && main_acc.accepting(a)) + allacc_edge[aut->edge_number(t)] = true; } // We do not need any other copy if the SCC is non-accepting, // of if it does not intersect any Fin. - if (!intersects_fin || si.is_rejecting_scc(n)) + if (!intersects_fin) continue; // Create clones @@ -698,7 +715,12 @@ namespace spot auto ns = state_map[s]; for (auto& t: aut->out(s)) { - if ((t.acc & r) || si.scc_of(t.dst) != n) + if ((t.acc & r) || si.scc_of(t.dst) != n + // edges that are already accepting in the + // main copy need not be copied in the + // clone, since cycles going through them + // are already accepted. + || allacc_edge[aut->edge_number(t)]) continue; auto nd = state_map[t.dst]; res->new_edge(ns, nd, t.cond, (t.acc & k) | a); diff --git a/tests/core/ltl2dstar4.test b/tests/core/ltl2dstar4.test index a0db47ec4..dfa004805 100755 --- a/tests/core/ltl2dstar4.test +++ b/tests/core/ltl2dstar4.test @@ -1,6 +1,6 @@ #!/bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2013, 2014, 2015, 2017 Laboratoire de Recherche et +# Copyright (C) 2013-2015, 2017, 2020 Laboratoire de Recherche et # Développement de l'Epita (LRDE). # # This file is part of Spot, a model checking library. @@ -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 25 149 416 2 0' +test "`cat out`" = '9 144 4 18 98 202 2 0' ltlfilt -f '(GFa -> GFb) & (GFc -> GFd)' -l | ltl2dstar --ltl2nba=spin:ltl2tgba@-s $STR - - | diff --git a/tests/python/remfin.py b/tests/python/remfin.py index b6f53d453..7eb9ab4d2 100644 --- a/tests/python/remfin.py +++ b/tests/python/remfin.py @@ -1,6 +1,6 @@ # -*- mode: python; coding: utf-8 -*- -# Copyright (C) 2015-2018 Laboratoire de Recherche et Développement -# de l'Epita +# Copyright (C) 2015-2018, 2020 Laboratoire de Recherche et Développement de +# l'Epita # # This file is part of Spot, a model checking library. # @@ -67,3 +67,29 @@ assert(a.prop_universal().is_maybe()) assert(a.prop_unambiguous().is_maybe()) assert(a.is_deterministic() == True) assert(a.is_unambiguous() == True) + +a = spot.automaton(""" +HOA: v1 +States: 3 +Start: 0 +AP: 2 "a" "b" +acc-name: Buchi +Acceptance: 5 Inf(0)&Fin(4) | Inf(2)&Inf(3) | Inf(1) +--BODY-- +State: 0 {3} +[t] 0 +[0] 1 {1} +[!0] 2 {0 4} +State: 1 {3} +[1] 0 +[0&1] 1 {0} +[!0&1] 2 {2 4} +State: 2 +[!1] 0 +[0&!1] 1 {0} +[!0&!1] 2 {0 4} +--END-- +""") +b = spot.remove_fin(a) +size = (b.num_states(), b.num_edges()) +assert size == (5, 17);