reduce_parity: fix to work on automata with deleted edges
* spot/twaalgos/parity.cc (reduce_parity): Use the size of the edge vector to initialize piprime1 and piprime2, not the number of edges. * tests/python/parity.py: Add test case, based on a report by Yann Thierry-Mieg.
This commit is contained in:
parent
58f33deeca
commit
3f9f6029e7
3 changed files with 25 additions and 5 deletions
5
NEWS
5
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
|
- purge_dead_states() will now also remove edges labeled by false
|
||||||
(except self-loops).
|
(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)
|
New in spot 2.10.4 (2022-02-01)
|
||||||
|
|
||||||
Bug fixed:
|
Bug fixed:
|
||||||
|
|
|
||||||
|
|
@ -1,6 +1,6 @@
|
||||||
// -*- coding: utf-8 -*-
|
// -*- coding: utf-8 -*-
|
||||||
// Copyright (C) 2016, 2018, 2019 Laboratoire de Recherche et Développement
|
// Copyright (C) 2016, 2018, 2019, 2022 Laboratoire de Recherche et
|
||||||
// de l'Epita (LRDE).
|
// Développement de l'Epita (LRDE).
|
||||||
//
|
//
|
||||||
// This file is part of Spot, a model checking library.
|
// This file is part of Spot, a model checking library.
|
||||||
//
|
//
|
||||||
|
|
@ -465,8 +465,9 @@ namespace spot
|
||||||
// using k=0 or k=1.
|
// using k=0 or k=1.
|
||||||
//
|
//
|
||||||
// -2 means the edge was never assigned a color.
|
// -2 means the edge was never assigned a color.
|
||||||
std::vector<int> piprime1(aut->num_edges() + 1, -2); // k=1
|
unsigned evs = aut->edge_vector().size();
|
||||||
std::vector<int> piprime2(aut->num_edges() + 1, -2); // k=0
|
std::vector<int> piprime1(evs, -2); // k=1
|
||||||
|
std::vector<int> piprime2(evs, -2); // k=0
|
||||||
bool sba = aut->prop_state_acc().is_true();
|
bool sba = aut->prop_state_acc().is_true();
|
||||||
|
|
||||||
auto rec =
|
auto rec =
|
||||||
|
|
|
||||||
|
|
@ -1,6 +1,6 @@
|
||||||
#!/usr/bin/python3
|
#!/usr/bin/python3
|
||||||
# -*- mode: python; coding: utf-8 -*-
|
# -*- 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.
|
# l'EPITA.
|
||||||
#
|
#
|
||||||
# This file is part of Spot, a model checking library.
|
# 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)
|
assert "invalid state number" in str(e)
|
||||||
else:
|
else:
|
||||||
report_missing_exception()
|
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
|
||||||
|
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue