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

replace bdd_satoneset(x,y,bddfalse) loops by minterms_of(x,y)

Browse source 
This replaces loops of the form

   while (all != bddfalse) {
      bdd one = bdd_satoneset(all, sup, bddfalse);
      all -= one;
      // ... use one ...
   }

by the more efficient

   for (bdd one: minterms_of(all, sub))
      // ... use one ...

This patch only focues on loops where the third
argument of bdd_satoneset is bddfalse.

* spot/twaalgos/cobuchi.cc, spot/twaalgos/complement.cc,
spot/twaalgos/determinize.cc, spot/twaalgos/dtbasat.cc,
spot/twaalgos/dtwasat.cc, spot/twaalgos/hoa.cc,
spot/twaalgos/powerset.cc: Improve bdd_satoneset()-based loops.
*
This commit is contained in:
Alexandre Duret-Lutz 2021-04-12 19:07:25 +02:00
parent f3c42596aa
commit d54dca610e
7 changed files with 93 additions and 163 deletions
Download patch file Download diff file Expand all files Collapse all files

21
spot/twaalgos/cobuchi.cc
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*- // -*- coding: utf-8 -*-
// Copyright (C) 2017-2018 Laboratoire de Recherche et Développement // Copyright (C) 2017-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.
@ -426,13 +426,11 @@ namespace spot
ap_(aut->ap_vars()) ap_(aut->ap_vars())
{ {
// Get all bdds. // Get all bdds.
bdd all = bddtrue; unsigned i = 0;
for (unsigned i = 0; all != bddfalse; ++i) for (bdd one: minterms_of(bddtrue, ap_))
{ {
bdd one = bdd_satoneset(all, ap_, bddfalse);
num2bdd_.push_back(one); num2bdd_.push_back(one);
bdd2num_[one] = i; bdd2num_[one] = i++;
all -= one;
} }
} }
@ -455,15 +453,8 @@ namespace spot
{ {
size_t base = src * nc; size_t base = src * nc;
for (auto& t: aut_->out(src)) for (auto& t: aut_->out(src))
{ for (bdd one: minterms_of(t.cond, ap_))
bdd all = t.cond; bv_aut_trans_->at(base + bdd2num_[one]).set(t.dst);
while (all != bddfalse)
{
bdd one = bdd_satoneset(all, ap_, bddfalse);
all -= one;
bv_aut_trans_->at(base + bdd2num_[one]).set(t.dst);
}
}
} }
trace << "All_states:\n" << *bv_aut_trans_ << '\n'; trace << "All_states:\n" << *bv_aut_trans_ << '\n';

15
spot/twaalgos/complement.cc
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*- // -*- coding: utf-8 -*-
// Copyright (C) 2013-2015, 2017-2020 Laboratoire de Recherche et // Copyright (C) 2013-2015, 2017-2021 Laboratoire de Recherche et
// Développement de l'Epita. // Développement de l'Epita.
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
@ -484,15 +484,10 @@ namespace spot
{0}); {0});
} }
} }
while (all != bddfalse) for (bdd one: minterms_of(all, msupport))
{ // Compute all new states available from the generated
bdd one = bdd_satoneset(all, msupport, bddfalse); // letter.
all -= one; ncsb_successors(std::move(ms), top.second, one);
// Compute all new states available from the generated
// letter.
ncsb_successors(std::move(ms), top.second, one);
}
} }
res_->merge_edges(); res_->merge_edges();

23
spot/twaalgos/determinize.cc
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*- // -*- coding: utf-8 -*-
// Copyright (C) 2015-2020 Laboratoire de Recherche et // Copyright (C) 2015-2021 Laboratoire de Recherche et
// Développement de l'Epita. // Développement de l'Epita.
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
@ -548,21 +548,6 @@ namespace spot
return res; return res;
} }
// Compute a vector of letters from a given support
std::vector<bdd>
letters(const bdd& allap)
{
std::vector<bdd> res;
bdd all = bddtrue;
while (all != bddfalse)
{
bdd one = bdd_satoneset(all, allap, bddfalse);
all -= one;
res.emplace_back(one);
}
return res;
}
class safra_support class safra_support
{ {
const std::vector<bdd>& state_supports; const std::vector<bdd>& state_supports;
@ -579,7 +564,11 @@ namespace spot
supp &= state_supports[n.first]; supp &= state_supports[n.first];
auto i = cache.emplace(supp, std::vector<bdd>()); auto i = cache.emplace(supp, std::vector<bdd>());
if (i.second) // insertion took place if (i.second) // insertion took place
i.first->second = letters(supp); {
std::vector<bdd>& res = i.first->second;
for (bdd one: minterms_of(bddtrue, supp))
res.emplace_back(one);
}
return i.first->second; return i.first->second;
} }
}; };

74
spot/twaalgos/dtbasat.cc
View file

@ -1,6 +1,6 @@
// -*- coding: utf-8 -*- // -*- coding: utf-8 -*-
// Copyright (C) 2013-2018 Laboratoire de Recherche // Copyright (C) 2013-2018, 2021 Laboratoire de Recherche et
// et Développement de l'Epita. // Développement de l'Epita.
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
// //
@ -272,17 +272,16 @@ namespace spot
} }
// Fill dict's bdd vetor (alpha_vect) and save each bdd and it's // Fill dict's bdd vetor (alpha_vect) and save each bdd and it's
// corresponding index in alpha_map. This is necessary beacause some // corresponding index in alpha_map. This is necessary beacause
// loops start from a precise bdd. Therefore, it's useful to know // some loops start from a precise bdd. Therefore, it's useful
// it's corresponding index to deal with vars_helper. // to know its corresponding index to deal with vars_helper.
bdd all = bddtrue; unsigned j = 0;
for (unsigned j = 0; all != bddfalse; ++j) for (bdd one: minterms_of(bddtrue, ap))
{ {
bdd one = bdd_satoneset(all, ap, bddfalse); d.alpha_vect.push_back(one);
d.alpha_vect.push_back(one); d.alpha_map[d.alpha_vect[j]] = j;
d.alpha_map[d.alpha_vect[j]] = j; ++j;
all -= one; }
}
// Initialize vars_helper by giving it all the necessary information. // Initialize vars_helper by giving it all the necessary information.
// 1: nacc_size is 1 (with Büchi) | true: means dtbasat, i-e, not dtwasat. // 1: nacc_size is 1 (with Büchi) | true: means dtbasat, i-e, not dtwasat.
@ -389,24 +388,18 @@ namespace spot
for (auto& tr: ref->out(q1p)) for (auto& tr: ref->out(q1p))
{ {
unsigned dp = tr.dst; unsigned dp = tr.dst;
bdd all = tr.cond; for (bdd s: minterms_of(tr.cond, ap))
while (all != bddfalse) for (unsigned q2 = 0; q2 < d.cand_size; q2++)
{ {
bdd s = bdd_satoneset(all, ap, bddfalse); int prev = d.pathid_ref(q1, q1p, q1, q1p);
all -= s; int succ = d.pathid_ref(q2, dp, q2, dp);
if (prev == succ)
continue;
for (unsigned q2 = 0; q2 < d.cand_size; q2++) cnf_comment(prev, "∧", d.fmt_t(q1, s, q2), "δ →",
{ d.fmt_p(q2, dp, q2, dp), '\n');
int prev = d.pathid_ref(q1, q1p, q1, q1p); solver.add({-prev, -d.transid(q1, s, q2), succ, 0});
int succ = d.pathid_ref(q2, dp, q2, dp); }
if (prev == succ)
continue;
cnf_comment(prev, "∧", d.fmt_t(q1, s, q2), "δ →",
d.fmt_p(q2, dp, q2, dp), '\n');
solver.add({-prev, -d.transid(q1, s, q2), succ, 0});
}
}
} }
} }
} }
@ -452,11 +445,8 @@ namespace spot
{ {
if (dp == q1p && q3 == q1) // (4) looping if (dp == q1p && q3 == q1) // (4) looping
{ {
bdd all = tr.cond; for (bdd s: minterms_of(tr.cond, ap))
while (all != bddfalse)
{ {
bdd s = bdd_satoneset(all, ap, bddfalse);
all -= s;
#if TRACE #if TRACE
std::string f_t = d.fmt_t(q2, s, q1); std::string f_t = d.fmt_t(q2, s, q1);
cnf_comment(f_p, "R ∧", f_t, "δ → ¬", f_t, cnf_comment(f_p, "R ∧", f_t, "δ → ¬", f_t,
@ -474,12 +464,8 @@ namespace spot
if (pid1 == pid2) if (pid1 == pid2)
continue; continue;
bdd all = tr.cond; for (bdd s: minterms_of(tr.cond, ap))
while (all != bddfalse)
{ {
bdd s = bdd_satoneset(all, ap, bddfalse);
all -= s;
cnf_comment(f_p, "R ∧", d.fmt_t(q2, s, q3), cnf_comment(f_p, "R ∧", d.fmt_t(q2, s, q3),
"δ →", d.fmt_p(q1, q1p, q3, dp), "δ →", d.fmt_p(q1, q1p, q3, dp),
"R\n"); "R\n");
@ -539,11 +525,8 @@ namespace spot
// it is accepting in the reference. // it is accepting in the reference.
if (!ra.accepting(tr.acc)) if (!ra.accepting(tr.acc))
continue; continue;
bdd all = tr.cond; for (bdd s: minterms_of(tr.cond, ap))
while (all != bddfalse)
{ {
bdd s = bdd_satoneset(all, ap, bddfalse);
all -= s;
#if TRACE #if TRACE
std::string f_t = d.fmt_t(q2, s, q1); std::string f_t = d.fmt_t(q2, s, q1);
cnf_comment(f_p, "C ∧", f_t, "δ →", f_t, cnf_comment(f_p, "C ∧", f_t, "δ →", f_t,
@ -561,11 +544,8 @@ namespace spot
if (pid1 == pid2) if (pid1 == pid2)
continue; continue;
bdd all = tr.cond; for (bdd s: minterms_of(tr.cond, ap))
while (all != bddfalse)
{ {
bdd s = bdd_satoneset(all, ap, bddfalse);
all -= s;
#if TRACE #if TRACE
std::string f_t = d.fmt_t(q2, s, q3); std::string f_t = d.fmt_t(q2, s, q3);
cnf_comment(f_p, "C ∧", f_t, "δ ∧ ¬", f_t, cnf_comment(f_p, "C ∧", f_t, "δ ∧ ¬", f_t,

50
spot/twaalgos/dtwasat.cc
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*- // -*- coding: utf-8 -*-
// Copyright (C) 2013-2020 Laboratoire de Recherche // Copyright (C) 2013-2021 Laboratoire de Recherche
// et Développement de l'Epita. // et Développement de l'Epita.
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
@ -501,16 +501,15 @@ namespace spot
} }
// Fill dict's bdd vetor (alpha_vect) and save each bdd and it's // Fill dict's bdd vetor (alpha_vect) and save each bdd and it's
// corresponding index in alpha_map. This is necessary beacause some // corresponding index in alpha_map. This is necessary beacause
// loops start from a precise bdd. Therefore, it's useful to know // some loops start from a precise bdd. Therefore, it's useful
// it's corresponding index to deal with vars_helper. // to know its corresponding index to deal with vars_helper.
bdd all = bddtrue; unsigned j = 0;
for (unsigned j = 0; all != bddfalse; ++j) for (bdd one: minterms_of(bddtrue, ap))
{ {
bdd one = bdd_satoneset(all, ap, bddfalse);
d.alpha_vect.push_back(one); d.alpha_vect.push_back(one);
d.alpha_map[d.alpha_vect[j]] = j; d.alpha_map[d.alpha_vect[j]] = j;
all -= one; ++j;
} }
// Initialize vars_helper by giving it all the necessary information. // Initialize vars_helper by giving it all the necessary information.
@ -670,24 +669,17 @@ namespace spot
for (auto& tr: ref->out(q1p)) for (auto& tr: ref->out(q1p))
{ {
unsigned dp = tr.dst; unsigned dp = tr.dst;
bdd all = tr.cond; for (bdd s: minterms_of(tr.cond, ap))
while (all != bddfalse) for (unsigned q2 = 0; q2 < d.cand_size; ++q2)
{ {
bdd s = bdd_satoneset(all, ap, bddfalse); int succ = d.pathid(q2, dp, q2, dp);
all -= s; if (p1id == succ)
continue;
for (unsigned q2 = 0; q2 < d.cand_size; ++q2) cnf_comment(d.fmt_p(q1, q1p, q1, q1p), " ∧ ",
{ d.fmt_t(q1, s, q2), "δ → ",
int succ = d.pathid(q2, dp, q2, dp); d.fmt_p(q2, dp, q2, dp), '\n');
if (p1id == succ) solver.add({-p1id, -d.transid(q1, s, q2), succ, 0});
continue; }
cnf_comment(d.fmt_p(q1, q1p, q1, q1p), " ∧ ",
d.fmt_t(q1, s, q2), "δ → ",
d.fmt_p(q2, dp, q2, dp), '\n');
solver.add({-p1id, -d.transid(q1, s, q2), succ, 0});
}
}
} }
} }
@ -738,13 +730,9 @@ namespace spot
for (unsigned q3 = 0; q3 < d.cand_size; ++q3) for (unsigned q3 = 0; q3 < d.cand_size; ++q3)
{ {
bdd all = tr.cond;
acc_cond::mark_t curacc = tr.acc; acc_cond::mark_t curacc = tr.acc;
while (all != bddfalse) for (bdd l: minterms_of(tr.cond, ap))
{ {
bdd l = bdd_satoneset(all, ap, bddfalse);
all -= l;
int ti = d.transid(q2, l, q3); int ti = d.transid(q2, l, q3);
if (dp == q1p && q3 == q1) // (11,12) loop if (dp == q1p && q3 == q1) // (11,12) loop
{ {

51
spot/twaalgos/hoa.cc
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*- // -*- coding: utf-8 -*-
// Copyright (C) 2014-2020 Laboratoire de Recherche et // Copyright (C) 2014-2021 Laboratoire de Recherche et
// Developpement de l'Epita (LRDE). // Developpement de l'Epita (LRDE).
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
@ -710,33 +710,28 @@ namespace spot
else else
{ {
for (auto& t: aut->out(i)) for (auto& t: aut->out(i))
{ for (bdd one: minterms_of(t.cond, md.all_ap))
bdd cond = t.cond; {
while (cond != bddfalse) unsigned level = 1;
{ unsigned pos = 0U;
bdd one = bdd_satoneset(cond, md.all_ap, bddfalse); while (one != bddtrue)
cond -= one; {
unsigned level = 1; bdd h = bdd_high(one);
unsigned pos = 0U; if (h == bddfalse)
while (one != bddtrue) {
{ one = bdd_low(one);
bdd h = bdd_high(one); }
if (h == bddfalse) else
{ {
one = bdd_low(one); pos |= level;
} one = h;
else }
{ level <<= 1;
pos |= level; }
one = h; out[pos] = t.dst;
} if (this_acc != Hoa_Acceptance_States)
level <<= 1; outm[pos] = t.acc;
} }
out[pos] = t.dst;
if (this_acc != Hoa_Acceptance_States)
outm[pos] = t.acc;
}
}
unsigned n = out.size(); unsigned n = out.size();
for (unsigned i = 0; i < n;) for (unsigned i = 0; i < n;)
{ {

22
spot/twaalgos/powerset.cc
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*- // -*- coding: utf-8 -*-
// Copyright (C) 2009-2011, 2013-2019 Laboratoire de Recherche et // Copyright (C) 2009-2011, 2013-2019, 2021 Laboratoire de Recherche et
// Développement de l'Epita (LRDE). // Développement de l'Epita (LRDE).
// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6), // Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre // département Systèmes Répartis Coopératifs (SRC), Université Pierre
@ -96,12 +96,9 @@ namespace spot
std::vector<bdd> num2bdd; std::vector<bdd> num2bdd;
num2bdd.reserve(1UL << nap); num2bdd.reserve(1UL << nap);
std::map<bdd, unsigned, bdd_less_than> bdd2num; std::map<bdd, unsigned, bdd_less_than> bdd2num;
bdd all = bddtrue;
bdd allap = aut->ap_vars(); bdd allap = aut->ap_vars();
while (all != bddfalse) for (bdd one: minterms_of(bddtrue, allap))
{ {
bdd one = bdd_satoneset(all, allap, bddfalse);
all -= one;
bdd2num.emplace(one, num2bdd.size()); bdd2num.emplace(one, num2bdd.size());
num2bdd.emplace_back(one); num2bdd.emplace_back(one);
} }
@ -183,16 +180,11 @@ namespace spot
for (unsigned i = 0; i < nc; ++i) for (unsigned i = 0; i < nc; ++i)
bv->at(base + i).clear_all(); bv->at(base + i).clear_all();
for (auto& t: aut->out(src)) for (auto& t: aut->out(src))
{ for (bdd one: minterms_of(t.cond, allap))
bdd all = t.cond; {
while (all != bddfalse) unsigned num = bdd2num[one];
{ bv->at(base + num).set(t.dst);
bdd one = bdd_satoneset(all, allap, bddfalse); }
all -= one;
unsigned num = bdd2num[one];
bv->at(base + num).set(t.dst);
}
}
assert(idx == lru.begin()->first); assert(idx == lru.begin()->first);
return idx; return idx;