Commit 8a44ed08 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

* tgba/tgbaproduct.cc, tgba/tgbaproduct.hh:

(state_bdd_product, tgba_product_succ_iterator): Rename as ...
(state_product, tgba_succ_iterator_product): ... these.
parent e238135b
2003-08-20 Alexandre Duret-Lutz <aduret@src.lip6.fr> 2003-08-20 Alexandre Duret-Lutz <aduret@src.lip6.fr>
* tgba/tgbaproduct.cc, tgba/tgbaproduct.hh:
(state_bdd_product, tgba_product_succ_iterator): Rename as ...
(state_product, tgba_succ_iterator_product): ... these.
* iface/gspn/dcswavefm.test: New file. * iface/gspn/dcswavefm.test: New file.
* iface/gspn/Makefile.am (check_PROGRAMS): Add fmgspn-rg and * iface/gspn/Makefile.am (check_PROGRAMS): Add fmgspn-rg and
fmgspn-srg. fmgspn-srg.
......
...@@ -6,25 +6,25 @@ namespace spot ...@@ -6,25 +6,25 @@ namespace spot
{ {
//////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////
// state_bdd_product // state_product
state_bdd_product::state_bdd_product(const state_bdd_product& o) state_product::state_product(const state_product& o)
: state(), : state(),
left_(o.left()->clone()), left_(o.left()->clone()),
right_(o.right()->clone()) right_(o.right()->clone())
{ {
} }
state_bdd_product::~state_bdd_product() state_product::~state_product()
{ {
delete left_; delete left_;
delete right_; delete right_;
} }
int int
state_bdd_product::compare(const state* other) const state_product::compare(const state* other) const
{ {
const state_bdd_product* o = dynamic_cast<const state_bdd_product*>(other); const state_product* o = dynamic_cast<const state_product*>(other);
assert(o); assert(o);
int res = left_->compare(o->left()); int res = left_->compare(o->left());
if (res != 0) if (res != 0)
...@@ -32,16 +32,16 @@ namespace spot ...@@ -32,16 +32,16 @@ namespace spot
return right_->compare(o->right()); return right_->compare(o->right());
} }
state_bdd_product* state_product*
state_bdd_product::clone() const state_product::clone() const
{ {
return new state_bdd_product(*this); return new state_product(*this);
} }
//////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////
// tgba_product_succ_iterator // tgba_succ_iterator_product
tgba_product_succ_iterator::tgba_product_succ_iterator tgba_succ_iterator_product::tgba_succ_iterator_product
(tgba_succ_iterator* left, tgba_succ_iterator* right, (tgba_succ_iterator* left, tgba_succ_iterator* right,
bdd left_neg, bdd right_neg) bdd left_neg, bdd right_neg)
: left_(left), right_(right), : left_(left), right_(right),
...@@ -50,7 +50,7 @@ namespace spot ...@@ -50,7 +50,7 @@ namespace spot
{ {
} }
tgba_product_succ_iterator::~tgba_product_succ_iterator() tgba_succ_iterator_product::~tgba_succ_iterator_product()
{ {
delete left_; delete left_;
if (right_) if (right_)
...@@ -58,7 +58,7 @@ namespace spot ...@@ -58,7 +58,7 @@ namespace spot
} }
void void
tgba_product_succ_iterator::step_() tgba_succ_iterator_product::step_()
{ {
left_->next(); left_->next();
if (left_->done()) if (left_->done())
...@@ -69,7 +69,7 @@ namespace spot ...@@ -69,7 +69,7 @@ namespace spot
} }
void void
tgba_product_succ_iterator::next_non_false_() tgba_succ_iterator_product::next_non_false_()
{ {
while (!done()) while (!done())
{ {
...@@ -87,7 +87,7 @@ namespace spot ...@@ -87,7 +87,7 @@ namespace spot
} }
void void
tgba_product_succ_iterator::first() tgba_succ_iterator_product::first()
{ {
if (!right_) if (!right_)
return; return;
...@@ -108,33 +108,33 @@ namespace spot ...@@ -108,33 +108,33 @@ namespace spot
} }
void void
tgba_product_succ_iterator::next() tgba_succ_iterator_product::next()
{ {
step_(); step_();
next_non_false_(); next_non_false_();
} }
bool bool
tgba_product_succ_iterator::done() const tgba_succ_iterator_product::done() const
{ {
return !right_ || right_->done(); return !right_ || right_->done();
} }
state_bdd_product* state_product*
tgba_product_succ_iterator::current_state() const tgba_succ_iterator_product::current_state() const
{ {
return new state_bdd_product(left_->current_state(), return new state_product(left_->current_state(),
right_->current_state()); right_->current_state());
} }
bdd bdd
tgba_product_succ_iterator::current_condition() const tgba_succ_iterator_product::current_condition() const
{ {
return current_cond_; return current_cond_;
} }
bdd tgba_product_succ_iterator::current_accepting_conditions() const bdd tgba_succ_iterator_product::current_accepting_conditions() const
{ {
return ((left_->current_accepting_conditions() & right_neg_) return ((left_->current_accepting_conditions() & right_neg_)
| (right_->current_accepting_conditions() & left_neg_)); | (right_->current_accepting_conditions() & left_neg_));
...@@ -166,17 +166,17 @@ namespace spot ...@@ -166,17 +166,17 @@ namespace spot
state* state*
tgba_product::get_init_state() const tgba_product::get_init_state() const
{ {
return new state_bdd_product(left_->get_init_state(), return new state_product(left_->get_init_state(),
right_->get_init_state()); right_->get_init_state());
} }
tgba_product_succ_iterator* tgba_succ_iterator_product*
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
{ {
const state_bdd_product* s = const state_product* s =
dynamic_cast<const state_bdd_product*>(local_state); dynamic_cast<const state_product*>(local_state);
assert(s); assert(s);
// If global_automaton is not specified, THIS is the root of a // If global_automaton is not specified, THIS is the root of a
...@@ -191,7 +191,7 @@ namespace spot ...@@ -191,7 +191,7 @@ 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_product_succ_iterator(li, ri, return new tgba_succ_iterator_product(li, ri,
left_->neg_accepting_conditions(), left_->neg_accepting_conditions(),
right_->neg_accepting_conditions()); right_->neg_accepting_conditions());
} }
...@@ -199,8 +199,7 @@ namespace spot ...@@ -199,8 +199,7 @@ namespace spot
bdd bdd
tgba_product::compute_support_conditions(const state* in) const tgba_product::compute_support_conditions(const state* in) const
{ {
const state_bdd_product* s = const state_product* s = dynamic_cast<const state_product*>(in);
dynamic_cast<const state_bdd_product*>(in);
assert(s); assert(s);
bdd lsc = left_->support_conditions(s->left()); bdd lsc = left_->support_conditions(s->left());
bdd rsc = right_->support_conditions(s->right()); bdd rsc = right_->support_conditions(s->right());
...@@ -210,8 +209,7 @@ namespace spot ...@@ -210,8 +209,7 @@ namespace spot
bdd bdd
tgba_product::compute_support_variables(const state* in) const tgba_product::compute_support_variables(const state* in) const
{ {
const state_bdd_product* s = const state_product* s = dynamic_cast<const state_product*>(in);
dynamic_cast<const state_bdd_product*>(in);
assert(s); assert(s);
bdd lsc = left_->support_variables(s->left()); bdd lsc = left_->support_variables(s->left());
bdd rsc = right_->support_variables(s->right()); bdd rsc = right_->support_variables(s->right());
...@@ -227,7 +225,7 @@ namespace spot ...@@ -227,7 +225,7 @@ namespace spot
std::string std::string
tgba_product::format_state(const state* state) const tgba_product::format_state(const state* state) const
{ {
const state_bdd_product* s = dynamic_cast<const state_bdd_product*>(state); const state_product* s = dynamic_cast<const state_product*>(state);
assert(s); assert(s);
return (left_->format_state(s->left()) return (left_->format_state(s->left())
+ " * " + " * "
...@@ -237,7 +235,7 @@ namespace spot ...@@ -237,7 +235,7 @@ namespace spot
state* state*
tgba_product::project_state(const state* s, const tgba* t) const tgba_product::project_state(const state* s, const tgba* t) const
{ {
const state_bdd_product* s2 = dynamic_cast<const state_bdd_product*>(s); const state_product* s2 = dynamic_cast<const state_product*>(s);
assert(s2); assert(s2);
if (t == this) if (t == this)
return s2->clone(); return s2->clone();
......
...@@ -11,24 +11,24 @@ namespace spot ...@@ -11,24 +11,24 @@ namespace spot
/// ///
/// This state is in fact a pair of state: the state from the left /// This state is in fact a pair of state: the state from the left
/// automaton and that of the right. /// automaton and that of the right.
class state_bdd_product : public state class state_product : public state
{ {
public: public:
/// \brief Constructor /// \brief Constructor
/// \param left The state from the left automaton. /// \param left The state from the left automaton.
/// \param right The state from the right automaton. /// \param right The state from the right automaton.
/// These state are acquired by spot::state_bdd_product, and will /// These states are acquired by spot::state_product, and will
/// be deleted on destruction. /// be deleted on destruction.
state_bdd_product(state* left, state* right) state_product(state* left, state* right)
: left_(left), : left_(left),
right_(right) right_(right)
{ {
} }
/// Copy constructor /// Copy constructor
state_bdd_product(const state_bdd_product& o); state_product(const state_product& o);
virtual ~state_bdd_product(); virtual ~state_product();
state* state*
left() const left() const
...@@ -43,7 +43,7 @@ namespace spot ...@@ -43,7 +43,7 @@ namespace spot
} }
virtual int compare(const state* other) const; virtual int compare(const state* other) const;
virtual state_bdd_product* clone() const; virtual state_product* clone() const;
private: private:
state* left_; ///< State from the left automaton. state* left_; ///< State from the left automaton.
...@@ -52,14 +52,14 @@ namespace spot ...@@ -52,14 +52,14 @@ namespace spot
/// \brief Iterate over the successors of a product computed on the fly. /// \brief Iterate over the successors of a product computed on the fly.
class tgba_product_succ_iterator: public tgba_succ_iterator class tgba_succ_iterator_product: public tgba_succ_iterator
{ {
public: public:
tgba_product_succ_iterator(tgba_succ_iterator* left, tgba_succ_iterator_product(tgba_succ_iterator* left,
tgba_succ_iterator* right, tgba_succ_iterator* right,
bdd left_neg, bdd right_neg); bdd left_neg, bdd right_neg);
virtual ~tgba_product_succ_iterator(); virtual ~tgba_succ_iterator_product();
// iteration // iteration
void first(); void first();
...@@ -67,7 +67,7 @@ namespace spot ...@@ -67,7 +67,7 @@ namespace spot
bool done() const; bool done() const;
// inspection // inspection
state_bdd_product* current_state() const; state_product* current_state() const;
bdd current_condition() const; bdd current_condition() const;
bdd current_accepting_conditions() const; bdd current_accepting_conditions() const;
...@@ -100,7 +100,7 @@ namespace spot ...@@ -100,7 +100,7 @@ namespace spot
virtual state* get_init_state() const; virtual state* get_init_state() const;
virtual tgba_product_succ_iterator* virtual tgba_succ_iterator_product*
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;
......
Markdown is supported
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