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

simulation: remove unnecessary iteration

Browse source 
This fixes #442.

* spot/twaalgos/simulation.cc (iterated_simulations_): Initialize next
so that we can exit after the first iteration if no change was made.
* NEWS: Mention the bug.
This commit is contained in:
Alexandre Duret-Lutz 2020-11-24 16:24:44 +01:00
parent fb224d3f63
commit 97eedd7c5c
2 changed files with 8 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

4
NEWS
View file

@ -152,6 +152,10 @@ New in spot 2.9.5.dev (not yet released)
- twa_graph::merge_edges() could fail to merge two transitions if the - twa_graph::merge_edges() could fail to merge two transitions if the
destination transition was the first of the automaton. (Issue #441) destination transition was the first of the automaton. (Issue #441)
- On non-deterministic automata, iterated_simulations() was
performing an (unnecessary) second iteration even when the first
one failed to reduce the automaton. (Issue #442)
New in spot 2.9.5 (2020-11-19) New in spot 2.9.5 (2020-11-19)
Bugs fixed: Bugs fixed:

8
spot/twaalgos/simulation.cc
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*- // -*- coding: utf-8 -*-
// Copyright (C) 2012-2019 Laboratoire de Recherche et Développement // Copyright (C) 2012-2020 Laboratoire de Recherche et Développement
// de l'Epita (LRDE). // de l'Epita (LRDE).
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
@ -70,13 +70,13 @@ namespace spot
{ {
} }
automaton_size(const twa_graph_ptr& a) automaton_size(const const_twa_graph_ptr& a)
: edges(a->num_edges()), : edges(a->num_edges()),
states(a->num_states()) states(a->num_states())
{ {
} }
void set_size(const twa_graph_ptr& a) void set_size(const const_twa_graph_ptr& a)
{ {
states = a->num_states(); states = a->num_states();
edges = a->num_edges(); edges = a->num_edges();
@ -920,7 +920,7 @@ namespace spot
{ {
twa_graph_ptr res = nullptr; twa_graph_ptr res = nullptr;
automaton_size prev; automaton_size prev;
automaton_size next; automaton_size next(t);
do do
{ {