* src/tgba/tgbabddprod.cc, src/tgba/tgbabddprod.hh: Rename as ...
* src/tgba/tgbaproduct.cc, src/tgba/tgbaproduct.hh: ... these. (tgba_bdd_product, tgba_bdd_product_succ_iterator): Rename as ... (tgba_product, tgba_product_succ_iterator): ... these, and adjust all uses. * src/tgba/tgbabddtranslateproxy.cc, src/tgba/tgbabddtranslateproxy.hh: Rename as ... * src/tgba/tgbatranslateproxy.cc, src/tgba/tgbatranslateproxy.hh: ... these. (tgba_bdd_translate_proxy, tgba_bdd_translate_proxy_succ_iterator): Rename as ... (tgba_translate_proxy, tgba_translate_proxy_succ_iterator): ... these, and adjust all uses.
This commit is contained in:
Alexandre Duret-Lutz
parent
b1d2b351fb
commit
4db70160c9
9 changed files with 96 additions and 83 deletions
16
ChangeLog
16
ChangeLog
|
|
@ -1,7 +1,21 @@
|
|||
2003-06-16 Alexandre Duret-Lutz <aduret@src.lip6.fr>
|
||||
|
||||
* src/tgba/tgbabddprod.cc, src/tgba/tgbabddprod.hh: Rename as ...
|
||||
* src/tgba/tgbaproduct.cc, src/tgba/tgbaproduct.hh: ... these.
|
||||
(tgba_bdd_product, tgba_bdd_product_succ_iterator): Rename as ...
|
||||
(tgba_product, tgba_product_succ_iterator): ... these, and adjust
|
||||
all uses.
|
||||
* src/tgba/tgbabddtranslateproxy.cc,
|
||||
src/tgba/tgbabddtranslateproxy.hh: Rename as ...
|
||||
* src/tgba/tgbatranslateproxy.cc,
|
||||
src/tgba/tgbatranslateproxy.hh: ... these.
|
||||
(tgba_bdd_translate_proxy, tgba_bdd_translate_proxy_succ_iterator):
|
||||
Rename as ...
|
||||
(tgba_translate_proxy, tgba_translate_proxy_succ_iterator): ... these,
|
||||
and adjust all uses.
|
||||
|
||||
Make sure we can multiply two tgba_explicit.
|
||||
|
||||
|
||||
* tgba/state.hh (state::translate, state::clone, state::as_bdd):
|
||||
New virtual methods.
|
||||
* tgba/stataebdd.cc (state::translate, state::clone): New methods.
|
||||
|
|
|
|||
|
|
@ -30,11 +30,11 @@ libtgba_la_SOURCES = \
|
|||
tgbabdddict.cc \
|
||||
tgbabdddict.hh \
|
||||
tgbabddfactory.hh \
|
||||
tgbabddprod.cc \
|
||||
tgbabddprod.hh \
|
||||
tgbabddtranslatefactory.cc \
|
||||
tgbabddtranslatefactory.hh \
|
||||
tgbabddtranslateproxy.cc \
|
||||
tgbabddtranslateproxy.hh \
|
||||
tgbaexplicit.cc \
|
||||
tgbaexplicit.hh
|
||||
tgbaexplicit.hh \
|
||||
tgbaproduct.cc \
|
||||
tgbaproduct.hh \
|
||||
tgbatranslateproxy.cc \
|
||||
tgbatranslateproxy.hh
|
||||
|
|
|
|||
|
|
@ -26,7 +26,7 @@ namespace spot
|
|||
///
|
||||
/// If this state uses any BDD variable. This function
|
||||
/// should rewrite the variables according to \a rewrite.
|
||||
/// This used by spot::tgbabddtranslateproxy.
|
||||
/// This used by spot::tgba_translate_proxy.
|
||||
virtual void translate(bddPair* rewrite)
|
||||
{
|
||||
// This does nothing by default and is
|
||||
|
|
|
|||
|
|
@ -1,5 +1,5 @@
|
|||
#include "tgbabddprod.hh"
|
||||
#include "tgbabddtranslateproxy.hh"
|
||||
#include "tgbaproduct.hh"
|
||||
#include "tgbatranslateproxy.hh"
|
||||
#include "dictunion.hh"
|
||||
#include <cassert>
|
||||
|
||||
|
|
@ -33,15 +33,15 @@ namespace spot
|
|||
}
|
||||
|
||||
////////////////////////////////////////////////////////////
|
||||
// tgba_bdd_product_succ_iterator
|
||||
// tgba_product_succ_iterator
|
||||
|
||||
tgba_bdd_product_succ_iterator::tgba_bdd_product_succ_iterator
|
||||
tgba_product_succ_iterator::tgba_product_succ_iterator
|
||||
(tgba_succ_iterator* left, tgba_succ_iterator* right)
|
||||
: left_(left), right_(right)
|
||||
{
|
||||
}
|
||||
|
||||
tgba_bdd_product_succ_iterator::~tgba_bdd_product_succ_iterator()
|
||||
tgba_product_succ_iterator::~tgba_product_succ_iterator()
|
||||
{
|
||||
delete left_;
|
||||
if (right_)
|
||||
|
|
@ -49,7 +49,7 @@ namespace spot
|
|||
}
|
||||
|
||||
void
|
||||
tgba_bdd_product_succ_iterator::step_()
|
||||
tgba_product_succ_iterator::step_()
|
||||
{
|
||||
left_->next();
|
||||
if (left_->done())
|
||||
|
|
@ -60,7 +60,7 @@ namespace spot
|
|||
}
|
||||
|
||||
void
|
||||
tgba_bdd_product_succ_iterator::next_non_false_()
|
||||
tgba_product_succ_iterator::next_non_false_()
|
||||
{
|
||||
while (!done())
|
||||
{
|
||||
|
|
@ -78,7 +78,7 @@ namespace spot
|
|||
}
|
||||
|
||||
void
|
||||
tgba_bdd_product_succ_iterator::first()
|
||||
tgba_product_succ_iterator::first()
|
||||
{
|
||||
if (!right_)
|
||||
return;
|
||||
|
|
@ -98,41 +98,41 @@ namespace spot
|
|||
}
|
||||
|
||||
void
|
||||
tgba_bdd_product_succ_iterator::next()
|
||||
tgba_product_succ_iterator::next()
|
||||
{
|
||||
step_();
|
||||
next_non_false_();
|
||||
}
|
||||
|
||||
bool
|
||||
tgba_bdd_product_succ_iterator::done()
|
||||
tgba_product_succ_iterator::done()
|
||||
{
|
||||
return !right_ || right_->done();
|
||||
}
|
||||
|
||||
|
||||
state_bdd_product*
|
||||
tgba_bdd_product_succ_iterator::current_state()
|
||||
tgba_product_succ_iterator::current_state()
|
||||
{
|
||||
return new state_bdd_product(left_->current_state(),
|
||||
right_->current_state());
|
||||
}
|
||||
|
||||
bdd
|
||||
tgba_bdd_product_succ_iterator::current_condition()
|
||||
tgba_product_succ_iterator::current_condition()
|
||||
{
|
||||
return current_cond_;
|
||||
}
|
||||
|
||||
bdd tgba_bdd_product_succ_iterator::current_promise()
|
||||
bdd tgba_product_succ_iterator::current_promise()
|
||||
{
|
||||
return left_->current_promise() & right_->current_promise();
|
||||
}
|
||||
|
||||
////////////////////////////////////////////////////////////
|
||||
// tgba_bdd_product
|
||||
// tgba_product
|
||||
|
||||
tgba_bdd_product::tgba_bdd_product(const tgba& left, const tgba& right)
|
||||
tgba_product::tgba_product(const tgba& left, const tgba& right)
|
||||
: dict_(tgba_bdd_dict_union(left.get_dict(), right.get_dict()))
|
||||
{
|
||||
// Translate the left automaton if needed.
|
||||
|
|
@ -143,7 +143,7 @@ namespace spot
|
|||
}
|
||||
else
|
||||
{
|
||||
left_ = new tgba_bdd_translate_proxy(left, dict_);
|
||||
left_ = new tgba_translate_proxy(left, dict_);
|
||||
left_should_be_freed_ = true;
|
||||
}
|
||||
|
||||
|
|
@ -155,12 +155,12 @@ namespace spot
|
|||
}
|
||||
else
|
||||
{
|
||||
right_ = new tgba_bdd_translate_proxy(right, dict_);
|
||||
right_ = new tgba_translate_proxy(right, dict_);
|
||||
right_should_be_freed_ = true;
|
||||
}
|
||||
}
|
||||
|
||||
tgba_bdd_product::~tgba_bdd_product()
|
||||
tgba_product::~tgba_product()
|
||||
{
|
||||
if (left_should_be_freed_)
|
||||
delete left_;
|
||||
|
|
@ -169,31 +169,31 @@ namespace spot
|
|||
}
|
||||
|
||||
state*
|
||||
tgba_bdd_product::get_init_state() const
|
||||
tgba_product::get_init_state() const
|
||||
{
|
||||
return new state_bdd_product(left_->get_init_state(),
|
||||
right_->get_init_state());
|
||||
}
|
||||
|
||||
tgba_bdd_product_succ_iterator*
|
||||
tgba_bdd_product::succ_iter(const state* state) const
|
||||
tgba_product_succ_iterator*
|
||||
tgba_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);
|
||||
return new tgba_product_succ_iterator(li, ri);
|
||||
}
|
||||
|
||||
const tgba_bdd_dict&
|
||||
tgba_bdd_product::get_dict() const
|
||||
tgba_product::get_dict() const
|
||||
{
|
||||
return dict_;
|
||||
}
|
||||
|
||||
std::string
|
||||
tgba_bdd_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);
|
||||
assert(s);
|
||||
|
|
@ -1,5 +1,5 @@
|
|||
#ifndef SPOT_TGBA_TGBABDDPROD_HH
|
||||
# define SPOT_TGBA_TGBABDDPROD_HH
|
||||
#ifndef SPOT_TGBA_TGBAPRODUCT_HH
|
||||
# define SPOT_TGBA_TGBAPRODUCT_HH
|
||||
|
||||
#include "tgba.hh"
|
||||
#include "statebdd.hh"
|
||||
|
|
@ -7,7 +7,7 @@
|
|||
namespace spot
|
||||
{
|
||||
|
||||
/// \brief A state for spot::tgba_bdd_product.
|
||||
/// \brief A state for spot::tgba_product.
|
||||
///
|
||||
/// This state is in fact a pair of state: the state from the left
|
||||
/// automaton and that of the right.
|
||||
|
|
@ -50,13 +50,13 @@ namespace spot
|
|||
|
||||
|
||||
/// \brief Iterate over the successors of a product computed on the fly.
|
||||
class tgba_bdd_product_succ_iterator: public tgba_succ_iterator
|
||||
class tgba_product_succ_iterator: public tgba_succ_iterator
|
||||
{
|
||||
public:
|
||||
tgba_bdd_product_succ_iterator(tgba_succ_iterator* left,
|
||||
tgba_succ_iterator* right);
|
||||
tgba_product_succ_iterator(tgba_succ_iterator* left,
|
||||
tgba_succ_iterator* right);
|
||||
|
||||
virtual ~tgba_bdd_product_succ_iterator();
|
||||
virtual ~tgba_product_succ_iterator();
|
||||
|
||||
// iteration
|
||||
void first();
|
||||
|
|
@ -82,20 +82,20 @@ namespace spot
|
|||
};
|
||||
|
||||
/// \brief A lazy product. (States are computed on the fly.)
|
||||
class tgba_bdd_product : public tgba
|
||||
class tgba_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);
|
||||
tgba_product(const tgba& left, const tgba& right);
|
||||
|
||||
virtual ~tgba_bdd_product();
|
||||
virtual ~tgba_product();
|
||||
|
||||
virtual state* get_init_state() const;
|
||||
|
||||
virtual tgba_bdd_product_succ_iterator*
|
||||
virtual tgba_product_succ_iterator*
|
||||
succ_iter(const state* state) const;
|
||||
|
||||
virtual const tgba_bdd_dict& get_dict() const;
|
||||
|
|
@ -112,4 +112,4 @@ namespace spot
|
|||
|
||||
}
|
||||
|
||||
#endif // SPOT_TGBA_TGBABDDPROD_HH
|
||||
#endif // SPOT_TGBA_TGBAPRODUCT_HH
|
||||
|
|
@ -1,46 +1,45 @@
|
|||
#include "tgbabddtranslateproxy.hh"
|
||||
#include "tgbatranslateproxy.hh"
|
||||
#include "bddprint.hh"
|
||||
#include <cassert>
|
||||
|
||||
namespace spot
|
||||
{
|
||||
|
||||
// tgba_bdd_translate_proxy_succ_iterator
|
||||
// tgba_translate_proxy_succ_iterator
|
||||
// --------------------------------------
|
||||
|
||||
tgba_bdd_translate_proxy_succ_iterator::
|
||||
tgba_bdd_translate_proxy_succ_iterator(tgba_succ_iterator* it,
|
||||
bddPair* rewrite)
|
||||
tgba_translate_proxy_succ_iterator::
|
||||
tgba_translate_proxy_succ_iterator(tgba_succ_iterator* it,
|
||||
bddPair* rewrite)
|
||||
: iter_(it), rewrite_(rewrite)
|
||||
{
|
||||
}
|
||||
|
||||
tgba_bdd_translate_proxy_succ_iterator::
|
||||
~tgba_bdd_translate_proxy_succ_iterator()
|
||||
tgba_translate_proxy_succ_iterator::~tgba_translate_proxy_succ_iterator()
|
||||
{
|
||||
delete iter_;
|
||||
}
|
||||
|
||||
void
|
||||
tgba_bdd_translate_proxy_succ_iterator::first()
|
||||
tgba_translate_proxy_succ_iterator::first()
|
||||
{
|
||||
iter_->first();
|
||||
}
|
||||
|
||||
void
|
||||
tgba_bdd_translate_proxy_succ_iterator::next()
|
||||
tgba_translate_proxy_succ_iterator::next()
|
||||
{
|
||||
iter_->next();
|
||||
}
|
||||
|
||||
bool
|
||||
tgba_bdd_translate_proxy_succ_iterator::done()
|
||||
tgba_translate_proxy_succ_iterator::done()
|
||||
{
|
||||
return iter_->done();
|
||||
}
|
||||
|
||||
state*
|
||||
tgba_bdd_translate_proxy_succ_iterator::current_state()
|
||||
tgba_translate_proxy_succ_iterator::current_state()
|
||||
{
|
||||
state* s = iter_->current_state();
|
||||
s->translate(rewrite_);
|
||||
|
|
@ -48,23 +47,23 @@ namespace spot
|
|||
}
|
||||
|
||||
bdd
|
||||
tgba_bdd_translate_proxy_succ_iterator::current_condition()
|
||||
tgba_translate_proxy_succ_iterator::current_condition()
|
||||
{
|
||||
return bdd_replace(iter_->current_condition(), rewrite_);
|
||||
}
|
||||
|
||||
bdd
|
||||
tgba_bdd_translate_proxy_succ_iterator::current_promise()
|
||||
tgba_translate_proxy_succ_iterator::current_promise()
|
||||
{
|
||||
return bdd_replace(iter_->current_promise(), rewrite_);
|
||||
}
|
||||
|
||||
|
||||
// tgba_bdd_translate_proxy
|
||||
// tgba_translate_proxy
|
||||
// ------------------------
|
||||
|
||||
tgba_bdd_translate_proxy::tgba_bdd_translate_proxy(const tgba& from,
|
||||
const tgba_bdd_dict& to)
|
||||
tgba_translate_proxy::tgba_translate_proxy(const tgba& from,
|
||||
const tgba_bdd_dict& to)
|
||||
: from_(from), to_(to)
|
||||
{
|
||||
const tgba_bdd_dict& f = from.get_dict();
|
||||
|
|
@ -99,40 +98,40 @@ namespace spot
|
|||
}
|
||||
}
|
||||
|
||||
tgba_bdd_translate_proxy::~tgba_bdd_translate_proxy()
|
||||
tgba_translate_proxy::~tgba_translate_proxy()
|
||||
{
|
||||
bdd_freepair(rewrite_from_);
|
||||
bdd_freepair(rewrite_to_);
|
||||
}
|
||||
|
||||
state*
|
||||
tgba_bdd_translate_proxy::get_init_state() const
|
||||
tgba_translate_proxy::get_init_state() const
|
||||
{
|
||||
state* s = from_.get_init_state();
|
||||
s->translate(rewrite_to_);
|
||||
return s;
|
||||
}
|
||||
|
||||
tgba_bdd_translate_proxy_succ_iterator*
|
||||
tgba_bdd_translate_proxy::succ_iter(const state* s) const
|
||||
tgba_translate_proxy_succ_iterator*
|
||||
tgba_translate_proxy::succ_iter(const state* s) const
|
||||
{
|
||||
state* s2 = s->clone();
|
||||
s2->translate(rewrite_from_);
|
||||
tgba_bdd_translate_proxy_succ_iterator *res =
|
||||
new tgba_bdd_translate_proxy_succ_iterator(from_.succ_iter(s2),
|
||||
tgba_translate_proxy_succ_iterator *res =
|
||||
new tgba_translate_proxy_succ_iterator(from_.succ_iter(s2),
|
||||
rewrite_to_);
|
||||
delete s2;
|
||||
return res;
|
||||
}
|
||||
|
||||
const tgba_bdd_dict&
|
||||
tgba_bdd_translate_proxy::get_dict() const
|
||||
tgba_translate_proxy::get_dict() const
|
||||
{
|
||||
return to_;
|
||||
}
|
||||
|
||||
std::string
|
||||
tgba_bdd_translate_proxy::format_state(const state* s) const
|
||||
tgba_translate_proxy::format_state(const state* s) const
|
||||
{
|
||||
state* s2 = s->clone();
|
||||
s2->translate(rewrite_from_);
|
||||
|
|
@ -1,5 +1,5 @@
|
|||
#ifndef SPOT_TGBA_TGBABDDTRANSLATEPROXY_HH
|
||||
# define SPOT_TGBA_TGBABDDTRANSLATEPROXY_HH
|
||||
#ifndef SPOT_TGBA_TGBATRANSLATEPROXY_HH
|
||||
# define SPOT_TGBA_TGBATRANSLATEPROXY_HH
|
||||
|
||||
#include "tgba.hh"
|
||||
|
||||
|
|
@ -7,12 +7,12 @@ namespace spot
|
|||
{
|
||||
/// \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
|
||||
class tgba_translate_proxy_succ_iterator: public tgba_succ_iterator
|
||||
{
|
||||
public:
|
||||
tgba_bdd_translate_proxy_succ_iterator(tgba_succ_iterator* it,
|
||||
bddPair* rewrite);
|
||||
virtual ~tgba_bdd_translate_proxy_succ_iterator();
|
||||
tgba_translate_proxy_succ_iterator(tgba_succ_iterator* it,
|
||||
bddPair* rewrite);
|
||||
virtual ~tgba_translate_proxy_succ_iterator();
|
||||
|
||||
// iteration
|
||||
void first();
|
||||
|
|
@ -31,20 +31,20 @@ namespace spot
|
|||
|
||||
/// \brief Proxy for a spot::tgba_bdd_concrete that renumber BDD variables
|
||||
/// on the fly.
|
||||
class tgba_bdd_translate_proxy: public tgba
|
||||
class tgba_translate_proxy: public tgba
|
||||
{
|
||||
public:
|
||||
/// \brief Constructor.
|
||||
/// \param from The spot::tgba to masquerade.
|
||||
/// \param to The new dictionary to use.
|
||||
tgba_bdd_translate_proxy(const tgba& from,
|
||||
const tgba_bdd_dict& to);
|
||||
tgba_translate_proxy(const tgba& from,
|
||||
const tgba_bdd_dict& to);
|
||||
|
||||
virtual ~tgba_bdd_translate_proxy();
|
||||
virtual ~tgba_translate_proxy();
|
||||
|
||||
virtual state* get_init_state() const;
|
||||
|
||||
virtual tgba_bdd_translate_proxy_succ_iterator*
|
||||
virtual tgba_translate_proxy_succ_iterator*
|
||||
succ_iter(const state* state) const;
|
||||
|
||||
virtual const tgba_bdd_dict& get_dict() const;
|
||||
|
|
@ -60,4 +60,4 @@ namespace spot
|
|||
|
||||
}
|
||||
|
||||
#endif // SPOT_TGBA_TGBABDDTRANSLATEPROXY_HH
|
||||
#endif // SPOT_TGBA_TGBATRANSLATEPROXY_HH
|
||||
|
|
@ -2,7 +2,7 @@
|
|||
#include <cassert>
|
||||
#include "tgba/ltl2tgba.hh"
|
||||
#include "tgba/tgbaexplicit.hh"
|
||||
#include "tgba/tgbabddprod.hh"
|
||||
#include "tgba/tgbaproduct.hh"
|
||||
#include "tgbaparse/public.hh"
|
||||
#include "tgbaalgos/save.hh"
|
||||
#include "ltlast/allnodes.hh"
|
||||
|
|
@ -33,7 +33,7 @@ main(int argc, char** argv)
|
|||
return 2;
|
||||
|
||||
{
|
||||
spot::tgba_bdd_product p(*a1, *a2);
|
||||
spot::tgba_product p(*a1, *a2);
|
||||
spot::tgba_save_reachable(std::cout, p);
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -4,7 +4,7 @@
|
|||
#include "ltlast/allnodes.hh"
|
||||
#include "ltlparse/public.hh"
|
||||
#include "tgba/ltl2tgba.hh"
|
||||
#include "tgba/tgbabddprod.hh"
|
||||
#include "tgba/tgbaproduct.hh"
|
||||
#include "tgba/tgbabddconcreteproduct.hh"
|
||||
#include "tgbaalgos/dotty.hh"
|
||||
|
||||
|
|
@ -46,7 +46,7 @@ main(int argc, char** argv)
|
|||
#ifdef BDD_CONCRETE_PRODUCT
|
||||
spot::tgba_bdd_concrete p = spot::product(a1, a2);
|
||||
#else
|
||||
spot::tgba_bdd_product p(a1, a2);
|
||||
spot::tgba_product p(a1, a2);
|
||||
#endif
|
||||
|
||||
spot::dotty_reachable(std::cout, p);
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue