From fc92c88cdbc6382bbb1e80dbcf1e8bb66da34b0c Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Fri, 14 Jan 2022 15:46:53 +0100 Subject: [PATCH] sccinfo: fix accepting run computation MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit * 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. --- NEWS | 3 +++ THANKS | 1 + spot/twaalgos/sccinfo.cc | 8 ++++---- tests/python/genem.py | 13 +++++++++++-- 4 files changed, 19 insertions(+), 6 deletions(-) diff --git a/NEWS b/NEWS index b56c83f78..29f70cd4c 100644 --- a/NEWS +++ b/NEWS @@ -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: diff --git a/THANKS b/THANKS index cd1a8be60..c526bf75e 100644 --- a/THANKS +++ b/THANKS @@ -9,6 +9,7 @@ Cambridge Yang Caroline Lemieux Christian Dax Christopher Ziegler +Clément Tamines David Müller Ernesto Posse Étienne Renault diff --git a/spot/twaalgos/sccinfo.cc b/spot/twaalgos/sccinfo.cc index c31999c37..7d82c6b81 100644 --- a/spot/twaalgos/sccinfo.cc +++ b/spot/twaalgos/sccinfo.cc @@ -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) { diff --git a/tests/python/genem.py b/tests/python/genem.py index efc0a84a8..5da9ce85c 100644 --- a/tests/python/genem.py +++ b/tests/python/genem.py @@ -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])