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

* src/tgba/tgbabddconcrete.cc (set_init_state, succ_iter):

Browse source 
Revert the change from 2003-06-12, it needs more work (the
automaton generated on Xa&(b U !a) was bogus, with that
patch).
This commit is contained in:
Alexandre Duret-Lutz 2003-06-19 14:26:42 +00:00
parent ad0aa705cf
commit 8e51474fa2
2 changed files with 7 additions and 52 deletions
Download patch file Download diff file Expand all files Collapse all files

7
ChangeLog
View file

@ -1,7 +1,12 @@
2003-06-19 Alexandre Duret-Lutz <aduret@src.lip6.fr>
* 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.

52
src/tgba/tgbabddconcrete.cc
View file

@ -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);
}