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

simplify some uses of minato_isop

Browse source 
Typically intead of doing

    minato_isop isop(rel & letter);
    while (bdd cube = isop.next()) {
       bdd res = bdd_exists(cube, ap)
       ...
    }

do

    minato_isop isop(bdd_relprod(rel, letter, ap);
    while (bdd res = isop.next()) {
       ...
    }

this way the existential quantification is done once at the same time
of the conjunction, and isop has fewer variable to work with.

* 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-09-21 14:04:18 +02:00
parent c45ff0c94c
commit aa7992c65f
4 changed files with 36 additions and 48 deletions
Download patch file Download diff file Expand all files Collapse all files

41
spot/twaalgos/alternation.cc
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*- // -*- 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). // Développement de l'Epita (LRDE).
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
@ -457,12 +457,10 @@ 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(bs & oneletter); minato_isop isop(bdd_relprod(bs, oneletter, ap));
bdd cube; 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_);
v.clear(); v.clear();
acc_cond::mark_t m = bdd_to_state(dest, v); acc_cond::mark_t m = bdd_to_state(dest, v);
@ -491,7 +489,7 @@ namespace spot
unsigned d = new_state(v, has_mark); unsigned d = new_state(v, has_mark);
if (has_mark) if (has_mark)
m.set(0); 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 all_states_;
bdd ap_; bdd ap_;
bdd all_letters_; bdd all_letters_;
bdd transition_; bdd dest_;
bdd cond_;
minato_isop isop_; minato_isop isop_;
const std::map<int, unsigned>& var_to_state_; const std::map<int, unsigned>& var_to_state_;
univ_remover_state* dst_; univ_remover_state* dst_;
@ -587,8 +586,8 @@ namespace spot
const std::vector<int>& state_to_var, const std::vector<int>& state_to_var,
const std::map<int, unsigned>& var_to_state, const std::map<int, unsigned>& var_to_state,
bdd all_states) bdd all_states)
: transitions_(bddtrue), all_states_(all_states), transition_(bddfalse), : transitions_(bddtrue), all_states_(all_states), dest_(bddfalse),
isop_(bddfalse), var_to_state_(var_to_state) cond_(bddfalse), isop_(bddfalse), var_to_state_(var_to_state)
{ {
// Build the bdd transitions_, from which we extract the successors. // Build the bdd transitions_, from which we extract the successors.
for (unsigned s : state->states()) for (unsigned s : state->states())
@ -627,20 +626,20 @@ namespace spot
void one_transition() void one_transition()
{ {
transition_ = isop_.next(); dest_ = isop_.next();
if (transition_ != bddfalse || all_letters_ != bddfalse) if (dest_ != bddfalse || all_letters_ != bddfalse)
{ {
// If it was the last transition, try the next letter. // If it was the last transition, try the next letter.
if (transition_ == bddfalse) if (dest_ == bddfalse)
{ {
bdd oneletter = bdd_satoneset(all_letters_, ap_, bddfalse); bdd oneletter = bdd_satoneset(all_letters_, ap_, bddfalse);
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(oneletter & transitions_); isop_ = minato_isop(bdd_relprod(transitions_, oneletter, ap_));
transition_ = isop_.next(); dest_ = isop_.next();
} }
bdd dest_bdd = bdd_exist(transition_, ap_); std::set<unsigned> dest = bdd_to_state(dest_);
std::set<unsigned> dest = bdd_to_state(dest_bdd);
dst_ = new univ_remover_state(dest); dst_ = new univ_remover_state(dest);
} }
} }
@ -648,18 +647,18 @@ namespace spot
virtual bool first() override virtual bool first() override
{ {
one_transition(); one_transition();
return transition_ != bddfalse; return dest_ != bddfalse;
} }
virtual bool next() override virtual bool next() override
{ {
one_transition(); one_transition();
return transition_ != bddfalse; return dest_ != bddfalse;
} }
virtual bool done() const override virtual bool done() const override
{ {
return transition_ == bddfalse && all_letters_ == bddfalse; return dest_ == bddfalse && all_letters_ == bddfalse;
} }
virtual const state* dst() const override virtual const state* dst() const override
@ -669,7 +668,7 @@ namespace spot
virtual bdd cond() const override virtual bdd cond() const override
{ {
return bdd_exist(transition_, all_states_); return cond_;
} }
virtual acc_cond::mark_t acc() const override virtual acc_cond::mark_t acc() const override

15
spot/twaalgos/dualize.cc
View file

@ -1,6 +1,6 @@
// -*- coding: utf-8 -*- // -*- coding: utf-8 -*-
// Copyright (C) 2017-2019, 2021 Laboratoire de Recherche et Développement // Copyright (C) 2017-2019, 2021-2022 Laboratoire de Recherche et
// de l'Epita (LRDE). // Développement de l'Epita (LRDE).
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
// //
@ -155,14 +155,11 @@ namespace spot
for (bdd oneletter: minterms_of(letters, ap)) for (bdd oneletter: minterms_of(letters, ap))
{ {
minato_isop isop(delta & oneletter); minato_isop isop(bdd_relprod(delta, oneletter, ap));
bdd cube; 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(); st.clear();
acc_cond::mark_t m = bdd_to_state(dest, st); acc_cond::mark_t m = bdd_to_state(dest, st);
if (st.empty()) if (st.empty())
@ -171,7 +168,7 @@ namespace spot
if (aut_->prop_state_acc()) if (aut_->prop_state_acc())
m = aut_->state_acc_sets(i); 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);
} }
} }
} }

13
spot/twaalgos/simulation.cc
View file

@ -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(sig & one); minato_isop isop(bdd_relprod(sig, one, sup_all_atomic_prop));
++nb_minterms; ++nb_minterms;
@ -603,17 +603,12 @@ namespace spot
// Take the edge, and keep only the variable which // Take the edge, and keep only the variable which
// are used to represent the class. // are used to represent the class.
bdd dst = bdd_existcomp(cond_acc_dest, bdd dst = bdd_existcomp(cond_acc_dest, all_class_var_);
all_class_var_);
// Keep only ones who are acceptance condition. // Keep only ones who are acceptance condition.
auto acc = bdd_to_mark(bdd_existcomp(cond_acc_dest, auto acc = bdd_to_mark(bdd_existcomp(cond_acc_dest,
all_proms_)); all_proms_));
// Keep the other!
bdd cond = bdd_existcomp(cond_acc_dest,
sup_all_atomic_prop);
// Because we have complemented all the Inf // Because we have complemented all the Inf
// acceptance conditions on the input automaton, // acceptance conditions on the input automaton,
// we must revert them to create a new edge. // we must revert them to create a new edge.
@ -630,11 +625,11 @@ namespace spot
accst[srcst] = acc; accst[srcst] = acc;
acc = {}; acc = {};
} }
gb->new_edge(dst.id(), src.id(), cond, acc); gb->new_edge(dst.id(), src.id(), one, acc);
} }
else else
{ {
gb->new_edge(src.id(), dst.id(), cond, acc); gb->new_edge(src.id(), dst.id(), one, acc);
} }
} }
} }

15
spot/twaalgos/toweak.cc
View file

@ -1,6 +1,6 @@
// -*- coding: utf-8 -*- // -*- coding: utf-8 -*-
// Copyright (C) 2017, 2018, 2021 Laboratoire de Recherche et Développement // Copyright (C) 2017, 2018, 2021, 2022 Laboratoire de Recherche et
// de l'Epita (LRDE). // Développement de l'Epita (LRDE).
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
// //
@ -179,14 +179,11 @@ namespace spot
for (bdd oneletter: minterms_of(letters, ap)) for (bdd oneletter: minterms_of(letters, ap))
{ {
minato_isop isop(delta & oneletter); minato_isop isop(bdd_relprod(delta, oneletter, ap));
bdd cube; 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(); states.clear();
while (dest != bddtrue) while (dest != bddtrue)
{ {
@ -199,7 +196,7 @@ namespace spot
} }
res_->new_univ_edge(new_state(st.id, st.rank, st.mark), res_->new_univ_edge(new_state(st.id, st.rank, st.mark),
states.begin(), states.end(), states.begin(), states.end(),
cond, mark); oneletter, mark);
} }
} }
todo_.pop(); todo_.pop();