From f2403c91dcebf4d8c43cb0faaf07a9eeea9a5f10 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Fri, 10 Jul 2020 18:05:18 +0200 Subject: [PATCH] run: fix reduce on automata with Fin Reported by Florian Renkin. * spot/twaalgos/emptiness.cc (reduce): If the automaton uses Fin acceptance, check the reduced cycle and revert to the original cycle if necessary. * tests/python/intrun.py: New file. * tests/Makefile.am: Add it. * spot/twaalgos/emptiness.hh: Improve documentation. --- NEWS | 5 +++++ spot/twaalgos/emptiness.cc | 37 +++++++++++++++++++++++++++++-------- spot/twaalgos/emptiness.hh | 8 +++++++- tests/Makefile.am | 1 + tests/python/intrun.py | 38 ++++++++++++++++++++++++++++++++++++++ 5 files changed, 80 insertions(+), 9 deletions(-) create mode 100644 tests/python/intrun.py diff --git a/NEWS b/NEWS index eb833532f..7d8adbe84 100644 --- a/NEWS +++ b/NEWS @@ -61,6 +61,11 @@ New in spot 2.9.0.dev (not yet released) - Improve ltldo diagnostics to fix spurious test-suite failure on systems with antique GNU libc. + - twa_run::reduce() could reduce accepting runs incorrectly on + automata using Fin in their acceptance condition. This caused + issues in intersecting_run(), exclusive_run(), + intersecting_word(), exclusive_word(), which all call reduce(). + New in spot 2.9 (2020-04-30) Command-line tools: diff --git a/spot/twaalgos/emptiness.cc b/spot/twaalgos/emptiness.cc index d07fd938f..5ca65224d 100644 --- a/spot/twaalgos/emptiness.cc +++ b/spot/twaalgos/emptiness.cc @@ -304,11 +304,7 @@ namespace spot { state_set::const_iterator i = seen.begin(); while (i != seen.end()) - { - const state* ptr = *i; - ++i; - ptr->destroy(); - } + (*i++)->destroy(); } void @@ -353,17 +349,19 @@ namespace spot { ensure_non_empty_cycle("twa_run::reduce()"); auto& a = aut; + auto& acc = a->acc(); auto res = std::make_shared(a); state_set ss; shortest_path shpath(a); shpath.set_target(&ss); // We want to find a short segment of the original cycle that - // contains all acceptance conditions. + // satisfies the acceptance condition. const state* segment_start; // The initial state of the segment. const state* segment_next; // The state immediately after the segment. + // Start from the end of the original cycle, and rewind until all // acceptance sets have been seen. acc_cond::mark_t seen_acc = {}; @@ -374,7 +372,7 @@ namespace spot --seg; seen_acc |= seg->acc; } - while (!a->acc().accepting(seen_acc)); + while (!acc.accepting(seen_acc)); segment_start = seg->s; // Now go forward and ends the segment as soon as we have seen all @@ -390,7 +388,7 @@ namespace spot ++seg; } - while (!a->acc().accepting(seen_acc)); + while (!acc.accepting(seen_acc)); segment_next = seg == cycle.end() ? cycle.front().s : seg->s; // Close this cycle if needed, that is, compute a cycle going @@ -402,6 +400,29 @@ namespace spot ss.clear(); assert(s->compare(segment_start) == 0); (void)s; + + // If the acceptance condition uses Fin, it's possible (and + // even quite likely) that the cycle we have constructed this + // way is now rejecting, because the closing steps might add + // unwanted colors. If that is the case, throw the reduced + // cycle away and simply preserve the original one verbatim. + if (acc.uses_fin_acceptance()) + { + acc_cond::mark_t seen = {}; + for (auto& st: res->cycle) + seen |= st.acc; + if (!acc.accepting(seen)) + { + for (auto& st: res->cycle) + st.s->destroy(); + res->cycle.clear(); + for (auto& st: cycle) + { + twa_run::step st2 = { st.s->clone(), st.label, st.acc }; + res->cycle.emplace_back(st2); + } + } + } } // Compute the prefix: it's the shortest path from the initial diff --git a/spot/twaalgos/emptiness.hh b/spot/twaalgos/emptiness.hh index 0ddda3f6d..78eb88477 100644 --- a/spot/twaalgos/emptiness.hh +++ b/spot/twaalgos/emptiness.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2011, 2013, 2014, 2015, 2016, 2017, 2018 Laboratoire de +// Copyright (C) 2011, 2013-2018, 2020 Laboratoire de // Recherche et Developpement de l'Epita (LRDE). // Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre @@ -413,6 +413,12 @@ namespace spot /// /// Return a run which is still accepting for aut, /// but is no longer than this one. + /// + /// This is done by trying to find a fragment of the accepting + /// single that is accepting, and trying to close a cycle around + /// this fragment with fewer edges than in the original cycle. + /// (This step works best in Fin-less automata.) And then trying + /// to find a shorter prefix leading to any state of the cycle. twa_run_ptr reduce() const; /// \brief Project an accepting run diff --git a/tests/Makefile.am b/tests/Makefile.am index b39a54be8..77b8f8ece 100644 --- a/tests/Makefile.am +++ b/tests/Makefile.am @@ -383,6 +383,7 @@ TESTS_python = \ python/genem.py \ python/implies.py \ python/interdep.py \ + python/intrun.py \ python/kripke.py \ python/ltl2tgba.test \ python/ltlf.py \ diff --git a/tests/python/intrun.py b/tests/python/intrun.py new file mode 100644 index 000000000..c86c6d643 --- /dev/null +++ b/tests/python/intrun.py @@ -0,0 +1,38 @@ +# -*- mode: python; coding: utf-8 -*- +# Copyright (C) 2020 Laboratoire de Recherche et Développement de l'Epita +# (LRDE). +# +# This file is part of Spot, a model checking library. +# +# Spot is free software; you can redistribute it and/or modify it +# under the terms of the GNU General Public License as published by +# the Free Software Foundation; either version 3 of the License, or +# (at your option) any later version. +# +# Spot is distributed in the hope that it will be useful, but WITHOUT +# ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +# or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +# License for more details. +# +# You should have received a copy of the GNU General Public License +# along with this program. If not, see . + +import spot + +# This issue was reported by Florian Renkin. The reduce() call used in +# intersecting_run() was bogus, and could incorrectly reduce a word +# intersecting the product into a word not intersecting the product if the +# acceptance condition uses some Fin. +a, b = spot.automata("""HOA: v1 States: 5 Start: 0 AP: 2 "p0" "p1" acc-name: +Rabin 2 Acceptance: 4 (Fin(0) & Inf(1)) | (Fin(2) & Inf(3)) properties: +trans-labels explicit-labels trans-acc complete properties: deterministic +--BODY-- State: 0 [t] 3 State: 1 [t] 4 {1} State: 2 [0] 2 {1} [!0] 1 {0} State: +3 [t] 1 {1} State: 4 [!0&1] 4 {3} [!0&!1] 3 [0] 2 {0} --END-- HOA: v1 States: 5 +Start: 0 AP: 2 "p0" "p1" Acceptance: 3 Inf(2) | (Fin(0) & Inf(1)) properties: +trans-labels explicit-labels trans-acc complete properties: deterministic +--BODY-- State: 0 [t] 3 State: 1 [t] 4 {1 2} State: 2 [0] 2 {1 2} [!0] 1 {0 2} +State: 3 [t] 1 {1 2} State: 4 [!0&1] 4 {2} [!0&!1] 3 {2} [0] 2 {0 2} --END--""") +r = b.intersecting_run(spot.complement(a)); +c = spot.twa_word(r).as_automaton() +assert c.intersects(b) +assert not c.intersects(a)