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

replace bdd_relprod by bdd_restrict

Browse source 
* spot/twaalgos/alternation.cc, spot/twaalgos/dualize.cc,
spot/twaalgos/simulation.cc, spot/twaalgos/toweak.cc: Here.
This commit is contained in:
Alexandre Duret-Lutz 2022-10-11 10:43:27 +02:00
parent 548f3d7663
commit 583ca38d91
4 changed files with 6 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

4
spot/twaalgos/alternation.cc
View file

@ -457,7 +457,7 @@ namespace spot
// First loop over all possible valuations atomic properties. // First loop over all possible valuations atomic properties.
for (bdd oneletter: minterms_of(all_letters, ap)) for (bdd oneletter: minterms_of(all_letters, ap))
{ {
minato_isop isop(bdd_relprod(bs, oneletter, ap)); minato_isop isop(bdd_restrict(bs, oneletter));
bdd dest; bdd dest;
while ((dest = isop.next()) != bddfalse) while ((dest = isop.next()) != bddfalse)
{ {
@ -636,7 +636,7 @@ namespace spot
cond_ = oneletter; cond_ = oneletter;
all_letters_ -= oneletter; all_letters_ -= oneletter;
// Get a sum of possible transitions matching this letter. // Get a sum of possible transitions matching this letter.
isop_ = minato_isop(bdd_relprod(transitions_, oneletter, ap_)); isop_ = minato_isop(bdd_restrict(transitions_, oneletter));
dest_ = isop_.next(); dest_ = isop_.next();
} }
std::set<unsigned> dest = bdd_to_state(dest_); std::set<unsigned> dest = bdd_to_state(dest_);

2
spot/twaalgos/dualize.cc
View file

@ -155,7 +155,7 @@ namespace spot
for (bdd oneletter: minterms_of(letters, ap)) for (bdd oneletter: minterms_of(letters, ap))
{ {
minato_isop isop(bdd_relprod(delta, oneletter, ap)); minato_isop isop(bdd_restrict(delta, oneletter));
bdd dest; bdd dest;
while ((dest = isop.next()) != bddfalse) while ((dest = isop.next()) != bddfalse)

4
spot/twaalgos/simulation.cc
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*- // -*- coding: utf-8 -*-
// Copyright (C) 2012-2021 Laboratoire de Recherche et Développement // Copyright (C) 2012-2022 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.
@ -590,7 +590,7 @@ namespace spot
// C1 then (!C1)C2, instead of C1 then C2. // C1 then (!C1)C2, instead of C1 then C2.
// With minatop_isop, we ensure that the no negative // With minatop_isop, we ensure that the no negative
// class variable will be seen (likewise for promises). // class variable will be seen (likewise for promises).
minato_isop isop(bdd_relprod(sig, one, sup_all_atomic_prop)); minato_isop isop(bdd_restrict(sig, one));
++nb_minterms; ++nb_minterms;

2
spot/twaalgos/toweak.cc
View file

@ -179,7 +179,7 @@ namespace spot
for (bdd oneletter: minterms_of(letters, ap)) for (bdd oneletter: minterms_of(letters, ap))
{ {
minato_isop isop(bdd_relprod(delta, oneletter, ap)); minato_isop isop(bdd_restrict(delta, oneletter));
bdd dest; bdd dest;
while ((dest = isop.next()) != bddfalse) while ((dest = isop.next()) != bddfalse)