Commit 94ac863c authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

Speedup tgba_product when one of the argument is a Kripke structure.

The gain is not very impressive.  The runtime of the first example
in iface/dve2/README (also in dve2check.test) is 15% faster.

* src/tgba/tgbaproduct.hh (tgba_succ_iterator_product): Move ...
* src/tgba/tgbaproduct.cc (tgba_succ_iterator_product,
tgba_succ_iterator_product_common): ... in these two classes.
(tgba_succ_iterator_product_kripke): New class to speedup
successor computation on Kripke structures.  We can assume that
all the transitions leaving the same state have the same label.
(tgba_product::tgba_product, tgba_product::succ_iter): Use
tgba_succ_iterator_product_kripke when appropriate.
(tgba_product_init::tgba_product_init): Adjust for the case
where tgba_product did reverse its operands.
parent 33732493
2011-03-30 Alexandre Duret-Lutz <adl@lrde.epita.fr>
Speedup tgba_product when one of the argument is a Kripke structure.
The gain is not very impressive. The runtime of the first example
in iface/dve2/README (also in dve2check.test) is 15% faster.
* src/tgba/tgbaproduct.hh (tgba_succ_iterator_product): Move ...
* src/tgba/tgbaproduct.cc (tgba_succ_iterator_product,
tgba_succ_iterator_product_common): ... in these two classes.
(tgba_succ_iterator_product_kripke): New class to speedup
successor computation on Kripke structures. We can assume that
all the transitions leaving the same state have the same label.
(tgba_product::tgba_product, tgba_product::succ_iter): Use
tgba_succ_iterator_product_kripke when appropriate.
(tgba_product_init::tgba_product_init): Adjust for the case
where tgba_product did reverse its operands.
2011-03-30 Alexandre Duret-Lutz <adl@lrde.epita.fr> 2011-03-30 Alexandre Duret-Lutz <adl@lrde.epita.fr>
* iface/dve2/dve2check.cc: Remove stray debug output. * iface/dve2/dve2check.cc: Remove stray debug output.
......
...@@ -25,6 +25,7 @@ ...@@ -25,6 +25,7 @@
#include <string> #include <string>
#include <cassert> #include <cassert>
#include "misc/hashfunc.hh" #include "misc/hashfunc.hh"
#include "kripke/kripke.hh"
namespace spot namespace spot
{ {
...@@ -72,105 +73,196 @@ namespace spot ...@@ -72,105 +73,196 @@ namespace spot
//////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////
// tgba_succ_iterator_product // tgba_succ_iterator_product
tgba_succ_iterator_product::tgba_succ_iterator_product namespace
(tgba_succ_iterator* left, tgba_succ_iterator* right,
bdd left_neg, bdd right_neg, bddPair* right_common_acc)
: left_(left), right_(right),
left_neg_(left_neg),
right_neg_(right_neg),
right_common_acc_(right_common_acc)
{ {
}
tgba_succ_iterator_product::~tgba_succ_iterator_product() class tgba_succ_iterator_product_common: public tgba_succ_iterator
{ {
delete left_; public:
delete right_; tgba_succ_iterator_product_common(tgba_succ_iterator* left,
} tgba_succ_iterator* right)
: left_(left), right_(right)
{
}
void virtual ~tgba_succ_iterator_product_common()
tgba_succ_iterator_product::step_()
{
left_->next();
if (left_->done())
{ {
left_->first(); delete left_;
right_->next(); delete right_;
} }
}
void virtual void next_non_false_() = 0;
tgba_succ_iterator_product::next_non_false_()
{ void first()
while (!done())
{ {
bdd l = left_->current_condition(); if (!right_)
bdd r = right_->current_condition(); return;
bdd current_cond = l & r;
if (current_cond != bddfalse) left_->first();
right_->first();
// If one of the two successor sets is empty initially, we
// reset right_, so that done() can detect this situation
// easily. (We choose to reset right_ because this variable
// is already used by done().)
if (left_->done() || right_->done())
{ {
current_cond_ = current_cond; delete right_;
right_ = 0;
return; return;
} }
next_non_false_();
}
bool done() const
{
return !right_ || right_->done();
}
state_product* current_state() const
{
return new state_product(left_->current_state(),
right_->current_state());
}
protected:
tgba_succ_iterator* left_;
tgba_succ_iterator* right_;
friend class spot::tgba_product;
};
/// \brief Iterate over the successors of a product computed on the fly.
class tgba_succ_iterator_product: public tgba_succ_iterator_product_common
{
public:
tgba_succ_iterator_product(tgba_succ_iterator* left,
tgba_succ_iterator* right,
bdd left_neg, bdd right_neg,
bddPair* right_common_acc)
: tgba_succ_iterator_product_common(left, right),
left_neg_(left_neg),
right_neg_(right_neg),
right_common_acc_(right_common_acc)
{
}
virtual ~tgba_succ_iterator_product()
{
}
void step_()
{
left_->next();
if (left_->done())
{
left_->first();
right_->next();
}
}
void next_non_false_()
{
while (!done())
{
bdd l = left_->current_condition();
bdd r = right_->current_condition();
bdd current_cond = l & r;
if (current_cond != bddfalse)
{
current_cond_ = current_cond;
return;
}
step_();
}
}
void next()
{
step_(); step_();
next_non_false_();
} }
}
void bdd current_condition() const
tgba_succ_iterator_product::first()
{
if (!right_)
return;
left_->first();
right_->first();
// If one of the two successor sets is empty initially, we reset
// right_, so that done() can detect this situation easily. (We
// choose to reset right_ because this variable is already used by
// done().)
if (left_->done() || right_->done())
{ {
delete right_; return current_cond_;
right_ = 0;
return;
} }
next_non_false_();
}
void bdd current_acceptance_conditions() const
tgba_succ_iterator_product::next() {
{ return ((left_->current_acceptance_conditions() & right_neg_)
step_(); | (bdd_replace(right_->current_acceptance_conditions(),
next_non_false_(); right_common_acc_) & left_neg_));
} }
bool protected:
tgba_succ_iterator_product::done() const bdd current_cond_;
{ bdd left_neg_;
return !right_ || right_->done(); bdd right_neg_;
} bddPair* right_common_acc_;
};
/// Iterate over the successors of a product computed on the fly.
/// This one assumes that LEFT is an iterator over a Kripke structure
class tgba_succ_iterator_product_kripke:
public tgba_succ_iterator_product_common
{
public:
tgba_succ_iterator_product_kripke(tgba_succ_iterator* left,
tgba_succ_iterator* right)
: tgba_succ_iterator_product_common(left, right)
{
}
virtual ~tgba_succ_iterator_product_kripke()
{
}
state_product* void next_non_false_()
tgba_succ_iterator_product::current_state() const {
{ // All the transitions of left_ iterator have the
return new state_product(left_->current_state(), // same label, because it is a Kripke structure.
right_->current_state()); bdd l = left_->current_condition();
} while (!right_->done())
{
bdd r = right_->current_condition();
bdd current_cond = l & r;
if (current_cond != bddfalse)
{
current_cond_ = current_cond;
return;
}
right_->next();
}
}
bdd void next()
tgba_succ_iterator_product::current_condition() const {
{ left_->next();
return current_cond_; if (left_->done())
} {
left_->first();
right_->next();
next_non_false_();
}
}
bdd tgba_succ_iterator_product::current_acceptance_conditions() const bdd current_condition() const
{ {
return ((left_->current_acceptance_conditions() & right_neg_) return current_cond_;
| (bdd_replace(right_->current_acceptance_conditions(), }
right_common_acc_) & left_neg_));
} bdd current_acceptance_conditions() const
{
return right_->current_acceptance_conditions();
}
protected:
bdd current_cond_;
};
} // anonymous
//////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////
// tgba_product // tgba_product
...@@ -178,7 +270,34 @@ namespace spot ...@@ -178,7 +270,34 @@ namespace spot
tgba_product::tgba_product(const tgba* left, const tgba* right) tgba_product::tgba_product(const tgba* left, const tgba* right)
: dict_(left->get_dict()), left_(left), right_(right) : dict_(left->get_dict()), left_(left), right_(right)
{ {
assert(dict_ == right->get_dict()); assert(dict_ == right_->get_dict());
// If one of the side is a Kripke structure, it is easier to deal
// with (we don't have to fix the acceptance conditions, and
// computing the successors can be improved a bit).
if (dynamic_cast<const kripke*>(left_))
{
left_kripke_ = true;
}
else if (dynamic_cast<const kripke*>(right_))
{
std::swap(left_, right_);
left_kripke_ = true;
}
else
{
left_kripke_ = false;
}
dict_->register_all_variables_of(&left_, this);
dict_->register_all_variables_of(&right_, this);
if (left_kripke_)
{
all_acceptance_conditions_ = right_->all_acceptance_conditions();
neg_acceptance_conditions_ = right_->neg_acceptance_conditions();
return;
}
bdd lna = left_->neg_acceptance_conditions(); bdd lna = left_->neg_acceptance_conditions();
bdd rna = right_->neg_acceptance_conditions(); bdd rna = right_->neg_acceptance_conditions();
...@@ -212,14 +331,12 @@ namespace spot ...@@ -212,14 +331,12 @@ namespace spot
all_acceptance_conditions_ = ((lac & right_acc_complement_) all_acceptance_conditions_ = ((lac & right_acc_complement_)
| (rac & left_acc_complement_)); | (rac & left_acc_complement_));
neg_acceptance_conditions_ = lna & rna; neg_acceptance_conditions_ = lna & rna;
dict_->register_all_variables_of(&left_, this);
dict_->register_all_variables_of(&right_, this);
} }
tgba_product::~tgba_product() tgba_product::~tgba_product()
{ {
bdd_freepair(right_common_acc_); if (!left_kripke_)
bdd_freepair(right_common_acc_);
dict_->unregister_all_my_variables(this); dict_->unregister_all_my_variables(this);
} }
...@@ -230,7 +347,7 @@ namespace spot ...@@ -230,7 +347,7 @@ namespace spot
right_->get_init_state()); right_->get_init_state());
} }
tgba_succ_iterator_product* tgba_succ_iterator*
tgba_product::succ_iter(const state* local_state, tgba_product::succ_iter(const state* local_state,
const state* global_state, const state* global_state,
const tgba* global_automaton) const const tgba* global_automaton) const
...@@ -251,10 +368,14 @@ namespace spot ...@@ -251,10 +368,14 @@ namespace spot
global_state, global_automaton); global_state, global_automaton);
tgba_succ_iterator* ri = right_->succ_iter(s->right(), tgba_succ_iterator* ri = right_->succ_iter(s->right(),
global_state, global_automaton); global_state, global_automaton);
return new tgba_succ_iterator_product(li, ri,
left_acc_complement_, if (left_kripke_)
right_acc_complement_, return new tgba_succ_iterator_product_kripke(li, ri);
right_common_acc_); else
return new tgba_succ_iterator_product(li, ri,
left_acc_complement_,
right_acc_complement_,
right_common_acc_);
} }
bdd bdd
...@@ -342,6 +463,8 @@ namespace spot ...@@ -342,6 +463,8 @@ namespace spot
: tgba_product(left, right), : tgba_product(left, right),
left_init_(left_init), right_init_(right_init) left_init_(left_init), right_init_(right_init)
{ {
if (left_ != left)
std::swap(left_init_, right_init_);
} }
state* state*
......
...@@ -75,44 +75,6 @@ namespace spot ...@@ -75,44 +75,6 @@ namespace spot
}; };
/// \brief Iterate over the successors of a product computed on the fly.
class tgba_succ_iterator_product: public tgba_succ_iterator
{
public:
tgba_succ_iterator_product(tgba_succ_iterator* left,
tgba_succ_iterator* right,
bdd left_neg, bdd right_neg,
bddPair* right_common_acc);
virtual ~tgba_succ_iterator_product();
// iteration
void first();
void next();
bool done() const;
// inspection
state_product* current_state() const;
bdd current_condition() const;
bdd current_acceptance_conditions() const;
private:
//@{
/// Internal routines to advance to the next successor.
void step_();
void next_non_false_();
//@}
protected:
tgba_succ_iterator* left_;
tgba_succ_iterator* right_;
bdd current_cond_;
bdd left_neg_;
bdd right_neg_;
bddPair* right_common_acc_;
friend class tgba_product;
};
/// \brief A lazy product. (States are computed on the fly.) /// \brief A lazy product. (States are computed on the fly.)
class tgba_product: public tgba class tgba_product: public tgba
{ {
...@@ -127,7 +89,7 @@ namespace spot ...@@ -127,7 +89,7 @@ namespace spot
virtual state* get_init_state() const; virtual state* get_init_state() const;
virtual tgba_succ_iterator_product* virtual tgba_succ_iterator*
succ_iter(const state* local_state, succ_iter(const state* local_state,
const state* global_state = 0, const state* global_state = 0,
const tgba* global_automaton = 0) const; const tgba* global_automaton = 0) const;
...@@ -148,15 +110,17 @@ namespace spot ...@@ -148,15 +110,17 @@ namespace spot
virtual bdd compute_support_conditions(const state* state) const; virtual bdd compute_support_conditions(const state* state) const;
virtual bdd compute_support_variables(const state* state) const; virtual bdd compute_support_variables(const state* state) const;
private: protected:
bdd_dict* dict_; bdd_dict* dict_;
const tgba* left_; const tgba* left_;
const tgba* right_; const tgba* right_;
bool left_kripke_;
bdd left_acc_complement_; bdd left_acc_complement_;
bdd right_acc_complement_; bdd right_acc_complement_;
bdd all_acceptance_conditions_; bdd all_acceptance_conditions_;
bdd neg_acceptance_conditions_; bdd neg_acceptance_conditions_;
bddPair* right_common_acc_; bddPair* right_common_acc_;
private:
// Disallow copy. // Disallow copy.
tgba_product(const tgba_product&); tgba_product(const tgba_product&);
tgba_product& operator=(const tgba_product&); tgba_product& operator=(const tgba_product&);
...@@ -169,7 +133,7 @@ namespace spot ...@@ -169,7 +133,7 @@ namespace spot
tgba_product_init(const tgba* left, const tgba* right, tgba_product_init(const tgba* left, const tgba* right,
const state* left_init, const state* right_init); const state* left_init, const state* right_init);
virtual state* get_init_state() const; virtual state* get_init_state() const;
private: protected:
const state* left_init_; const state* left_init_;
const state* right_init_; const state* right_init_;
}; };
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment