Commit 1e6dbe40 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

* src/tgba/statebdd.hh (state_bdd::as_bdd): Add non-const variant.

* src/tgba/tgbabddtranslateproxy.cc,
src/tgba/tgbabddtranslateproxy.hh: New files.
* src/tgba/Makefile.am (libtgba_la_SOURCES): Add them.
parent 331738d6
......@@ -30,6 +30,8 @@ libtgba_la_SOURCES = \
tgbabdddict.cc \
tgbabdddict.hh \
tgbabddfactory.hh \
tgbabddprod.cc \
tgbabddprod.hh \
tgbabddtranslatefactory.cc \
tgbabddtranslatefactory.hh \
tgbabddtranslateproxy.cc \
......
......@@ -46,7 +46,7 @@ namespace spot
{
bdd_freepair(next_to_now);
}
void
tgba_bdd_core_data::declare_now_next(bdd now, bdd next)
{
......@@ -57,14 +57,14 @@ namespace spot
notvar_set &= both;
notprom_set &= both;
}
void
tgba_bdd_core_data::declare_atomic_prop(bdd var)
{
notnow_set &= var;
notprom_set &= var;
}
void
tgba_bdd_core_data::declare_promise(bdd prom)
{
......
......@@ -29,4 +29,30 @@ namespace spot
}
return os;
}
bool
tgba_bdd_dict::contains(const tgba_bdd_dict& other) const
{
fv_map::const_iterator i;
for (i = other.var_map.begin(); i != other.var_map.end(); ++i)
{
fv_map::const_iterator i2 = var_map.find(i->first);
if (i2 == var_map.end() || i->second != i2->second)
return false;
}
for (i = other.now_map.begin(); i != other.now_map.end(); ++i)
{
fv_map::const_iterator i2 = now_map.find(i->first);
if (i2 == now_map.end() || i->second != i2->second)
return false;
}
for (i = other.prom_map.begin(); i != other.prom_map.end(); ++i)
{
fv_map::const_iterator i2 = prom_map.find(i->first);
if (i2 == prom_map.end() || i->second != i2->second)
return false;
}
return true;
}
}
......@@ -26,6 +26,9 @@ namespace spot
/// \brief Dump all variables for debugging.
/// \param os The output stream.
std::ostream& dump(std::ostream& os) const;
/// Whether this dictionary contains \a other.
bool contains(const tgba_bdd_dict& other) const;
};
}
......
#include "tgbabddprod.hh"
#include "tgbabddtranslateproxy.hh"
#include "dictunion.hh"
namespace spot
{
////////////////////////////////////////////////////////////
// state_bdd_product
state_bdd_product::~state_bdd_product()
{
delete left_;
delete right_;
}
int
state_bdd_product::compare(const state* other) const
{
const state_bdd_product* o = dynamic_cast<const state_bdd_product*>(other);
assert(o);
int res = left_->compare(o->left());
if (res != 0)
return res;
return right_->compare(o->right());
}
////////////////////////////////////////////////////////////
// tgba_bdd_product_succ_iterator
tgba_bdd_product_succ_iterator::tgba_bdd_product_succ_iterator
(tgba_succ_iterator* left, tgba_succ_iterator* right)
: left_(left), right_(right)
{
}
void
tgba_bdd_product_succ_iterator::step_()
{
left_->next();
if (left_->done())
{
left_->first();
right_->next();
}
}
void
tgba_bdd_product_succ_iterator::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
tgba_bdd_product_succ_iterator::first()
{
left_->first();
right_->first();
next_non_false_();
}
void
tgba_bdd_product_succ_iterator::next()
{
step_();
next_non_false_();
}
bool
tgba_bdd_product_succ_iterator::done()
{
return right_->done();
}
state_bdd*
tgba_bdd_product_succ_iterator::current_state()
{
state_bdd* ls = dynamic_cast<state_bdd*>(left_->current_state());
state_bdd* rs = dynamic_cast<state_bdd*>(right_->current_state());
assert(ls);
assert(rs);
return new state_bdd_product(ls, rs);
}
bdd
tgba_bdd_product_succ_iterator::current_condition()
{
return current_cond_;
}
bdd tgba_bdd_product_succ_iterator::current_promise()
{
return left_->current_promise() & right_->current_promise();
}
////////////////////////////////////////////////////////////
// tgba_bdd_product
tgba_bdd_product::tgba_bdd_product(const tgba& left, const tgba& right)
: dict_(tgba_bdd_dict_union(left.get_dict(), right.get_dict()))
{
// Translate the left automaton if needed.
if (dict_.contains(left.get_dict()))
{
left_ = &left;
left_should_be_freed_ = false;
}
else
{
left_ = new tgba_bdd_translate_proxy(left, dict_);
left_should_be_freed_ = true;
}
// Translate the right automaton if needed.
if (dict_.contains(right.get_dict()))
{
right_ = &right;
right_should_be_freed_ = false;
}
else
{
right_ = new tgba_bdd_translate_proxy(right, dict_);
right_should_be_freed_ = true;
}
}
tgba_bdd_product::~tgba_bdd_product()
{
if (left_should_be_freed_)
delete left_;
if (right_should_be_freed_)
delete right_;
}
state*
tgba_bdd_product::get_init_state() const
{
state_bdd* ls = dynamic_cast<state_bdd*>(left_->get_init_state());
state_bdd* rs = dynamic_cast<state_bdd*>(right_->get_init_state());
assert(ls);
assert(rs);
return new state_bdd_product(ls, rs);
}
tgba_bdd_product_succ_iterator*
tgba_bdd_product::succ_iter(const state* state) const
{
const state_bdd_product* s = dynamic_cast<const state_bdd_product*>(state);
assert(s);
tgba_succ_iterator* li = left_->succ_iter(s->left());
tgba_succ_iterator* ri = right_->succ_iter(s->right());
return new tgba_bdd_product_succ_iterator(li, ri);
}
const tgba_bdd_dict&
tgba_bdd_product::get_dict() const
{
return dict_;
}
std::string
tgba_bdd_product::format_state(const state* state) const
{
const state_bdd_product* s = dynamic_cast<const state_bdd_product*>(state);
assert(s);
return (left_->format_state(s->left())
+ " * "
+ right_->format_state(s->right()));
}
}
#ifndef SPOT_TGBA_TGBABDDPROD_HH
# define SPOT_TGBA_TGBABDDPROD_HH
#include "tgba.hh"
#include "statebdd.hh"
namespace spot
{
/// \brief A state for spot::tgba_bdd_product.
///
/// This state is in fact a pair of state: the state from the left
/// automaton and that of the right.
class state_bdd_product : public state_bdd
{
public:
/// \brief Constructor
/// \param left The state from the left automaton.
/// \param right The state from the right automaton.
/// These state are acquired by spot::state_bdd_product, and will
/// be deleted on destruction.
state_bdd_product(state_bdd* left, state_bdd* right)
: state_bdd(left->as_bdd() & right->as_bdd()),
left_(left),
right_(right)
{
}
virtual ~state_bdd_product();
state_bdd*
left() const
{
return left_;
}
state_bdd*
right() const
{
return right_;
}
virtual int compare(const state* other) const;
private:
state_bdd* left_; ///< State from the left automaton.
state_bdd* right_; ///< State from the right automaton.
};
/// \brief Iterate over the successors of a product computed on the fly.
class tgba_bdd_product_succ_iterator: public tgba_succ_iterator
{
public:
tgba_bdd_product_succ_iterator(tgba_succ_iterator* left,
tgba_succ_iterator* right);
// iteration
void first();
void next();
bool done();
// inspection
state_bdd* current_state();
bdd current_condition();
bdd current_promise();
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_;
};
/// \brief A lazy product. (States are computed on the fly.)
class tgba_bdd_product : public tgba
{
public:
/// \brief Constructor.
/// \param left The left automata in the product.
/// \param right The right automata in the product.
/// Do not be fooled by these arguments: a product \emph is commutative.
tgba_bdd_product(const tgba& left, const tgba& right);
virtual ~tgba_bdd_product();
virtual state* get_init_state() const;
virtual tgba_bdd_product_succ_iterator*
succ_iter(const state* state) const;
virtual const tgba_bdd_dict& get_dict() const;
virtual std::string format_state(const state* state) const;
private:
const tgba* left_;
bool left_should_be_freed_;
const tgba* right_;
bool right_should_be_freed_;
tgba_bdd_dict dict_;
};
}
#endif // SPOT_TGBA_TGBABDDPROD_HH
......@@ -6,7 +6,7 @@
namespace spot
{
/// \brief Proxy for a spot::tgba_succ_iterator_concrete that renumber
/// \brief Proxy for a spot::tgba_succ_iterator_concrete that renumber
/// BDD variables on the fly.
class tgba_bdd_translate_proxy_succ_iterator: public tgba_succ_iterator
{
......@@ -34,31 +34,30 @@ namespace spot
class tgba_bdd_translate_proxy: public tgba
{
public:
/// \brief Construcor.
/// \brief Constructor.
/// \param from The spot::tgba to masquerade.
/// \param to The new dictionary to use.
tgba_bdd_translate_proxy(const tgba& from,
tgba_bdd_translate_proxy(const tgba& from,
const tgba_bdd_dict& to);
virtual ~tgba_bdd_translate_proxy();
virtual state_bdd* get_init_state() const;
virtual tgba_bdd_translate_proxy_succ_iterator*
virtual tgba_bdd_translate_proxy_succ_iterator*
succ_iter(const state* state) const;
virtual const tgba_bdd_dict& get_dict() const;
virtual std::string
tgba_bdd_translate_proxy::format_state(const state* state) const;
virtual std::string format_state(const state* state) const;
private:
const tgba& from_; ///< The spot::tgba to masquerade.
tgba_bdd_dict to_; ///< The new dictionar to use.
bddPair* rewrite_to_; ///< The rewriting pair for from->to.
bddPair* rewrite_from_; ///< The rewriting pair for to->from.
};
}
#endif // SPOT_TGBA_TGBABDDTRANSLATEPROXY_HH
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