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

* src/tgba/tgbabddcoredata.cc (tgba_bdd_core_data::tgba_bdd_core_data,

Browse source 
tgba_bdd_core_data::translate): Handle all_accepting_conditions.
* src/tgba/tgbabddconcretefactory.cc
(tgba_bdd_concrete_factory::finish): Fill all_accepting_conditions.
This commit is contained in:
Alexandre Duret-Lutz 2003-07-07 09:34:15 +00:00
parent bca9d83c44
commit f754d1112d
3 changed files with 17 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

7
ChangeLog
View file

@ -1,3 +1,10 @@
2003-07-07 Alexandre Duret-Lutz <aduret@src.lip6.fr>
* src/tgba/tgbabddcoredata.cc (tgba_bdd_core_data::tgba_bdd_core_data,
tgba_bdd_core_data::translate): Handle all_accepting_conditions.
* src/tgba/tgbabddconcretefactory.cc
(tgba_bdd_concrete_factory::finish): Fill all_accepting_conditions.
2003-07-04 Alexandre Duret-Lutz <aduret@src.lip6.fr>
* src/tgbaalgos/ltl2tgba.cc (ltl_trad_visitor::visit): Declare

5
src/tgba/tgbabddconcretefactory.cc
View file

@ -105,6 +105,11 @@ namespace spot
// Any state matching the BDD formulae registered is part
// of this accepting set.
data_.accepting_conditions |= ai->second & acc;
// Keep track of all accepting conditions, so that we can
// easily check whether a transition satisfies all accepting
// conditions.
data_.all_accepting_conditions |= acc;
}
// Any constraint between Now variables also exist between Next

5
src/tgba/tgbabddcoredata.cc
View file

@ -5,6 +5,7 @@ namespace spot
tgba_bdd_core_data::tgba_bdd_core_data()
: relation(bddtrue),
accepting_conditions(bddfalse),
all_accepting_conditions(bddfalse),
now_set(bddtrue),
next_set(bddtrue),
nownext_set(bddtrue),
@ -23,6 +24,7 @@ namespace spot
tgba_bdd_core_data::tgba_bdd_core_data(const tgba_bdd_core_data& copy)
: relation(copy.relation),
accepting_conditions(copy.accepting_conditions),
all_accepting_conditions(copy.all_accepting_conditions),
now_set(copy.now_set),
next_set(copy.next_set),
nownext_set(copy.nownext_set),
@ -44,6 +46,8 @@ namespace spot
: relation(left.relation & right.relation),
accepting_conditions(left.accepting_conditions
| right.accepting_conditions),
all_accepting_conditions(left.all_accepting_conditions
| right.all_accepting_conditions),
now_set(left.now_set & right.now_set),
next_set(left.next_set & right.next_set),
nownext_set(left.nownext_set & right.nownext_set),
@ -114,6 +118,7 @@ namespace spot
{
relation = bdd_replace(relation, rewrite);
accepting_conditions = bdd_replace(accepting_conditions, rewrite);
all_accepting_conditions = bdd_replace(all_accepting_conditions, rewrite);
now_set = bdd_replace(now_set, rewrite);
next_set = bdd_replace(next_set, rewrite);
nownext_set = bdd_replace(nownext_set, rewrite);