From f754d1112d1ce93f0e1f0d3ea9f1c7f86f4c2485 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Mon, 7 Jul 2003 09:34:15 +0000 Subject: [PATCH] * 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. --- ChangeLog | 7 +++++++ src/tgba/tgbabddconcretefactory.cc | 5 +++++ src/tgba/tgbabddcoredata.cc | 5 +++++ 3 files changed, 17 insertions(+) diff --git a/ChangeLog b/ChangeLog index eed333f51..15d382649 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,10 @@ +2003-07-07 Alexandre Duret-Lutz + + * 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 * src/tgbaalgos/ltl2tgba.cc (ltl_trad_visitor::visit): Declare diff --git a/src/tgba/tgbabddconcretefactory.cc b/src/tgba/tgbabddconcretefactory.cc index f2600297b..a92fda890 100644 --- a/src/tgba/tgbabddconcretefactory.cc +++ b/src/tgba/tgbabddconcretefactory.cc @@ -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 diff --git a/src/tgba/tgbabddcoredata.cc b/src/tgba/tgbabddcoredata.cc index 8b540ca1e..0c0a0d010 100644 --- a/src/tgba/tgbabddcoredata.cc +++ b/src/tgba/tgbabddcoredata.cc @@ -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);