diff --git a/NEWS b/NEWS index db1db6ac1..271d6cacb 100644 --- a/NEWS +++ b/NEWS @@ -242,6 +242,10 @@ New in spot 2.9.7.dev (not yet released) - tgba_determinize() could create parity automata using more colors than necessary. (Related to issue #298) + - left->intersacting_run(right) could return a run with incorrect + colors (likely not corresponding to any existing transition of + left) if left was a weak automaton. + Deprecation notices: - twa_graph::defrag_states() and digraph::defrag_states() now take diff --git a/spot/twa/twa.cc b/spot/twa/twa.cc index bebcbddfa..986aeb397 100644 --- a/spot/twa/twa.cc +++ b/spot/twa/twa.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2011, 2014-2019 Laboratoire de Recherche et Developpement de -// l'EPITA (LRDE). +// Copyright (C) 2011, 2014-2019, 2021 Laboratoire de Recherche et +// Developpement de l'EPITA (LRDE). // Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. @@ -165,7 +165,14 @@ namespace spot { const_twa_graph_ptr g1 = ensure_existential_twa_graph(self); const_twa_graph_ptr g2 = ensure_existential_twa_graph(other); + // Reset g1.prop_weak() to disable the product optimization + // for weak automata, otherwise project(g1) would be unable to + // compute the correct marks. See issue #471. It's OK to + // optimize the right part if g2 is weak. + spot::trival g1weak = g1->prop_weak(); + std::const_pointer_cast(g1)->prop_weak(false); auto run = generic_accepting_run(product(g1, g2)); + std::const_pointer_cast(g1)->prop_weak(g1weak); if (!run) return nullptr; return run->reduce()->project(g1); diff --git a/tests/Makefile.am b/tests/Makefile.am index c0708f8b5..25be5e855 100644 --- a/tests/Makefile.am +++ b/tests/Makefile.am @@ -380,6 +380,7 @@ TESTS_ipython = \ TESTS_python = \ python/298.py \ python/341.py \ + python/471.py \ python/_altscc.ipynb \ python/_autparserr.ipynb \ python/_aux.ipynb \ diff --git a/tests/python/471.py b/tests/python/471.py new file mode 100644 index 000000000..6fee3a2d3 --- /dev/null +++ b/tests/python/471.py @@ -0,0 +1,28 @@ +# -*- mode: python; coding: utf-8 -*- +# Copyright (C) 2021 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 . + +# Test for Issue #471. + +import spot +a = spot.translate('Fa') +a = spot.to_generalized_rabin(a, False) +r1 = a.intersecting_run(a) +r2 = a.accepting_run() +assert str(r1) == str(r2) +assert a.prop_weak().is_true()