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

* iface/gspn/eesrg.cc (tgba_succ_iterator_gspn_eesrg::first_): New

Browse source 
attribute.
(tgba_succ_iterator_gspn_eesrg::step): Use first_.  Loop until
succ returns some successors.
Report from Soheib Baarir.
This commit is contained in:
Alexandre Duret-Lutz 2003-11-07 10:19:18 +00:00
parent f31caafb50
commit 10b2511dda
2 changed files with 68 additions and 50 deletions
Download patch file Download diff file Expand all files Collapse all files

8
ChangeLog
View file

@ -1,3 +1,11 @@
2003-11-07 Alexandre Duret-Lutz <adl@src.lip6.fr>
* iface/gspn/eesrg.cc (tgba_succ_iterator_gspn_eesrg::first_): New
attribute.
(tgba_succ_iterator_gspn_eesrg::step): Use first_. Loop until
succ returns some successors.
Report from Soheib Baarir.
2003-11-06 Alexandre Duret-Lutz <adl@src.lip6.fr> 2003-11-06 Alexandre Duret-Lutz <adl@src.lip6.fr>
* iface/gspn/eesrg.cc (tgba_succ_iterator_gspn_eesrg::step): Fix * iface/gspn/eesrg.cc (tgba_succ_iterator_gspn_eesrg::step): Fix

30
iface/gspn/eesrg.cc
View file

@ -162,17 +162,15 @@ namespace spot
successors_(0), successors_(0),
size_(0), size_(0),
current_(0), current_(0),
data_(data) data_(data),
not_first_(false)
{ {
} }
virtual virtual
~tgba_succ_iterator_gspn_eesrg() ~tgba_succ_iterator_gspn_eesrg()
{ {
// If the iterator is done, successors_ has already if (successors_)
// been freed from step(). (We can't use 0 do indicate
// this, because successor_==0 means something else to step().)
if (successors_ && !done())
succ_free(successors_); succ_free(successors_);
if (operand_) if (operand_)
delete operand_; delete operand_;
@ -184,17 +182,26 @@ namespace spot
if (++current_ < size_) if (++current_ < size_)
return; return;
do
{
if (successors_) if (successors_)
{
succ_free(successors_); succ_free(successors_);
successors_ = 0;
}
if (all_conds_ == bddfalse) if (all_conds_ == bddfalse)
{ {
// SUCCESSORS_ is 0 when step() is called from first(). if (not_first_)
if (successors_)
{ {
assert(!operand_->done()); assert(!operand_->done());
operand_->next(); operand_->next();
} }
else
{
// operand_->first() has already been called from first().
not_first_ = true;
}
if (operand_->done()) if (operand_->done())
return; return;
all_conds_ = operand_->current_condition(); all_conds_ = operand_->current_condition();
@ -225,9 +232,9 @@ namespace spot
res = 1; res = 1;
} }
// It's OK if VAR is unknown from GreatSPN (it might have // It's OK if VAR is unknown from GreatSPN (it might
// been used to synchornize other automaton or something), // have been used to synchornize another automaton or
// just skip it. // something), just skip it.
tgba_gspn_eesrg_private_::prop_map::iterator i = tgba_gspn_eesrg_private_::prop_map::iterator i =
data_->prop_dict.find(var); data_->prop_dict.find(var);
if (i != data_->prop_dict.end()) if (i != data_->prop_dict.end())
@ -239,6 +246,8 @@ namespace spot
succ(state_, props, &successors_, &size_); succ(state_, props, &successors_, &size_);
current_ = 0; current_ = 0;
} }
while (size_ == 0); // Repeat until we have a successor.
}
virtual void virtual void
first() first()
@ -309,6 +318,7 @@ namespace spot
size_t size_; /// size of successors_ size_t size_; /// size of successors_
size_t current_; /// current position in successors_ size_t current_; /// current position in successors_
tgba_gspn_eesrg_private_* data_; tgba_gspn_eesrg_private_* data_;
bool not_first_; /// Whether this is not the first step.
}; // tgba_succ_iterator_gspn_eesrg }; // tgba_succ_iterator_gspn_eesrg