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

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

Browse source 
Because the loops iterate in the opposite order, multiple
test cases need to be adjusted.

* spot/taalgos/tgba2ta.cc, spot/twaalgos/alternation.cc,
spot/twaalgos/dualize.cc, spot/twaalgos/ltl2tgba_fm.cc,
spot/twaalgos/simulation.cc, spot/twaalgos/stutter.cc,
spot/twaalgos/toweak.cc: Replace loops based on
bdd_satonest(x,y,bddtrue) by loops based on minterms_of(x,y).
* tests/core/degenscc.test, tests/core/dualize.test,
tests/core/genltl.test, tests/core/readsave.test,
tests/python/alternation.ipynb, tests/python/automata.ipynb,
tests/python/decompose.ipynb, tests/python/decompose_scc.py,
tests/python/dualize.py, tests/python/sccinfo.py,
tests/python/simstate.py, tests/python/testingaut.ipynb,
tests/python/word.ipynb: Adjust expected test cases.  The
only regression is in genltl.test, but the worsened case
should eventually be fixed as discussed in issue #425 anyway.
This commit is contained in:
Alexandre Duret-Lutz 2021-04-14 17:31:45 +02:00
parent d54dca610e
commit 2a38328a5c
20 changed files with 1315 additions and 1432 deletions
Download patch file Download diff file Expand all files Collapse all files

11
spot/twaalgos/alternation.cc
View file

@ -1,6 +1,6 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2016-2019 Laboratoire de Recherche et Développement
// de l'Epita (LRDE).
// Copyright (C) 2016-2019, 2021 Laboratoire de Recherche et
// Développement de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
//
@ -456,11 +456,8 @@ namespace spot
bdd all_letters = bdd_exist(bs, all_vars_);
// First loop over all possible valuations atomic properties.
while (all_letters != bddfalse)
for (bdd oneletter: minterms_of(all_letters, ap))
{
bdd oneletter = bdd_satoneset(all_letters, ap, bddtrue);
all_letters -= oneletter;
minato_isop isop(bs & oneletter);
bdd cube;
while ((cube = isop.next()) != bddfalse)
@ -637,7 +634,7 @@ namespace spot
// If it was the last transition, try the next letter.
if (transition_ == bddfalse)
{
bdd oneletter = bdd_satoneset(all_letters_, ap_, bddtrue);
bdd oneletter = bdd_satoneset(all_letters_, ap_, bddfalse);
all_letters_ -= oneletter;
// Get a sum of possible transitions matching this letter.
isop_ = minato_isop(oneletter & transitions_);

7
spot/twaalgos/dualize.cc
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2017-2019 Laboratoire de Recherche et Développement
// Copyright (C) 2017-2019, 2021 Laboratoire de Recherche et Développement
// de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
@ -153,11 +153,8 @@ namespace spot
bdd ap = bdd_exist(bdd_support(delta), all_vars_);
bdd letters = bdd_exist(delta, all_vars_);
while (letters != bddfalse)
for (bdd oneletter: minterms_of(letters, ap))
{
bdd oneletter = bdd_satoneset(letters, ap, bddtrue);
letters -= oneletter;
minato_isop isop(delta & oneletter);
bdd cube;

60
spot/twaalgos/ltl2tgba_fm.cc
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2008-2019 Laboratoire de Recherche et Développement
// Copyright (C) 2008-2019, 2021 Laboratoire de Recherche et Développement
// de l'Epita (LRDE).
// Copyright (C) 2003-2006 Laboratoire d'Informatique de Paris 6
// (LIP6), département Systèmes Répartis Coopératifs (SRC), Université
@ -899,11 +899,8 @@ namespace spot
bdd res_det = bddfalse;
bdd var_set = bdd_existcomp(bdd_support(res_ndet), dict_.var_set);
bdd all_props = bdd_existcomp(res_ndet, dict_.var_set);
while (all_props != bddfalse)
for (bdd label: minterms_of(all_props, var_set))
{
bdd label = bdd_satoneset(all_props, var_set, bddtrue);
all_props -= label;
formula dest =
dict_.bdd_to_sere(bdd_appex(res_ndet, label, bddop_and,
dict_.var_set));
@ -998,11 +995,8 @@ namespace spot
// Generate (deterministic) successors
bdd var_set = bdd_existcomp(bdd_support(res), dict_.var_set);
bdd all_props = bdd_existcomp(res, dict_.var_set);
while (all_props != bddfalse)
for (bdd label: minterms_of(all_props, var_set))
{
bdd label = bdd_satoneset(all_props, var_set, bddtrue);
all_props -= label;
formula dest =
dict_.bdd_to_sere(bdd_appex(res, label, bddop_and,
dict_.var_set));
@ -1475,11 +1469,8 @@ namespace spot
{
bdd var_set = bdd_existcomp(bdd_support(f1), dict_.var_set);
bdd all_props = bdd_existcomp(f1, dict_.var_set);
while (all_props != bddfalse)
for (bdd label: minterms_of(all_props, var_set))
{
bdd label = bdd_satoneset(all_props, var_set, bddtrue);
all_props -= label;
formula dest =
dict_.bdd_to_sere(bdd_appex(f1, label, bddop_and,
dict_.var_set));
@ -1559,11 +1550,8 @@ namespace spot
bdd var_set = bdd_existcomp(bdd_support(f1), dict_.var_set);
bdd all_props = bdd_existcomp(f1, dict_.var_set);
bdd missing = !all_props;
while (all_props != bddfalse)
for (bdd label: minterms_of(all_props, var_set))
{
bdd label = bdd_satoneset(all_props, var_set, bddtrue);
all_props -= label;
formula dest =
dict_.bdd_to_sere(bdd_appex(f1, label, bddop_and,
dict_.var_set));
@ -1793,16 +1781,15 @@ namespace spot
if (t.has_rational)
{
bdd res = bddfalse;
bdd var_set = bdd_existcomp(bdd_support(t.symbolic), d_.var_set);
bdd all_props = bdd_existcomp(t.symbolic, d_.var_set);
while (all_props != bddfalse)
bdd var_set = bddtrue;
bdd all_props = bddtrue;
if (d_.exprop)
{
var_set = bdd_existcomp(bdd_support(t.symbolic), d_.var_set);
all_props = bdd_existcomp(t.symbolic, d_.var_set);
}
for (bdd one_prop_set: minterms_of(all_props, var_set))
{
bdd one_prop_set = bddtrue;
if (d_.exprop)
one_prop_set = bdd_satoneset(all_props, var_set, bddtrue);
all_props -= one_prop_set;
minato_isop isop(t.symbolic & one_prop_set);
bdd cube;
while ((cube = isop.next()) != bddfalse)
@ -2110,24 +2097,21 @@ namespace spot
dests.clear();
// Compute all outgoing arcs.
// If EXPROP is set, we will refine the symbolic
// representation of the successors for all combinations of
// the atomic properties involved in the formula.
// VAR_SET is the set of these properties.
bdd var_set = bdd_existcomp(bdd_support(res), d.var_set);
// ALL_PROPS is the combinations we have yet to consider.
// We used to start with `all_props = bddtrue', but it is
// more efficient to start with the set of all satisfiable
// variables combinations.
bdd all_props = bdd_existcomp(res, d.var_set);
while (all_props != bddfalse)
// ALL_PROPS is the satisfiable combinations of VAR_SET to consider.
bdd var_set = bddtrue;
bdd all_props = bddtrue;
if (exprop)
{
bdd one_prop_set = bddtrue;
if (exprop)
one_prop_set = bdd_satoneset(all_props, var_set, bddtrue);
all_props -= one_prop_set;
var_set = bdd_existcomp(bdd_support(res), d.var_set);
all_props = bdd_existcomp(res, d.var_set);
}
for (bdd one_prop_set: minterms_of(all_props, var_set))
{
// Compute prime implicants.
// The reason we use prime implicants and not bdd_satone()
// is that we do not want to get any negation in front of Next

19
spot/twaalgos/simulation.cc
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2012-2020 Laboratoire de Recherche et Développement
// Copyright (C) 2012-2021 Laboratoire de Recherche et Développement
// de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
@ -538,7 +538,7 @@ namespace spot
stat.states = bdd_lstate_.size();
stat.edges = 0;
unsigned nb_satoneset = 0;
unsigned nb_minterms = 0;
unsigned nb_minato = 0;
auto all_inf = all_inf_;
@ -573,24 +573,19 @@ namespace spot
bdd all_atomic_prop = bdd_exist(sig, nonapvars);
// First loop over all possible valuations atomic properties.
while (all_atomic_prop != bddfalse)
for (bdd one: minterms_of(all_atomic_prop, sup_all_atomic_prop))
{
bdd one = bdd_satoneset(all_atomic_prop,
sup_all_atomic_prop,
bddtrue);
all_atomic_prop -= one;
// For each possible valuation, iterate over all possible
// destination classes. We use minato_isop here, because
// if the same valuation of atomic properties can go
// to two different classes C1 and C2, iterating on
// C1 + C2 with the above bdd_satoneset loop will see
// C1 + C2 with the above minters_of loop will see
// 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);
++nb_satoneset;
++nb_minterms;
bdd cond_acc_dest;
while ((cond_acc_dest = isop.next()) != bddfalse)
@ -750,8 +745,8 @@ namespace spot
true, // stutter inv.
});
// !unambiguous and !semi-deterministic are not preserved
if (!Cosimulation && nb_minato == nb_satoneset)
// Note that nb_minato != nb_satoneset does not imply
if (!Cosimulation && nb_minato == nb_minterms)
// Note that nb_minato != nb_minterms does not imply
// non-deterministic, because of the merge_edges() above.
res->prop_universal(true);
if (Sba)

13
spot/twaalgos/stutter.cc
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2014-2020 Laboratoire de Recherche et Développement de
// Copyright (C) 2014-2021 Laboratoire de Recherche et Développement de
// l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
@ -187,7 +187,7 @@ namespace spot
void
next_edge()
{
one_ = bdd_satoneset(cond_, aps_, bddtrue);
one_ = bdd_satoneset(cond_, aps_, bddfalse);
cond_ -= one_;
if (need_loop_ && (state_->cond() == one_)
&& (state_ == it_->dst()))
@ -313,11 +313,8 @@ namespace spot
for (auto& t : a->out(s.first))
{
bdd all = t.cond;
while (all != bddfalse)
for (bdd one: minterms_of(t.cond, atomic_propositions))
{
bdd one = bdd_satoneset(all, atomic_propositions, bddtrue);
all -= one;
stutter_state d(t.dst, one);
auto r = ss2num.emplace(d, ss2num.size());
@ -408,10 +405,8 @@ namespace spot
// Do not use td in the loop because the new_edge()
// might invalidate it.
auto acc = td.acc;
while (all != bddfalse)
for (bdd one: minterms_of(all, atomic_propositions))
{
bdd one = bdd_satoneset(all, atomic_propositions, bddtrue);
all -= one;
// Skip if there is a loop for this particular letter.
if (bdd_implies(one, selfloops[src])
|| bdd_implies(one, selfloops[dst]))

7
spot/twaalgos/toweak.cc
View file

@ -1,5 +1,5 @@
// -*- 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).
//
// This file is part of Spot, a model checking library.
@ -177,11 +177,8 @@ namespace spot
bdd ap = bdd_exist(bdd_support(delta), all_states_);
bdd letters = bdd_exist(delta, all_states_);
while (letters != bddfalse)
for (bdd oneletter: minterms_of(letters, ap))
{
bdd oneletter = bdd_satoneset(letters, ap, bddtrue);
letters -= oneletter;
minato_isop isop(delta & oneletter);
bdd cube;