From 2ea7cbe0f532c6481bb8e5dceb0387f75e1b763c Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 2 Jul 2003 14:19:04 +0000 Subject: [PATCH] * src/tgba/tgbabddcoredata.hh (tgba_bdd_core_data::nownext_set): New attribute. * tgba/tgbabddcoredata.cc, tgba/tgbabddtranslatefactory.cc: Handle nownext_set. * src/tgba/succiterconcrete.cc (tgba_succ_iterator_concrete::next): Use nownext_set to simplify. --- ChangeLog | 9 ++++++++- src/tgba/succiterconcrete.cc | 6 +++--- src/tgba/tgbabddcoredata.cc | 8 ++++---- src/tgba/tgbabddcoredata.hh | 4 ++-- src/tgba/tgbabddtranslatefactory.cc | 2 +- 5 files changed, 18 insertions(+), 11 deletions(-) diff --git a/ChangeLog b/ChangeLog index facb6d92e..c215e2739 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,5 +1,12 @@ 2003-07-02 Alexandre Duret-Lutz + * src/tgba/tgbabddcoredata.hh (tgba_bdd_core_data::nownext_set): + New attribute. + * tgba/tgbabddcoredata.cc, tgba/tgbabddtranslatefactory.cc: + Handle nownext_set. + * src/tgba/succiterconcrete.cc + (tgba_succ_iterator_concrete::next): Use nownext_set to simplify. + Rewrite tgba_succ_iterator_concrete::next for the fourth time (or is it the fifth?). @@ -14,7 +21,7 @@ (tgba_succ_iterator_concrete::first): Likewise. (tgba_succ_iterator_concrete::next): Rewrite. * tgba/tgbabddcoredata.hh (tgba_bdd_core_data::acc_set): New attribute. - * tgba/tgbabddcoredata.cc, tgba/tgbabddtranslatefactory.cc: + * tgba/tgbabddcoredata.cc, tgba/tgbabddtranslatefactory.cc: Handle acc_set. 2003-07-01 Alexandre Duret-Lutz diff --git a/src/tgba/succiterconcrete.cc b/src/tgba/succiterconcrete.cc index 0d011a1dd..395fcda01 100644 --- a/src/tgba/succiterconcrete.cc +++ b/src/tgba/succiterconcrete.cc @@ -111,7 +111,7 @@ namespace spot { // AS is false when no transition from ST belongs to // an accepting set. Iterate over ST directly. - trans_set_ = bdd_exist(st, data_.now_set & data_.next_set); + trans_set_ = bdd_exist(st, data_.nownext_set); } else { @@ -119,7 +119,7 @@ namespace spot // only work over a set of transitions sharing the // same accepting set. - as = bdd_exist(as, data_.now_set & data_.next_set); + as = bdd_exist(as, data_.nownext_set); // as = (a | (!a)&b) & (Acc[a] | Acc[b]) + (!a & Acc[b]) bdd cube = bdd_satone(as); // cube = (!ab & Acc[a]) @@ -137,7 +137,7 @@ namespace spot // Pick and remove one satisfaction from trans_set_left_. bdd cube = bdd_satone(trans_set_left_); trans_set_left_ &= !cube; - // Let this cube grow as much as possible. + // Let this cube grow as much as possible. // (e.g., cube "(!a)&b" taken from "a | (!a)&b" can // be simplified to "b"). cube = bdd_simplify(cube, cube | neg_trans_set_); diff --git a/src/tgba/tgbabddcoredata.cc b/src/tgba/tgbabddcoredata.cc index 782510619..9fdf1ae4e 100644 --- a/src/tgba/tgbabddcoredata.cc +++ b/src/tgba/tgbabddcoredata.cc @@ -7,7 +7,7 @@ namespace spot accepting_conditions(bddfalse), now_set(bddtrue), next_set(bddtrue), - negnow_set(bddtrue), + nownext_set(bddtrue), notnow_set(bddtrue), notnext_set(bddtrue), var_set(bddtrue), @@ -25,7 +25,7 @@ namespace spot accepting_conditions(copy.accepting_conditions), now_set(copy.now_set), next_set(copy.next_set), - negnow_set(copy.negnow_set), + nownext_set(copy.nownext_set), notnow_set(copy.notnow_set), notnext_set(copy.notnext_set), var_set(copy.var_set), @@ -46,7 +46,7 @@ namespace spot | right.accepting_conditions), now_set(left.now_set & right.now_set), next_set(left.next_set & right.next_set), - negnow_set(left.negnow_set & right.negnow_set), + nownext_set(left.nownext_set & right.nownext_set), notnow_set(left.notnow_set & right.notnow_set), notnext_set(left.notnext_set & right.notnext_set), var_set(left.var_set & right.var_set), @@ -80,10 +80,10 @@ namespace spot { now_set &= now; next_set &= next; - negnow_set &= !now; notnext_set &= now; notnow_set &= next; bdd both = now & next; + nownext_set &= both; notvar_set &= both; notacc_set &= both; varandnext_set &= next; diff --git a/src/tgba/tgbabddcoredata.hh b/src/tgba/tgbabddcoredata.hh index a978c4b40..344e62b77 100644 --- a/src/tgba/tgbabddcoredata.hh +++ b/src/tgba/tgbabddcoredata.hh @@ -65,8 +65,8 @@ namespace spot bdd now_set; /// The conjunction of all Next variables, in their positive form. bdd next_set; - /// The conjunction of all Now variables, in their negated form. - bdd negnow_set; + /// The conjunction of all Now and Next variables, in their positive form. + bdd nownext_set; /// \brief The (positive) conjunction of all variables which are /// not Now variables. bdd notnow_set; diff --git a/src/tgba/tgbabddtranslatefactory.cc b/src/tgba/tgbabddtranslatefactory.cc index 0e6a6a410..a10fb3b6e 100644 --- a/src/tgba/tgbabddtranslatefactory.cc +++ b/src/tgba/tgbabddtranslatefactory.cc @@ -16,7 +16,7 @@ namespace spot 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_.negnow_set = bdd_replace(in.negnow_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);