diff --git a/NEWS b/NEWS index 0ac838737..9775339fe 100644 --- a/NEWS +++ b/NEWS @@ -4,6 +4,12 @@ New in spot 2.11.3.dev (not yet released) - spot.acd() no longer depends on jQuery for interactivity. + Bug fixes: + + - When merging initial states from state-based automata with + multiple initial states (because Spot supports only one), the HOA + parser could break state-based acceptance. (Issue #522.) + New in spot 2.11.3 (2022-12-09) Bug fixes: diff --git a/THANKS b/THANKS index 356d187a1..93155f9d1 100644 --- a/THANKS +++ b/THANKS @@ -48,6 +48,7 @@ Nikos Gorogiannis Ondřej Lengál Paul Guénézan Pierre Ganty +Raven Beutner Reuben Rowe Roei Nahum Rüdiger Ehlers diff --git a/spot/parseaut/parseaut.yy b/spot/parseaut/parseaut.yy index 4d96b8c1c..7d5fac361 100644 --- a/spot/parseaut/parseaut.yy +++ b/spot/parseaut/parseaut.yy @@ -1,5 +1,5 @@ /* -*- coding: utf-8 -*- -** Copyright (C) 2014-2022 Laboratoire de Recherche et Développement +** Copyright (C) 2014-2023 Laboratoire de Recherche et Développement ** de l'Epita (LRDE). ** ** This file is part of Spot, a model checking library. @@ -2610,7 +2610,7 @@ static void fix_initial_state(result_& r) start.resize(std::distance(start.begin(), res)); assert(start.size() >= 1); - if (start.size() == 1) + if (start.size() == 1) { if (r.opts.want_kripke) r.h->ks->set_init_state(start.front().front()); @@ -2627,13 +2627,13 @@ static void fix_initial_state(result_& r) "a single initial state"); return; } + auto& aut = r.h->aut; // Fiddling with initial state may turn an incomplete automaton // into a complete one. - if (r.complete.is_false()) - r.complete = spot::trival::maybe(); + if (aut->prop_complete().is_false()) + aut->prop_complete(spot::trival::maybe()); // Multiple initial states. We might need to add a fake one, // unless one of the actual initial state has no incoming edge. - auto& aut = r.h->aut; std::vector has_incoming(aut->num_states(), 0); for (auto& t: aut->edges()) for (unsigned ud: aut->univ_dests(t)) @@ -2672,6 +2672,9 @@ static void fix_initial_state(result_& r) { unsigned p = pp.front(); if (p != init) + // FIXME: If p has no incoming we should be able to + // change the source of the edges of p instead of + // adding new edges. for (auto& t: aut->out(p)) aut->new_edge(init, t.dst, t.cond); } @@ -2694,6 +2697,24 @@ static void fix_initial_state(result_& r) } combiner.new_dests(init, comb_or); } + + // Merging two states may break state-based acceptance + // make sure all outgoing edges have the same color. + if (aut->prop_state_acc().is_true()) + { + bool first = true; + spot::acc_cond::mark_t prev; + for (auto& e: aut->out(init)) + if (first) + { + first = false; + prev = e.acc; + } + else if (e.acc != prev) + { + e.acc = prev; + } + } } } @@ -2871,8 +2892,8 @@ namespace spot r.aut_or_ks->set_named_prop("aliases", p); } fix_acceptance(r); + fix_properties(r); // before fix_initial_state fix_initial_state(r); - fix_properties(r); if (r.h->aut && !r.h->aut->is_existential()) r.h->aut->merge_univ_dests(); return r.h; diff --git a/tests/Makefile.am b/tests/Makefile.am index 4c2fe830c..8a180ddda 100644 --- a/tests/Makefile.am +++ b/tests/Makefile.am @@ -1,5 +1,5 @@ ## -*- coding: utf-8 -*- -## Copyright (C) 2009-2022 Laboratoire de Recherche et Développement +## Copyright (C) 2009-2023 Laboratoire de Recherche et Développement ## de l'Epita (LRDE). ## Copyright (C) 2003-2006 Laboratoire d'Informatique de Paris 6 ## (LIP6), département Systèmes Répartis Coopératifs (SRC), Université @@ -223,6 +223,7 @@ TESTS_misc = \ TESTS_twa = \ core/385.test \ core/521.test \ + core/522.test \ core/acc.test \ core/acc2.test \ core/bdddict.test \ diff --git a/tests/core/522.test b/tests/core/522.test new file mode 100755 index 000000000..5fe6ba945 --- /dev/null +++ b/tests/core/522.test @@ -0,0 +1,43 @@ +#!/bin/sh +# -*- coding: utf-8 -*- +# Copyright (C) 2023 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 . + +. ./defs + +set -e + +# For issue #522. + +cat >552.hoa < out.hoa +grep 'States: 7' out.hoa