diff --git a/NEWS b/NEWS index 167e4f770..20c507343 100644 --- a/NEWS +++ b/NEWS @@ -57,6 +57,11 @@ New in spot 2.10.4.dev (net yet released) - purge_dead_states() will now also remove edges labeled by false (except self-loops). + Bugs fixed: + + - reduce_parity() produced incorrect results when applied to + automata with deleted edges. + New in spot 2.10.4 (2022-02-01) Bug fixed: diff --git a/spot/twaalgos/parity.cc b/spot/twaalgos/parity.cc index 35ec10a90..94c7bd922 100644 --- a/spot/twaalgos/parity.cc +++ b/spot/twaalgos/parity.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2016, 2018, 2019 Laboratoire de Recherche et Développement -// de l'Epita (LRDE). +// Copyright (C) 2016, 2018, 2019, 2022 Laboratoire de Recherche et +// Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -465,8 +465,9 @@ namespace spot // using k=0 or k=1. // // -2 means the edge was never assigned a color. - std::vector piprime1(aut->num_edges() + 1, -2); // k=1 - std::vector piprime2(aut->num_edges() + 1, -2); // k=0 + unsigned evs = aut->edge_vector().size(); + std::vector piprime1(evs, -2); // k=1 + std::vector piprime2(evs, -2); // k=0 bool sba = aut->prop_state_acc().is_true(); auto rec = diff --git a/tests/python/parity.py b/tests/python/parity.py index dfeb24d3d..b0389c40e 100644 --- a/tests/python/parity.py +++ b/tests/python/parity.py @@ -1,6 +1,6 @@ #!/usr/bin/python3 # -*- mode: python; coding: utf-8 -*- -# Copyright (C) 2018, 2019 Laboratoire de Recherche et Développement de +# Copyright (C) 2018, 2019, 2022 Laboratoire de Recherche et Développement de # l'EPITA. # # This file is part of Spot, a model checking library. @@ -155,3 +155,17 @@ except RuntimeError as e: assert "invalid state number" in str(e) else: report_missing_exception() + + +a = spot.automaton("""HOA: v1 name: "F(!p0 | X!p1)" States: 3 +Start: 1 AP: 2 "p0" "p1" acc-name: Buchi Acceptance: 1 Inf(0) +properties: trans-labels explicit-labels trans-acc complete +properties: deterministic terminal --BODY-- State: 0 [t] 0 {0} State: +1 [!0] 0 [0] 2 State: 2 [!0 | !1] 0 [0&1] 2 --END--""") +# Erase the first edge of state 1 +oi = a.out_iteraser(1) +oi.erase() +# postprocess used to call reduce_parity that did not +# work correctly on automata with deleted edges. +sm = a.postprocess("gen", "small") +assert sm.num_states() == 3