alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

sccinfo: fix accepting run computation

Browse source 
* spot/twaalgos/sccinfo.cc (scc_info::get_accepting_run): Ignore edges
whose colors are not part of the colors gathered in the SCC up to
deciding acceptance.
* tests/python/genem.py: New test case, reported by Clément Tamines.
* THANKS: Add him.
* NEWS: Mention the bug.
This commit is contained in:
Alexandre Duret-Lutz 2022-01-14 15:46:53 +01:00
parent 890423936f
commit fc92c88cdb
4 changed files with 19 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

3
NEWS
View file

@ -36,6 +36,9 @@ New in spot 2.10.2.dev (not yet released)
- Work around GraphViz bug #2179 by avoiding unnecessary empty
lines in the acceptance conditions shown in dot.
- Fix a case where generic_accepting_run() incorrectly returns a
cycle around a rejecting self-loop.
New in spot 2.10.2 (2021-12-03)
Bugs fixed:

1
THANKS
View file

@ -9,6 +9,7 @@ Cambridge Yang
Caroline Lemieux
Christian Dax
Christopher Ziegler
Clément Tamines
David Müller
Ernesto Posse
Étienne Renault

8
spot/twaalgos/sccinfo.cc
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2014-2021 Laboratoire de Recherche et Développement
// Copyright (C) 2014-2022 Laboratoire de Recherche et Développement
// de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
@ -637,8 +637,8 @@ namespace spot
const unsigned start = (unsigned)substart;
// Cycle search
acc_cond actual_cond = acccond.restrict_to(node.acc_marks())
.force_inf(node.acc_marks());
acc_cond::mark_t allc = node.acc_marks();
acc_cond actual_cond = acccond.restrict_to(allc).force_inf(allc);
assert(!actual_cond.uses_fin_acceptance());
assert(!actual_cond.is_f());
acc_cond::mark_t acc_to_see = actual_cond.accepting_sets(node.acc_marks());
@ -650,7 +650,7 @@ namespace spot
[&](const twa_graph::edge_storage_t& t)
{
// Stay in the specified SCC.
return scc_of(t.dst) != scc || filter(t);
return scc_of(t.dst) != scc || filter(t) || !t.acc.subset(allc);
},
[&](const twa_graph::edge_storage_t& t)
{

13
tests/python/genem.py
View file

@ -1,5 +1,5 @@
# -*- mode: python; coding: utf-8 -*-
# Copyright (C) 2018-2021 Laboratoire de Recherche et Développement de l'Epita
# Copyright (C) 2018-2022 Laboratoire de Recherche et Développement de l'Epita
# (LRDE).
#
# This file is part of Spot, a model checking library.
@ -138,6 +138,15 @@ State: 0 [0&1] 0 {4 6 7} [0&!1] 1 {0 6} [!0&1] 0 {3 7} [!0&!1] 0 {0}
State: 1 [0&1] 0 {4 6 7} [0&!1] 1 {3 6} [!0&1] 0 {4 7} [!0&!1] 1 {0}
--END--""")
# From Clément Tamines (2022-01-14)
act = spot.automaton("""HOA: v1 States: 5 Start: 0 AP: 1 "p0"
acc-name: none Acceptance: 8 (Inf(6) | Fin(7)) & (Inf(4) | Fin(5)) &
(Inf(2) | Fin(3)) & (Inf(0) | Fin(1)) properties: trans-labels
explicit-labels trans-acc --BODY-- State: 0 [!0] 1 {1 2 5 6} [!0] 3 {0
2 5 6} State: 1 [!0] 4 {1 3 5 6} [0] 3 {0 2 4 7} [!0] 1 {0 2 4 7}
State: 2 [0] 2 {1 2 5 6} [0] 1 {0 3 4 6} [!0] 4 {0 2 4 6} State: 3
[!0] 2 {0 3 5 7} State: 4 [!0] 2 {0 3 4 6} --END--""")
def generic_emptiness2_rec(aut):
spot.cleanup_acceptance_here(aut, False)
@ -306,4 +315,4 @@ def run_bench(automata):
assert run3.replay(spot.get_cout()) is True
run_bench([a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a360])
run_bench([a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a360, act])