diff --git a/NEWS b/NEWS index 4d9d1def2..e8774df45 100644 --- a/NEWS +++ b/NEWS @@ -32,6 +32,10 @@ New in spot 2.11.3.dev (not yet released) incorrectly handling of states without successors, causing some segfaults. (Issue #524.) + - Running delay_branching_here() on state-based automata (this was not + done in Spot so far) may require the output to use transition-based + acceptance. (Issue #525.) + New in spot 2.11.3 (2022-12-09) Bug fixes: diff --git a/spot/twaalgos/dbranch.cc b/spot/twaalgos/dbranch.cc index 19a0d9474..7cf1b262e 100644 --- a/spot/twaalgos/dbranch.cc +++ b/spot/twaalgos/dbranch.cc @@ -66,6 +66,10 @@ namespace spot hashmap_t first_dest[1 + is_game]; auto& g = aut->get_graph(); + // Merging outgoing transitions may cause the automaton to need + // transition-based acceptance. + bool need_trans = !aut->prop_state_acc().is_true(); + // setup a DFS std::vector seen(ns); std::stack todo; @@ -128,9 +132,18 @@ namespace spot unsigned& mergedlast = g.state_storage(mergedst).succ_tail; unsigned& candfirst = g.state_storage(canddst).succ; if (mergedlast) - aut->edge_storage(mergedlast).next_succ = candfirst; + { + aut->edge_storage(mergedlast).next_succ = candfirst; + // Do we need to require transition-based acceptance? + if (!need_trans) + need_trans = + (aut->edge_storage(candfirst).acc + != aut->edge_storage(mergedfirst).acc); + } else // mergedst had no successor - mergedfirst = candfirst; + { + mergedfirst = candfirst; + } mergedlast = candlast; // 2) updating the source of the merged transitions for (unsigned e2 = candfirst; e2 != 0;) @@ -149,6 +162,8 @@ namespace spot changed = true; } } + if (need_trans) + aut->prop_state_acc(false); return changed; } } diff --git a/spot/twaalgos/dbranch.hh b/spot/twaalgos/dbranch.hh index 9cd0efa5e..022c1a75b 100644 --- a/spot/twaalgos/dbranch.hh +++ b/spot/twaalgos/dbranch.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2022 Laboratoire de Recherche et Développement +// Copyright (C) 2022, 2023 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -26,10 +26,15 @@ namespace spot /// \ingroup twa_algorithms /// \brief Merge states to delay /// - /// If a state (x) has two outgoing transitions (x,l,m,y) and - /// (x,l,m,z) going to states (x) and (y) that have no other - /// incoming edges, then (y) and (z) can be merged (keeping the - /// union of their outgoing destinations). + /// In an automaton with transition-based acceptance, if a state (x) + /// has two outgoing transitions (x,l,m,y) and (x,l,m,z) going to + /// states (x) and (y) that have no other incoming edges, then (y) + /// and (z) can be merged (keeping the union of their outgoing + /// destinations). + /// + /// If the input automaton uses state-based acceptance, running this + /// function might make the acceptance transition-based, but only if + /// two states with different acceptance are merged at some point. /// /// \return true iff the automaton was modified. SPOT_API bool delay_branching_here(const twa_graph_ptr& aut); diff --git a/tests/python/dbranch.py b/tests/python/dbranch.py index ecf17d7d0..268c4a3c6 100644 --- a/tests/python/dbranch.py +++ b/tests/python/dbranch.py @@ -1,5 +1,5 @@ # -*- mode: python; coding: utf-8 -*- -# Copyright (C) 2022 Laboratoire de Recherche et +# Copyright (C) 2022, 2023 Laboratoire de Recherche et # Développement de l'Epita (LRDE). # # This file is part of Spot, a model checking library. @@ -145,3 +145,30 @@ State: 5 State: 6 [t] 6 --END--""") + +# Running delay_branching_here on state-based acceptance may require +# the output to use transition-based acceptance. (Issue #525.) +a = spot.automaton(""" +HOA: v1 States: 4 Start: 0 AP: 2 "a" "b" Acceptance: 1 Inf(0) --BODY-- +State: 0 [0] 1 [0] 2 State: 1 [1] 3 State: 2 {0} [!1] 3 State: 3 [t] 0 +--END--""") +copy = spot.make_twa_graph(a, spot.twa_prop_set.all()) +if spot.delay_branching_here(a): + a.purge_unreachable_states() +tc.assertTrue(spot.are_equivalent(a, copy)) +tc.assertEqual(a.to_str(), """HOA: v1 +States: 3 +Start: 0 +AP: 2 "b" "a" +acc-name: Buchi +Acceptance: 1 Inf(0) +properties: trans-labels explicit-labels trans-acc deterministic +--BODY-- +State: 0 +[1] 1 +State: 1 +[0] 2 +[!0] 2 {0} +State: 2 +[t] 0 +--END--""")