From ae10361bddb9a3a858272a272be7ccd34800c677 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Tue, 18 Apr 2023 14:48:10 +0200 Subject: [PATCH] twa_run: let as_twa work on the result of intersecting_run Reported by Philipp Schlehuber-Caissier. * spot/twaalgos/emptiness.cc (as_twa): Simplify considerably. Don't try to replay the run, and don't merge identical states. * spot/twaalgos/word.hh, spot/twaalgos/emptiness.hh: Improve documentation. * tests/python/intrun.py: Add a test case. * NEWS: Mention the bug. --- NEWS | 5 +++ spot/twaalgos/emptiness.cc | 75 +++++++++++--------------------------- spot/twaalgos/emptiness.hh | 6 +-- spot/twaalgos/word.hh | 7 +++- tests/python/intrun.py | 40 +++++++++++++++++++- 5 files changed, 73 insertions(+), 60 deletions(-) diff --git a/NEWS b/NEWS index 37a8ebf88..7fbb4f66a 100644 --- a/NEWS +++ b/NEWS @@ -25,6 +25,11 @@ New in spot 2.11.4.dev (not yet released) - Building from the git repository would fail to report a missing emacs (issue #528). + - Fix exception raised by aut1.intersecting_run(aut2).as_twa() + because the run did not match transitions present in aut1 + verbatim. We also changed the behavior of as_twa() to not merge + identical states. + New in spot 2.11.4 (2023-02-10) Python: diff --git a/spot/twaalgos/emptiness.cc b/spot/twaalgos/emptiness.cc index fd3319141..ef8890f95 100644 --- a/spot/twaalgos/emptiness.cc +++ b/spot/twaalgos/emptiness.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2009, 2011-2019, 2021 Laboratoire de Recherche et +// Copyright (C) 2009, 2011-2019, 2021, 2023 Laboratoire de Recherche et // Développement 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 @@ -570,7 +570,7 @@ namespace spot if (debug) os << "ERROR: First state of run (in " << in << "): " << aut->format_state(i->s) - << "\ndoes not match initial state of automata: " + << "\ndoes not match initial state of automaton: " << aut->format_state(s) << '\n'; s->destroy(); return false; @@ -802,38 +802,38 @@ namespace spot res->set_named_prop("state-names", names); } - const state* s = aut->get_init_state(); unsigned src; unsigned dst; const twa_run::steps* l; - acc_cond::mark_t seen_acc = {}; - - state_map seen; + unsigned cycle_entry = 0; if (prefix.empty()) - l = &cycle; + l = &cycle; else - l = &prefix; + l = &prefix; twa_run::steps::const_iterator i = l->begin(); - assert(s->compare(i->s) == 0); +#if NDEBUG + const state* init = aut->get_init_state(); + assert(init->compare(i->s) == 0); + init->destroy(); +#endif + src = res->new_state(); - seen.emplace(i->s, src); if (names) - names->push_back(aut->format_state(s)); + names->push_back(aut->format_state(i->s)); for (; i != l->end();) { - // expected outgoing transition bdd label = i->label; acc_cond::mark_t acc = i->acc; - // compute the next expected state const state* next; ++i; if (i != l->end()) { + dst = res->new_state(); next = i->s; } else @@ -842,57 +842,24 @@ namespace spot { l = &cycle; i = l->begin(); + cycle_entry = dst = res->new_state(); + } + else + { + dst = cycle_entry; } next = l->begin()->s; } - // browse the actual outgoing transitions and - // look for next; - const state* the_next = nullptr; - for (auto j: aut->succ(s)) + if (names && i != l->end()) { - if (j->cond() != label - || j->acc() != acc) - continue; - - const state* s2 = j->dst(); - if (s2->compare(next) == 0) - { - the_next = s2; - break; - } - s2->destroy(); + assert(dst == names->size()); + names->push_back(aut->format_state(next)); } - s->destroy(); - if (!the_next) - throw std::runtime_error("twa_run::as_twa() unable to replay run"); - s = the_next; - - - auto p = seen.emplace(next, 0); - if (p.second) - { - unsigned ns = res->new_state(); - p.first->second = ns; - if (names) - { - assert(ns == names->size()); - names->push_back(aut->format_state(next)); - } - } - dst = p.first->second; - res->new_edge(src, dst, label, acc); src = dst; - - // Sum acceptance conditions. - if (l == &cycle && i != l->begin()) - seen_acc |= acc; } - s->destroy(); - - assert(aut->acc().accepting(seen_acc)); return res; } diff --git a/spot/twaalgos/emptiness.hh b/spot/twaalgos/emptiness.hh index 47896a1d7..66bf8ca56 100644 --- a/spot/twaalgos/emptiness.hh +++ b/spot/twaalgos/emptiness.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2011, 2013-2018, 2020-2021 Laboratoire de +// Copyright (C) 2011, 2013-2018, 2020-2021, 2023 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 @@ -451,9 +451,9 @@ namespace spot /// Note that this works only if the automaton is a twa_graph_ptr. void highlight(unsigned color); - /// \brief Return a twa_graph_ptr corresponding to \a run + /// \brief Convert the run into a lasso-shaped automaton /// - /// Identical states are merged. + /// This preserves the original acceptance condition. /// /// If \a preserve_names is set, the created states are named /// using the format_state() result from the original state. diff --git a/spot/twaalgos/word.hh b/spot/twaalgos/word.hh index f6f70fc14..979a4070b 100644 --- a/spot/twaalgos/word.hh +++ b/spot/twaalgos/word.hh @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2013, 2014, 2015, 2016, 2018, 2019 Laboratoire de Recherche et -// Développement de l'Epita (LRDE). +// Copyright (C) 2013-2016, 2018-2019, 2023 Laboratoire de Recherche +// et Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -80,6 +80,9 @@ namespace spot /// \brief Convert the twa_word as an automaton. /// + /// Convert the twa_word into a lasso-shapred automaton + /// with "true" acceptance condition. + /// /// This is useful to evaluate a word on an automaton. twa_graph_ptr as_automaton() const; diff --git a/tests/python/intrun.py b/tests/python/intrun.py index e3b708a95..02a7aedd6 100644 --- a/tests/python/intrun.py +++ b/tests/python/intrun.py @@ -1,5 +1,5 @@ # -*- mode: python; coding: utf-8 -*- -# Copyright (C) 2020, 2022 Laboratoire de Recherche et Développement +# Copyright (C) 2020, 2022, 2023 Laboratoire de Recherche et Développement # de l'Epita (LRDE). # # This file is part of Spot, a model checking library. @@ -38,3 +38,41 @@ r = b.intersecting_run(spot.complement(a)); c = spot.twa_word(r).as_automaton() tc.assertTrue(c.intersects(b)) tc.assertFalse(c.intersects(a)) + +# The next test came from Philipp Schlehuber-Caissier: running +# as_twa() on a run built from a A.intersecting_run(B) failed to build +# the automaton because it tried to rebuild the run on A and did not +# find transitions matching exactly. Additionally the idea of merging +# states in as_twa() seems to be a way to create some disasters, so we +# removed that too. +a = spot.translate("a"); +b = spot.translate("{a;1;a}"); +r = a.intersecting_run(b) +tc.assertEqual(str(r), """Prefix: + 1 + | a + 0 + | 1 {0} + 0 + | a {0} +Cycle: + 0 + | 1 {0} +""") +tc.assertEqual(r.as_twa().to_str(), """HOA: v1 +States: 4 +Start: 0 +AP: 1 "a" +acc-name: Buchi +Acceptance: 1 Inf(0) +properties: trans-labels explicit-labels state-acc deterministic +--BODY-- +State: 0 +[0] 1 +State: 1 {0} +[t] 2 +State: 2 {0} +[0] 3 +State: 3 {0} +[t] 3 +--END--""")