From 8e51474fa2ae95a03966395d2bf383468487e7a5 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 19 Jun 2003 14:26:42 +0000 Subject: [PATCH] * src/tgba/tgbabddconcrete.cc (set_init_state, succ_iter): Revert the change from 2003-06-12, it needs more work (the automaton generated on Xa&(b U !a) was bogus, with that patch). --- ChangeLog | 7 ++++- src/tgba/tgbabddconcrete.cc | 52 +------------------------------------ 2 files changed, 7 insertions(+), 52 deletions(-) diff --git a/ChangeLog b/ChangeLog index e2ce1cd94..5deb113d9 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,7 +1,12 @@ 2003-06-19 Alexandre Duret-Lutz + * src/tgba/tgbabddconcrete.cc (set_init_state, succ_iter): + Revert the change from 2003-06-12, it needs more work (the + automaton generated on Xa&(b U !a) was bogus, with that + patch). + * src/tgbatest/ltl2tgba.cc: Handle the -o and -r options. - + * src/tgbatest/tripprod.test, src/tgbatest/explprod.test, src/tgbatest/readsave.test: Adjust to reflect yesterday's bddprint.cc change. diff --git a/src/tgba/tgbabddconcrete.cc b/src/tgba/tgbabddconcrete.cc index 42da30774..58ef6b8b6 100644 --- a/src/tgba/tgbabddconcrete.cc +++ b/src/tgba/tgbabddconcrete.cc @@ -10,9 +10,8 @@ namespace spot } tgba_bdd_concrete::tgba_bdd_concrete(const tgba_bdd_factory& fact, bdd init) - : data_(fact.get_core_data()), dict_(fact.get_dict()) + : data_(fact.get_core_data()), dict_(fact.get_dict()), init_(init) { - set_init_state(init); } tgba_bdd_concrete::~tgba_bdd_concrete() @@ -22,40 +21,6 @@ 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; } @@ -79,21 +44,6 @@ 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); }