From d4b8ecdf9049bc8eb175eef0892ff9486102bd93 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 4 Mar 2020 16:41:23 +0100 Subject: [PATCH] genem: fix suboptimal selection of Fin to remove * 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. --- spot/twaalgos/genem.cc | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/spot/twaalgos/genem.cc b/spot/twaalgos/genem.cc index 0fb7f0bb3..5760b6d02 100644 --- a/spot/twaalgos/genem.cc +++ b/spot/twaalgos/genem.cc @@ -1,5 +1,5 @@ // -*- 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). // // This file is part of Spot, a model checking library. @@ -74,7 +74,7 @@ namespace spot } else { - int fo = acc.fin_one(); + int fo = disjunct.fin_one(); assert(fo >= 0); // Try to accept when Fin(fo) == true acc_cond::mark_t fo_m = {(unsigned) fo};