diff --git a/spot/twaalgos/alternation.cc b/spot/twaalgos/alternation.cc index a3762f9b0..8370f395b 100644 --- a/spot/twaalgos/alternation.cc +++ b/spot/twaalgos/alternation.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2016-2019, 2021 Laboratoire de Recherche et +// Copyright (C) 2016-2019, 2021, 2022 Laboratoire de Recherche et // Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -457,12 +457,10 @@ namespace spot // First loop over all possible valuations atomic properties. for (bdd oneletter: minterms_of(all_letters, ap)) { - minato_isop isop(bs & oneletter); - bdd cube; - while ((cube = isop.next()) != bddfalse) + minato_isop isop(bdd_relprod(bs, oneletter, ap)); + bdd dest; + while ((dest = isop.next()) != bddfalse) { - bdd cond = bdd_exist(cube, all_vars_); - bdd dest = bdd_existcomp(cube, all_vars_); v.clear(); acc_cond::mark_t m = bdd_to_state(dest, v); @@ -491,7 +489,7 @@ namespace spot unsigned d = new_state(v, has_mark); if (has_mark) m.set(0); - res->new_edge(s, d, cond, all_marks - m); + res->new_edge(s, d, oneletter, all_marks - m); } } } @@ -576,7 +574,8 @@ namespace spot bdd all_states_; bdd ap_; bdd all_letters_; - bdd transition_; + bdd dest_; + bdd cond_; minato_isop isop_; const std::map& var_to_state_; univ_remover_state* dst_; @@ -587,8 +586,8 @@ namespace spot const std::vector& state_to_var, const std::map& var_to_state, bdd all_states) - : transitions_(bddtrue), all_states_(all_states), transition_(bddfalse), - isop_(bddfalse), var_to_state_(var_to_state) + : transitions_(bddtrue), all_states_(all_states), dest_(bddfalse), + cond_(bddfalse), isop_(bddfalse), var_to_state_(var_to_state) { // Build the bdd transitions_, from which we extract the successors. for (unsigned s : state->states()) @@ -627,20 +626,20 @@ namespace spot void one_transition() { - transition_ = isop_.next(); - if (transition_ != bddfalse || all_letters_ != bddfalse) + dest_ = isop_.next(); + if (dest_ != bddfalse || all_letters_ != bddfalse) { // If it was the last transition, try the next letter. - if (transition_ == bddfalse) + if (dest_ == bddfalse) { bdd oneletter = bdd_satoneset(all_letters_, ap_, bddfalse); + cond_ = oneletter; all_letters_ -= oneletter; // Get a sum of possible transitions matching this letter. - isop_ = minato_isop(oneletter & transitions_); - transition_ = isop_.next(); + isop_ = minato_isop(bdd_relprod(transitions_, oneletter, ap_)); + dest_ = isop_.next(); } - bdd dest_bdd = bdd_exist(transition_, ap_); - std::set dest = bdd_to_state(dest_bdd); + std::set dest = bdd_to_state(dest_); dst_ = new univ_remover_state(dest); } } @@ -648,18 +647,18 @@ namespace spot virtual bool first() override { one_transition(); - return transition_ != bddfalse; + return dest_ != bddfalse; } virtual bool next() override { one_transition(); - return transition_ != bddfalse; + return dest_ != bddfalse; } virtual bool done() const override { - return transition_ == bddfalse && all_letters_ == bddfalse; + return dest_ == bddfalse && all_letters_ == bddfalse; } virtual const state* dst() const override @@ -669,7 +668,7 @@ namespace spot virtual bdd cond() const override { - return bdd_exist(transition_, all_states_); + return cond_; } virtual acc_cond::mark_t acc() const override diff --git a/spot/twaalgos/dualize.cc b/spot/twaalgos/dualize.cc index e42822740..91498ce8d 100644 --- a/spot/twaalgos/dualize.cc +++ b/spot/twaalgos/dualize.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2017-2019, 2021 Laboratoire de Recherche et Développement -// de l'Epita (LRDE). +// Copyright (C) 2017-2019, 2021-2022 Laboratoire de Recherche et +// Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -155,14 +155,11 @@ namespace spot for (bdd oneletter: minterms_of(letters, ap)) { - minato_isop isop(delta & oneletter); - bdd cube; + minato_isop isop(bdd_relprod(delta, oneletter, ap)); + bdd dest; - while ((cube = isop.next()) != bddfalse) + while ((dest = isop.next()) != bddfalse) { - bdd cond = bdd_exist(cube, all_vars_); - bdd dest = bdd_existcomp(cube, all_vars_); - st.clear(); acc_cond::mark_t m = bdd_to_state(dest, st); if (st.empty()) @@ -171,7 +168,7 @@ namespace spot if (aut_->prop_state_acc()) m = aut_->state_acc_sets(i); } - res->new_univ_edge(i, st.begin(), st.end(), cond, m); + res->new_univ_edge(i, st.begin(), st.end(), oneletter, m); } } } diff --git a/spot/twaalgos/simulation.cc b/spot/twaalgos/simulation.cc index e62762489..58ebfd79d 100644 --- a/spot/twaalgos/simulation.cc +++ b/spot/twaalgos/simulation.cc @@ -590,7 +590,7 @@ namespace spot // C1 then (!C1)C2, instead of C1 then C2. // With minatop_isop, we ensure that the no negative // class variable will be seen (likewise for promises). - minato_isop isop(sig & one); + minato_isop isop(bdd_relprod(sig, one, sup_all_atomic_prop)); ++nb_minterms; @@ -603,17 +603,12 @@ namespace spot // Take the edge, and keep only the variable which // are used to represent the class. - bdd dst = bdd_existcomp(cond_acc_dest, - all_class_var_); + bdd dst = bdd_existcomp(cond_acc_dest, all_class_var_); // Keep only ones who are acceptance condition. auto acc = bdd_to_mark(bdd_existcomp(cond_acc_dest, all_proms_)); - // Keep the other! - bdd cond = bdd_existcomp(cond_acc_dest, - sup_all_atomic_prop); - // Because we have complemented all the Inf // acceptance conditions on the input automaton, // we must revert them to create a new edge. @@ -630,11 +625,11 @@ namespace spot accst[srcst] = acc; acc = {}; } - gb->new_edge(dst.id(), src.id(), cond, acc); + gb->new_edge(dst.id(), src.id(), one, acc); } else { - gb->new_edge(src.id(), dst.id(), cond, acc); + gb->new_edge(src.id(), dst.id(), one, acc); } } } diff --git a/spot/twaalgos/toweak.cc b/spot/twaalgos/toweak.cc index 8f62477a4..543c7c9a1 100644 --- a/spot/twaalgos/toweak.cc +++ b/spot/twaalgos/toweak.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2017, 2018, 2021 Laboratoire de Recherche et Développement -// de l'Epita (LRDE). +// Copyright (C) 2017, 2018, 2021, 2022 Laboratoire de Recherche et +// Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -179,14 +179,11 @@ namespace spot for (bdd oneletter: minterms_of(letters, ap)) { - minato_isop isop(delta & oneletter); - bdd cube; + minato_isop isop(bdd_relprod(delta, oneletter, ap)); + bdd dest; - while ((cube = isop.next()) != bddfalse) + while ((dest = isop.next()) != bddfalse) { - bdd cond = bdd_exist(cube, all_states_); - bdd dest = bdd_existcomp(cube, all_states_); - states.clear(); while (dest != bddtrue) { @@ -199,7 +196,7 @@ namespace spot } res_->new_univ_edge(new_state(st.id, st.rank, st.mark), states.begin(), states.end(), - cond, mark); + oneletter, mark); } } todo_.pop();