alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

twa: fix intersecting_run on weak automata

Browse source 
Fixes #471, reported by Cambridge Yang.

* spot/twa/twa.cc (intersecting_run): Disable the product
optimization for weak automata.
* tests/python/471.py: New file.
* tests/Makefile.am: Add it.
* NEWS: Mention the bug.
This commit is contained in:
Alexandre Duret-Lutz 2021-07-07 18:00:41 +02:00
parent 09e4ab74a1
commit 0509263f82
4 changed files with 42 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

4
NEWS
View file

@ -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

11
spot/twa/twa.cc
View file

@ -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<twa_graph>(g1)->prop_weak(false);
auto run = generic_accepting_run(product(g1, g2));
std::const_pointer_cast<twa_graph>(g1)->prop_weak(g1weak);
if (!run)
return nullptr;
return run->reduce()->project(g1);

1
tests/Makefile.am
View file

@ -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 \

28
tests/python/471.py Normal file
View file

@ -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 <http://www.gnu.org/licenses/>.
# 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()