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

genem: fix suboptimal selection of Fin to remove

Browse source 
* spot/twaalgos/genem.cc: If a disjunct has no unit-Fin to remove the
code should select any Fin occuring in the disjunct, but it was
selecting any Fin occuring in the acceptance condition (made of
disjuncts) instead.  This could potentially double the number of
recursive calls.
This commit is contained in:
Alexandre Duret-Lutz 2020-03-04 16:41:23 +01:00
parent c98f82dc36
commit 3820f369b0
1 changed files with 2 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

6
spot/twaalgos/genem.cc
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*- // -*- coding: utf-8 -*-
// Copyright (C) 2017-2019 Laboratoire de Recherche et Developpement // Copyright (C) 2017-2020 Laboratoire de Recherche et Developpement
// 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.
@ -74,9 +74,7 @@ namespace spot
} }
else else
{ {
int fo = acc.fin_one(); int fo = disjunct.fin_one();
if (fo < 0)
std::cerr << autacc << acc << '\n';
assert(fo >= 0); assert(fo >= 0);
// Try to accept when Fin(fo) == true // Try to accept when Fin(fo) == true
acc_cond::mark_t fo_m = {(unsigned) fo}; acc_cond::mark_t fo_m = {(unsigned) fo};