Commit 48028986 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

sccinfo: fix accepting run computation

* 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.
parent da681e6b
...@@ -14,6 +14,9 @@ New in spot 2.10.2.dev (not yet released) ...@@ -14,6 +14,9 @@ New in spot 2.10.2.dev (not yet released)
- Work around GraphViz bug #2179 by avoiding unnecessary empty - Work around GraphViz bug #2179 by avoiding unnecessary empty
lines in the acceptance conditions shown in dot. 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) New in spot 2.10.2 (2021-12-03)
Bugs fixed: Bugs fixed:
......
...@@ -9,6 +9,7 @@ Cambridge Yang ...@@ -9,6 +9,7 @@ Cambridge Yang
Caroline Lemieux Caroline Lemieux
Christian Dax Christian Dax
Christopher Ziegler Christopher Ziegler
Clément Tamines
David Müller David Müller
Ernesto Posse Ernesto Posse
Étienne Renault Étienne Renault
......
// -*- coding: utf-8 -*- // -*- 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). // de l'Epita (LRDE).
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
...@@ -637,8 +637,8 @@ namespace spot ...@@ -637,8 +637,8 @@ namespace spot
const unsigned start = (unsigned)substart; const unsigned start = (unsigned)substart;
// Cycle search // Cycle search
acc_cond actual_cond = acccond.restrict_to(node.acc_marks()) acc_cond::mark_t allc = node.acc_marks();
.force_inf(node.acc_marks()); acc_cond actual_cond = acccond.restrict_to(allc).force_inf(allc);
assert(!actual_cond.uses_fin_acceptance()); assert(!actual_cond.uses_fin_acceptance());
assert(!actual_cond.is_f()); assert(!actual_cond.is_f());
acc_cond::mark_t acc_to_see = actual_cond.accepting_sets(node.acc_marks()); acc_cond::mark_t acc_to_see = actual_cond.accepting_sets(node.acc_marks());
...@@ -650,7 +650,7 @@ namespace spot ...@@ -650,7 +650,7 @@ namespace spot
[&](const twa_graph::edge_storage_t& t) [&](const twa_graph::edge_storage_t& t)
{ {
// Stay in the specified SCC. // 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) [&](const twa_graph::edge_storage_t& t)
{ {
......
# -*- mode: python; coding: utf-8 -*- # -*- 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). # (LRDE).
# #
# This file is part of Spot, a model checking library. # 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} ...@@ -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} State: 1 [0&1] 0 {4 6 7} [0&!1] 1 {3 6} [!0&1] 0 {4 7} [!0&!1] 1 {0}
--END--""") --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): def generic_emptiness2_rec(aut):
spot.cleanup_acceptance_here(aut, False) spot.cleanup_acceptance_here(aut, False)
...@@ -306,4 +315,4 @@ def run_bench(automata): ...@@ -306,4 +315,4 @@ def run_bench(automata):
assert run3.replay(spot.get_cout()) is True 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])
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment