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

* src/tgba/tgbabddcoredata.hh (tgba_bdd_core_data::translate): New

Browse source 
function.
* src/tgba/tgbabddcoredata.cc (tgba_bdd_core_data::translate):
Likewise.
* src/tgba/tgbabddtranslatefactory.cc
(tgba_bdd_translate_factory::tgba_bdd_translate_factory): Use
tgba_bdd_core_data::translate.
This commit is contained in:
Alexandre Duret-Lutz 2003-07-02 14:28:06 +00:00
parent 2ea7cbe0f5
commit 0fe98c6d18
4 changed files with 34 additions and 19 deletions
Download patch file Download diff file Expand all files Collapse all files

8
ChangeLog
View file

@ -1,5 +1,13 @@
2003-07-02 Alexandre Duret-Lutz <aduret@src.lip6.fr>
* src/tgba/tgbabddcoredata.hh (tgba_bdd_core_data::translate): New
function.
* src/tgba/tgbabddcoredata.cc (tgba_bdd_core_data::translate):
Likewise.
* src/tgba/tgbabddtranslatefactory.cc
(tgba_bdd_translate_factory::tgba_bdd_translate_factory): Use
tgba_bdd_core_data::translate.
* src/tgba/tgbabddcoredata.hh (tgba_bdd_core_data::nownext_set):
New attribute.
* tgba/tgbabddcoredata.cc, tgba/tgbabddtranslatefactory.cc:

18
src/tgba/tgbabddcoredata.cc
View file

@ -108,4 +108,22 @@ namespace spot
acc_set &= acc;
negacc_set &= !acc;
}
void
tgba_bdd_core_data::translate(bddPair* rewrite)
{
relation = bdd_replace(relation, rewrite);
accepting_conditions = bdd_replace(accepting_conditions, rewrite);
now_set = bdd_replace(now_set, rewrite);
next_set = bdd_replace(next_set, rewrite);
nownext_set = bdd_replace(nownext_set, rewrite);
notnow_set = bdd_replace(notnow_set, rewrite);
notnext_set = bdd_replace(notnext_set, rewrite);
notvar_set = bdd_replace(notvar_set, rewrite);
var_set = bdd_replace(var_set, rewrite);
varandnext_set = bdd_replace(varandnext_set, rewrite);
acc_set = bdd_replace(acc_set, rewrite);
notacc_set = bdd_replace(notacc_set, rewrite);
negacc_set = bdd_replace(negacc_set, rewrite);
}
}

6
src/tgba/tgbabddcoredata.hh
View file

@ -122,6 +122,12 @@ namespace spot
/// \brief Update the variable sets to take a new accepting condition
/// into account.
void declare_accepting_condition(bdd prom);
/// \brief Translate BDD variables.
///
/// Rewrite the variables according to \a rewrite.
/// This used by spot::tgba_bdd_translate_factory.
void translate(bddPair* rewrite);
};
}

21
src/tgba/tgbabddtranslatefactory.cc
View file

@ -6,28 +6,11 @@ namespace spot
{
tgba_bdd_translate_factory::tgba_bdd_translate_factory
(const tgba_bdd_concrete& from, const tgba_bdd_dict& to)
: dict_(to)
: data_(from.get_core_data()), dict_(to)
{
bddPair* rewrite = compute_pairs(from.get_dict());
const tgba_bdd_core_data& in = from.get_core_data();
data_.relation = bdd_replace(in.relation, rewrite);
data_.accepting_conditions = bdd_replace(in.accepting_conditions, rewrite);
data_.now_set = bdd_replace(in.now_set, rewrite);
data_.next_set = bdd_replace(in.next_set, rewrite);
data_.nownext_set = bdd_replace(in.nownext_set, rewrite);
data_.notnow_set = bdd_replace(in.notnow_set, rewrite);
data_.notnext_set = bdd_replace(in.notnext_set, rewrite);
data_.notvar_set = bdd_replace(in.notvar_set, rewrite);
data_.var_set = bdd_replace(in.var_set, rewrite);
data_.varandnext_set = bdd_replace(in.varandnext_set, rewrite);
data_.acc_set = bdd_replace(in.acc_set, rewrite);
data_.notacc_set = bdd_replace(in.notacc_set, rewrite);
data_.negacc_set = bdd_replace(in.negacc_set, rewrite);
data_.translate(rewrite);
init_ = bdd_replace(from.get_init_bdd(), rewrite);
bdd_freepair(rewrite);
}