From 5d2e0a42241937a2291d7ab090e1fe3961b7ed35 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 12 Jun 2003 15:21:33 +0000 Subject: [PATCH] * src/tgba/tgbabddconcrete.cc (set_init_state, succ_iter): Make sure to compute the status of the most Now variables possible. This helps to identify equivalant states. (tgba_bdd_concrete): Call set_init_state. --- ChangeLog | 7 +++++ src/tgba/tgbabddconcrete.cc | 52 ++++++++++++++++++++++++++++++++++++- 2 files changed, 58 insertions(+), 1 deletion(-) diff --git a/ChangeLog b/ChangeLog index b7899024c..81cdf4c41 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,10 @@ +2003-06-12 Alexandre Duret-Lutz + + * src/tgba/tgbabddconcrete.cc (set_init_state, succ_iter): Make + sure to compute the status of the most Now variables possible. + This helps to identify equivalant states. + (tgba_bdd_concrete): Call set_init_state. + 2003-06-10 Alexandre Duret-Lutz * src/tgba/ltl2tgba.cc (ltl_trad_visitor::visit): Handle F and G. diff --git a/src/tgba/tgbabddconcrete.cc b/src/tgba/tgbabddconcrete.cc index 58ef6b8b6..42da30774 100644 --- a/src/tgba/tgbabddconcrete.cc +++ b/src/tgba/tgbabddconcrete.cc @@ -10,8 +10,9 @@ namespace spot } tgba_bdd_concrete::tgba_bdd_concrete(const tgba_bdd_factory& fact, bdd init) - : data_(fact.get_core_data()), dict_(fact.get_dict()), init_(init) + : data_(fact.get_core_data()), dict_(fact.get_dict()) { + set_init_state(init); } tgba_bdd_concrete::~tgba_bdd_concrete() @@ -21,6 +22,40 @@ namespace spot void tgba_bdd_concrete::set_init_state(bdd s) { + // Usually, the ltl2tgba translator will return an + // initial state which does not include all true Now variables, + // even though the truth of some Now variables is garanteed. + // + // For instance, when building the automata for the formula GFa, + // the translator will define the following two equivalences + // Now[Fa] <=> a | (Prom[a] & Next[Fa]) + // Now[GFa] <=> Now[Fa] & Next[GFa] + // and return Now[GFa] as initial state. + // + // Starting for state Now[GFa], we could then build + // the following automaton: + // In state Now[GFa]: + // if `a', go to state Now[GFa] + // if True, go to state Now[GFa] & Now[Fa] with Prom[a] + // In state Now[GFa] & Now[Fa]: + // if `a', go to state Now[GFa] + // if True, go to state Now[GFa] & Now[Fa] with Prom[a] + // + // As we can see, states Now[GFa] and Now[GFa] & Now[Fa] share + // the same actions. This is no surprise, because + // Now[GFa] <=> Now[GFa] & Now[Fa] according to the equivalences + // defined by the translator. + // + // What sounds bogus is that we dissociated the two states: + // there should be only one, so that the automaton become + // + // In state Now[GFa] & Now[Fa]: + // if `a', go to state Now[GFa] & Now[GFa] + // if True, go to state Now[GFa] & Now[Fa] with Prom[a] + // + // To achieve this, we immerse the state into the relation + // to collect the status of other Now variables. + s &= bdd_relprod(s, data_.relation, data_.notnow_set); init_ = s; } @@ -44,6 +79,21 @@ namespace spot bdd succ_set = bdd_replace(bdd_exist(data_.relation & s->as_bdd(), data_.now_set), data_.next_to_now); + + // Immerse known Now variables into the relation to compute the + // status of any other Now variables. See the comment in + // set_init_state for the rational. Note that unlike + // set_init_state, we work only from the Now variables, not from + // any other atomic propositions around. This is because the Now + // variables and the atomic propositions do not correspond to the + // same instant: atomic propositions describe what we must verify + // now while Now variables describe the state where we go (and + // where something else we have to be checked) -- actually these + // Now variables are really Next variables renammed for + // convenience. + succ_set &= bdd_relprod(bdd_exist(succ_set, data_.notnow_set), + data_.relation, data_.notnow_set); + return new tgba_succ_iterator_concrete(data_, succ_set); }