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

use bdd_have_common_assignment in more places

Browse source 
* spot/twaalgos/gfguarantee.cc, spot/twaalgos/isdet.cc: Use it.
This commit is contained in:
Alexandre Duret-Lutz 2021-07-30 12:05:21 +02:00
parent a6aa799a17
commit 3614cf34a8
2 changed files with 3 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

2
spot/twaalgos/gfguarantee.cc
View file

@ -260,7 +260,7 @@ namespace spot
// history further. // history further.
if (hlen > 0) if (hlen > 0)
for (auto& ei: aut->out(moved_init)) for (auto& ei: aut->out(moved_init))
if ((ei.cond & econd) != bddfalse if (bdd_have_common_assignment(ei.cond, econd)
&& term[si.scc_of(ei.dst)]) && term[si.scc_of(ei.dst)])
goto failed; goto failed;

4
spot/twaalgos/isdet.cc
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*- // -*- coding: utf-8 -*-
// Copyright (C) 2012-2018 Laboratoire de Recherche et Développement // Copyright (C) 2012-2018, 2021 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.
@ -132,7 +132,7 @@ namespace spot
// Second pass to gather the relevant edges. // Second pass to gather the relevant edges.
if (!universal) if (!universal)
for (auto& t: aut->out(src)) for (auto& t: aut->out(src))
if ((t.cond & extra) != bddfalse) if (bdd_have_common_assignment(t.cond, extra))
(*highlight)[aut->get_graph().index_of_edge(t)] = color; (*highlight)[aut->get_graph().index_of_edge(t)] = color;
} }
aut->prop_universal(universal); aut->prop_universal(universal);