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

* src/tgba/succiter.hh (tgba_succ_iterator::current_condition):

Browse source 
State that this is a boolean function.
* src/tgba/succiterconcrete.hh
(tgba_succ_iterator_concrete::trans_dest_,
tgba_succ_iterator_concrete::trans_set_,
tgba_succ_iterator_concrete::trans_set_left_,
tgba_succ_iterator_concrete::neg_trans_set_): Remove.
* src/tgba/succiterconcrete.cc
(tgba_succ_iterator_concrete::tgba_succ_iterator_concrete,
tgba_succ_iterator_concrete::first): Adjust to removed members.
(tgba_succ_iterator_concrete::next): Simplify, transitions
are no labelled by boolean functions, not only conjunctions.
Suggested by Denis Poitrenaud.
This commit is contained in:
Alexandre Duret-Lutz 2003-07-03 14:02:23 +00:00
parent 3281b6e9b3
commit c09f646e3f
4 changed files with 64 additions and 86 deletions
Download patch file Download diff file Expand all files Collapse all files

26
ChangeLog
View file

@ -1,11 +1,27 @@
2003-07-03 Alexandre Duret-Lutz <aduret@src.lip6.fr>
* src/tgba/succiter.hh (tgba_succ_iterator::current_condition):
State that this is a boolean function.
* src/tgba/succiterconcrete.hh
(tgba_succ_iterator_concrete::trans_dest_,
tgba_succ_iterator_concrete::trans_set_,
tgba_succ_iterator_concrete::trans_set_left_,
tgba_succ_iterator_concrete::neg_trans_set_): Remove.
* src/tgba/succiterconcrete.cc
(tgba_succ_iterator_concrete::tgba_succ_iterator_concrete,
tgba_succ_iterator_concrete::first): Adjust to removed members.
(tgba_succ_iterator_concrete::next): Simplify, transitions
are no labelled by boolean functions, not only conjunctions.
Suggested by Denis Poitrenaud.
2003-07-02 Alexandre Duret-Lutz <aduret@src.lip6.fr>
* src/tgba/tgbabddcoredata.hh (tgba_bdd_core_data::translate): New
function.
* src/tgba/tgbabddcoredata.cc (tgba_bdd_core_data::translate):
* src/tgba/tgbabddcoredata.hh (tgba_bdd_core_data::translate): New
function.
* src/tgba/tgbabddcoredata.cc (tgba_bdd_core_data::translate):
Likewise.
* src/tgba/tgbabddtranslatefactory.cc
(tgba_bdd_translate_factory::tgba_bdd_translate_factory): Use
* src/tgba/tgbabddtranslatefactory.cc
(tgba_bdd_translate_factory::tgba_bdd_translate_factory): Use
tgba_bdd_core_data::translate.
* src/tgba/tgbabddcoredata.hh (tgba_bdd_core_data::nownext_set):

2
src/tgba/succiter.hh
View file

@ -66,6 +66,8 @@ namespace spot
/// with different conditions, leading to the same state.
virtual state* current_state() = 0;
/// \brief Get the condition on the transition leading to this successor.
///
/// This is a boolean function of atomic propositions.
virtual bdd current_condition() = 0;
/// \brief Get the accepting conditions on the transition leading
/// to this successor.

118
src/tgba/succiterconcrete.cc
View file

@ -8,9 +8,6 @@ namespace spot
: data_(d),
succ_set_(successors),
succ_set_left_(successors),
trans_dest_(bddfalse),
trans_set_(bddfalse),
trans_set_left_(bddfalse),
current_(bddfalse)
{
}
@ -23,9 +20,7 @@ namespace spot
tgba_succ_iterator_concrete::first()
{
succ_set_left_ = succ_set_;
trans_dest_ = bddfalse;
trans_set_ = bddfalse;
trans_set_left_ = bddfalse;
current_ = bddfalse;
if (!done())
next();
}
@ -49,10 +44,10 @@ namespace spot
// a & b & Next[a] & !Next[b]
// This denotes four transitions, three of which going to
// the same node. Obviously (a&b | !a&b | a&!b)
// == (a | b), so it's tempting to replace these three
// transitions by the following two:
// a & Next[a] & Next[b]
// b & Next[a] & Next[b]
// == (a | b), so it's tempting to replace these four
// transitions by
// (a + b) & Next[a] & Next[b]
// a & b & Next[a] & !Next[b]
// Is this always correct? No! It depends on the
// accepting conditions associated to each transition.
// We cannot merge transitions which have different
@ -70,86 +65,55 @@ namespace spot
do
{
// We performs a two-level iteration on transitions.
//
// succ_set_ and succ_set_left_ hold the information about the
// outer loop: the set of all transitiong going off this
// state.
//
// From this (outer) set, we compute subsets of transitions
// going to the same state and sharing the same accepting
// conditions. These are held by the trans_set_ and
// trans_set_left_ variables.
//
// We iterate of trans_set_ until all its transitions
// have been seen (trans_set_left_ is then empty). Then
// we remove trans_set_ from succ_set_left_ and compute another
// subset of succ_set_left_ to iterate over.
// FIXME: Iterating on the successors this way (calling
// bdd_satone{,set} and NANDing out the result from a
// set) requires several descent of the BDD. Maybe it would be
// faster to compute all satisfying formula in one operation.
if (trans_set_left_ == bddfalse)
succ_set_left_ &= !current_;
if (succ_set_left_ == bddfalse) // No more successors?
return;
// Pick one transition, and extract its destination.
bdd trans = bdd_satoneset(succ_set_left_, data_.next_set,
bddfalse);
bdd dest = bdd_exist(trans, data_.notnext_set);
// Gather all transitions going to this destination...
current_ = succ_set_left_ & dest;
// ... and compute their accepting sets.
bdd as = data_.accepting_conditions & current_;
// AS is false when no satisfaction of the current transition
// belongs to an accepting set: current_ can be used as-is.
if (as != bddfalse)
{
succ_set_left_ &= !(trans_set_ & trans_dest_);
if (succ_set_left_ == bddfalse) // No more successors?
return;
// Otherwise, we have accepting sets, and we should
// restrict current_ to a subset sharing the same
// accepting conditions.
// same accepting set.
// Pick one transition, and extract its destination.
bdd trans = bdd_satoneset(succ_set_left_, data_.next_set,
bddfalse);
trans_dest_ = bdd_exist(trans, data_.notnext_set);
// Gather all transitions going to this destination...
bdd st = succ_set_left_ & trans_dest_;
// ... and compute their accepting sets.
bdd as = data_.accepting_conditions & st;
if (as == bddfalse)
{
// AS is false when no transition from ST belongs to
// an accepting set. Iterate over ST directly.
trans_set_ = bdd_exist(st, data_.nownext_set);
}
else
{
// Otherwise, we have accepting sets, and we should
// only work over a set of transitions sharing the
// same accepting 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])
bdd prop = bdd_exist(cube, data_.acc_set);
// prop = (!a)&b
bdd acc = bdd_forall(bdd_restrict(as, prop), data_.var_set);
// acc = (Acc[a] | Acc[b])
trans_set_ = bdd_restrict(as, acc);
// trans_set = (a | (!a)&b)
}
trans_set_left_ = trans_set_;
neg_trans_set_ = !trans_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])
bdd prop = bdd_exist(cube, data_.acc_set);
// prop = (!a)&b
bdd acc = bdd_forall(bdd_restrict(as, prop), data_.var_set);
// acc = (Acc[a] | Acc[b])
bdd all = as & acc;
// all = (a | (!a)&b) & (Acc[a] | Acc[b])
current_ = bdd_exist(all, data_.acc_set) & dest;
// current_ = (a | (!a)&b) & (Next...)
}
// 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.
// (e.g., cube "(!a)&b" taken from "a | (!a)&b" can
// be simplified to "b").
cube = bdd_simplify(cube, cube | neg_trans_set_);
// Complete with the destination.
current_ = cube & trans_dest_;
assert(current_ != bddfalse);
// The destination state, computed here, should be compatible
// with the transition relation. Otherwise it won't have any
// successor (a dead node) and we can skip it. We need to
// compute current_state_ anyway, so this test costs us nothing.
current_state_ = bdd_replace(bdd_exist(current_, data_.notnext_set),
data_.next_to_now);
assert(dest == bdd_exist(current_, data_.notnext_set));
current_state_ = bdd_replace(dest, data_.next_to_now);
}
while ((current_state_ & data_.relation) == bddfalse);
}

4
src/tgba/succiterconcrete.hh
View file

@ -38,10 +38,6 @@ namespace spot
const tgba_bdd_core_data& data_; ///< Core data of the automaton.
bdd succ_set_; ///< The set of successors.
bdd succ_set_left_; ///< Unexplored successors (including current_).
bdd trans_dest_; ///< Destination state of currently explored subset
bdd trans_set_; ///< Set of successors with the same destination.
bdd neg_trans_set_; ///< Negation of trans_set_.
bdd trans_set_left_;///< Part of trans_set_ not yet explored.
bdd current_; ///< \brief Current successor, as a conjunction of
/// atomic proposition and Next variables.
bdd current_state_; ///< \brief Current successor, as a