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

Now succ_iter() can fetch extra information from

the root of a product to reduce its number of successors.
* src/tgba/Makefile.am (libtgba_la_SOURCES): Add tgba.cc.
* src/tgba/tgba.hh (tgba::succ_iter): Add the global_state and
global_automaton arguments.
(tgba::support_conditions, tgba::support_variables,
tgba::compute_support_conditions, tgba::compute_support_variables):
New functions.
(tgba::last_support_conditions_input_,
tgba::last_support_conditions_output_,
tgba::last_support_variables_input_,
tgba::last_support_variables_output_): New attributes.
* src/tgba/tgbabddconcrete.cc (tgba_bdd_concrete::succ_iter):
Handle the two new arguments.
(tgba_bdd_concrete::compute_support_conditions,
tgba_bdd_concrete::compute_support_variables): Implement them.
* src/tgba/tgbabddconcrete.hh: Adjust.
* src/tgba/tgbaexplicit.cc (tgba_explicit::succ_iter):	Ignore
the two new arguments.
(tgba_explicit::compute_support_conditions,
tgba_explicit::compute_support_variables): Implement them.
* src/tgba/tgbaexplicit.hh: Adjust.
* src/tgba/tgbaproduct.cc (tgba_product::succ_iter): Handle the
two new arguments.
(tgba_product::compute_support_conditions,
tgba_product::compute_support_variables): Implement them.
* src/tgba/tgbaproduct.hh: Adjust.
* iface/gspn/gspn.cc (tgba_gspn_private_::last_state_cond_input,
tgba_gspn_private_::last_state_cond_output,
(tgba_gspn_private_::tgba_gspn_private_): Set last_state_cond_input.
(tgba_gspn_private_::~tgba_gspn_private_): Delete
last_state_cond_input.
(tgba_gspn_private_::state_conds): New function, eved out
from tgba_gspn::succ_iter.
(tgba_gspn::succ_iter): Use it.  Use the two new arguments.
(tgba_gspn::compute_support_conditions,
tgba_gspn::compute_support_variables): New functions.
* iface/gspn/gspn.hh: Adjust.
parent 4bf6c52b
2003-07-17 Alexandre Duret-Lutz <aduret@src.lip6.fr>
* iface/gspn/gspn.cc (EVENT_TRUE): Override temporarily..
Now succ_iter() can fetch extra information from
the root of a product to reduce its number of successors.
* src/tgba/Makefile.am (libtgba_la_SOURCES): Add tgba.cc.
* src/tgba/tgba.hh (tgba::succ_iter): Add the global_state and
global_automaton arguments.
(tgba::support_conditions, tgba::support_variables,
tgba::compute_support_conditions, tgba::compute_support_variables):
New functions.
(tgba::last_support_conditions_input_,
tgba::last_support_conditions_output_,
tgba::last_support_variables_input_,
tgba::last_support_variables_output_): New attributes.
* src/tgba/tgbabddconcrete.cc (tgba_bdd_concrete::succ_iter):
Handle the two new arguments.
(tgba_bdd_concrete::compute_support_conditions,
tgba_bdd_concrete::compute_support_variables): Implement them.
* src/tgba/tgbabddconcrete.hh: Adjust.
* src/tgba/tgbaexplicit.cc (tgba_explicit::succ_iter): Ignore
the two new arguments.
(tgba_explicit::compute_support_conditions,
tgba_explicit::compute_support_variables): Implement them.
* src/tgba/tgbaexplicit.hh: Adjust.
* src/tgba/tgbaproduct.cc (tgba_product::succ_iter): Handle the
two new arguments.
(tgba_product::compute_support_conditions,
tgba_product::compute_support_variables): Implement them.
* src/tgba/tgbaproduct.hh: Adjust.
* iface/gspn/gspn.cc (tgba_gspn_private_::last_state_cond_input,
tgba_gspn_private_::last_state_cond_output,
(tgba_gspn_private_::tgba_gspn_private_): Set last_state_cond_input.
(tgba_gspn_private_::~tgba_gspn_private_): Delete
last_state_cond_input.
(tgba_gspn_private_::state_conds): New function, eved out
from tgba_gspn::succ_iter.
(tgba_gspn::succ_iter): Use it. Use the two new arguments.
(tgba_gspn::compute_support_conditions,
tgba_gspn::compute_support_variables): New functions.
* iface/gspn/gspn.hh: Adjust.
* iface/gspn/gspn.cc (EVENT_TRUE): Override temporarily.
(tgba_gspn::succ_iter): Fix usage of cube.
2003-07-16 Alexandre Duret-Lutz <aduret@src.lip6.fr>
......
#include "gspn.hh"
#include "tgbaalgos/dotty.hh"
int
int
main(int argc, char **argv)
try
{
spot::gspn_interface gspn(argc, argv);
spot::gspn_environment env;
env.declare("obs");
spot::bdd_dict* dict = new spot::bdd_dict();
spot::tgba_gspn a(dict, env);
spot::dotty_reachable(std::cout, &a);
delete dict;
}
catch (spot::gspn_exeption e)
{
{
std::cerr << e << std::endl;
throw;
}
......@@ -5,7 +5,7 @@
#include "gspn.hh"
#include "ltlvisit/destroy.hh"
// FIXME: Override signed definition of EVENT_TRUE until this is fixed
// FIXME: Override signed definition of EVENT_TRUE until this is fixed
// in gspnlib.h.
#undef EVENT_TRUE
#define EVENT_TRUE 0U
......@@ -28,6 +28,47 @@ namespace spot
}
// state_gspn
//////////////////////////////////////////////////////////////////////
class state_gspn: public state
{
public:
state_gspn(State s)
: state_(s)
{
}
virtual
~state_gspn()
{
}
virtual int
compare(const state* other) const
{
const state_gspn* o = dynamic_cast<const state_gspn*>(other);
assert(o);
return reinterpret_cast<char*>(o->get_state())
- reinterpret_cast<char*>(get_state());
}
virtual state_gspn* clone() const
{
return new state_gspn(get_state());
}
State
get_state() const
{
return state_;
}
private:
State state_;
}; // state_gspn
// tgba_gspn_private_
//////////////////////////////////////////////////////////////////////
......@@ -41,9 +82,12 @@ namespace spot
prop_map prop_dict;
AtomicProp *all_indexes;
size_t index_count;
const state_gspn* last_state_conds_input;
bdd last_state_conds_output;
tgba_gspn_private_(bdd_dict* dict, const gspn_environment& env)
: refs(0), dict(dict)
: refs(0), dict(dict), last_state_conds_input(0)
{
const gspn_environment::prop_map& p = env.get_prop_map();
......@@ -84,6 +128,8 @@ namespace spot
tgba_gspn_private_::~tgba_gspn_private_()
{
dict->unregister_all_my_variables(this);
if (last_state_conds_input)
delete last_state_conds_input;
}
bdd index_to_bdd(AtomicProp index) const
......@@ -94,47 +140,37 @@ namespace spot
assert(i != prop_dict.end());
return i->second.second;
}
};
// state_gspn
//////////////////////////////////////////////////////////////////////
class state_gspn: public state
{
public:
state_gspn(State s)
: state_(s)
{
}
virtual
~state_gspn()
{
}
virtual int
compare(const state* other) const
{
const state_gspn* o = dynamic_cast<const state_gspn*>(other);
assert(o);
return reinterpret_cast<char*>(o->get_state())
- reinterpret_cast<char*>(get_state());
}
virtual state_gspn* clone() const
bdd state_conds(const state_gspn* s)
{
return new state_gspn(get_state());
}
// Use cached value if possible.
if (!last_state_conds_input ||
last_state_conds_input->compare(s) != 0)
{
// Build the BDD of the conditions available on this state.
unsigned char* cube = 0;
// This is temporary. We ought to ask only what we need.
AtomicProp* want = all_indexes;
size_t count = index_count;
int res = satisfy(s->get_state(), want, &cube, count);
if (res)
throw gspn_exeption("satisfy()", res);
assert(cube);
last_state_conds_output = bddtrue;
for (size_t i = 0; i < count; ++i)
{
bdd v = index_to_bdd(want[i]);
last_state_conds_output &= cube[i] ? v : !v;
}
satisfy_free(cube);
State
get_state() const
{
return state_;
if (last_state_conds_input)
delete last_state_conds_input;
last_state_conds_input = s->clone();
}
return last_state_conds_output;
}
private:
State state_;
}; // state_gspn
};
// tgba_succ_iterator_gspn
......@@ -302,29 +338,44 @@ namespace spot
}
tgba_succ_iterator*
tgba_gspn::succ_iter(const state* state) const
tgba_gspn::succ_iter(const state* state,
const state* global_state,
const tgba* global_automaton) const
{
const state_gspn* s = dynamic_cast<const state_gspn*>(state);
assert(s);
(void) global_state;
(void) global_automaton;
// FIXME: Should pass global_automaton->support_variables(state)
// to state_conds.
bdd state_conds = data_->state_conds(s);
return new tgba_succ_iterator_gspn(state_conds, s->get_state(), data_);
}
// Build the BDD of the conditions available on this state.
unsigned char* cube = 0;
// This is temporary. We ought to ask only what we need.
AtomicProp* want = data_->all_indexes;
size_t count = data_->index_count;
int res = satisfy(s->get_state(), want, &cube, count);
if (res)
throw gspn_exeption("satisfy()", res);
assert(cube);
bdd state_conds = bddtrue;
for (size_t i = 0; i < count; ++i)
{
bdd v = data_->index_to_bdd(want[i]);
state_conds &= cube[i] ? v : !v;
}
satisfy_free(cube);
bdd
tgba_gspn::compute_support_conditions(const spot::state* state) const
{
const state_gspn* s = dynamic_cast<const state_gspn*>(state);
assert(s);
return data_->state_conds(s);
}
return new tgba_succ_iterator_gspn(state_conds, s->get_state(), data_);
bdd
tgba_gspn::compute_support_variables(const spot::state* state) const
{
// FIXME: At the time of writing, only tgba_gspn calls
// support_variables on the root of a product to gather the
// variables used by all other automata and let GPSN compute only
// these. Because support_variables() is recursive over the
// product treee, tgba_gspn::support_variables should not output
// all the variables known by GSPN; this would ruin the sole
// purpose of this function.
// However this works because we assume there is at most one
// tgba_gspn automata in a product (a legitimate assumption
// since the GSPN API is not re-entrant) and only this automata
// need to call support_variables (now _this_ is shady).
(void) state;
return bddtrue;
}
bdd_dict*
......
......@@ -90,11 +90,17 @@ namespace spot
tgba_gspn& operator=(const tgba_gspn& other);
virtual ~tgba_gspn();
virtual state* get_init_state() const;
virtual tgba_succ_iterator* succ_iter(const state* state) const;
virtual tgba_succ_iterator*
succ_iter(const state* local_state,
const state* global_state = 0,
const tgba* global_automaton = 0) const;
virtual bdd_dict* get_dict() const;
virtual std::string format_state(const state* state) const;
virtual bdd all_accepting_conditions() const;
virtual bdd neg_accepting_conditions() const;
protected:
virtual bdd compute_support_conditions(const spot::state* state) const;
virtual bdd compute_support_variables(const spot::state* state) const;
private:
tgba_gspn_private_* data_;
};
......
......@@ -26,6 +26,7 @@ libtgba_la_SOURCES = \
bddprint.cc \
statebdd.cc \
succiterconcrete.cc \
tgba.cc \
tgbabddconcrete.cc \
tgbabddconcretefactory.cc \
tgbabddconcreteproduct.cc \
......
#include "tgba.hh"
namespace spot
{
tgba::tgba()
: last_support_conditions_input_(0),
last_support_variables_input_(0)
{
}
tgba::~tgba()
{
if (last_support_conditions_input_)
delete last_support_conditions_input_;
if (last_support_variables_input_)
delete last_support_variables_input_;
}
bdd
tgba::support_conditions(const state* state) const
{
if (! last_support_conditions_input_
|| last_support_conditions_input_->compare(state) != 0)
{
last_support_conditions_output_ =
compute_support_conditions(state);
if (last_support_conditions_input_)
delete last_support_conditions_input_;
last_support_conditions_input_ = state->clone();
}
return last_support_conditions_output_;
}
bdd
tgba::support_variables(const state* state) const
{
if (! last_support_variables_input_
|| last_support_variables_input_->compare(state) != 0)
{
last_support_variables_output_ =
compute_support_variables(state);
if (last_support_variables_input_)
delete last_support_variables_input_;
last_support_variables_input_ = state->clone();
}
return last_support_variables_output_;
}
}
......@@ -31,12 +31,11 @@ namespace spot
/// a state.
class tgba
{
public:
virtual
~tgba()
{
}
protected:
tgba();
virtual ~tgba();
public:
/// \brief Get the initial state of the automaton.
///
/// The state has been allocated with \c new. It is the
......@@ -44,18 +43,63 @@ namespace spot
/// longer needed.
virtual state* get_init_state() const = 0;
/// \brief Get an iterator over the successors of \a state.
/// \brief Get an iterator over the successors of \a local_state.
///
/// The iterator has been allocated with \c new. It is the
/// responsability of the caller to \c delete it when no
/// longer needed.
///
/// \param state is the state whose successors are to be explored.
/// During synchornized products, additional informations are
/// passed about the entire product and its state. Recall that
/// products can be nested, forming a tree of spot::tgba where
/// most values are computed on demand. \a global_automaton
/// designate the root spot::tgba, and \a global_state its
/// state. This two objects can be used by succ_iter() to
/// restrict the set of successors to compute.
///
/// \param local_state The state whose successors are to be explored.
/// This pointer is not adopted in any way by \c succ_iter, and
/// it is still the caller's responsability to delete it when
/// appropriate (this can be done during the lifetime of
/// the iterator).
virtual tgba_succ_iterator* succ_iter(const state* state) const = 0;
/// \param global_state In a product, the state of the global
/// product automaton. Otherwise, 0. Like \a locale_state,
/// \a global_state is not adopted by \c succ_iter.
/// \param global_automaton In a product, the state of the global
/// product automaton. Otherwise, 0.
virtual tgba_succ_iterator*
succ_iter(const state* local_state,
const state* global_state = 0,
const tgba* global_automaton = 0) const = 0;
/// \brief Get a formula that must hold whatever successor is taken.
///
/// \return A formula which must be verified for all successors
/// of \a state.
///
/// This can be as simple as \c bddtrue, or more completely
/// the disjunction of the condition of all successors. This
/// is used as an hint by \c succ_iter() to reduce the number
/// of successor to compute in a product.
///
/// Sub classes should implement compute_support_conditions(),
/// this function is just a wrapper that will cache the
/// last return value for efficiency.
bdd support_conditions(const state* state) const;
/// \brief Get the conjunctions of variables tested by
/// the outgoing transitions of \a state.
///
/// All variables tested by outgoing transitions must be
/// returned. This is mandatory.
///
/// This is used as an hint by some \c succ_iter() to reduce the
/// number of successor to compute in a product.
///
/// Sub classes should implement compute_support_variables(),
/// this function is just a wrapper that will cache the
/// last return value for efficiency.
bdd support_variables(const state* state) const;
/// \brief Get the dictionary associated to the automaton.
///
......@@ -89,10 +133,21 @@ namespace spot
/// <tt>Acc[b]</tt> and <tt>Acc[c]</tt> to describe accepting sets,
/// this function should return <tt>!Acc[a]\&!Acc[b]\&!Acc[c]</tt>.
///
/// This is useful when making products: each operand conditions
/// This is useful when making products: each operand's condition
/// set should be augmented with the neg_accepting_conditions() of
/// the other operand.
virtual bdd neg_accepting_conditions() const = 0;
protected:
/// Do the actual computation of tgba::support_conditions().
virtual bdd compute_support_conditions(const state* state) const = 0;
/// Do the actual computation of tgba::support_variables().
virtual bdd compute_support_variables(const state* state) const = 0;
private:
mutable const state* last_support_conditions_input_;
mutable bdd last_support_conditions_output_;
mutable const state* last_support_variables_input_;
mutable bdd last_support_variables_output_;
};
}
......
......@@ -71,14 +71,46 @@ namespace spot
}
tgba_succ_iterator_concrete*
tgba_bdd_concrete::succ_iter(const state* state) const
tgba_bdd_concrete::succ_iter(const state* state,
const state* global_state,
const tgba* global_automaton) const
{
const state_bdd* s = dynamic_cast<const state_bdd*>(state);
assert(s);
bdd succ_set = data_.relation & s->as_bdd();
// If we are in a product, inject the local conditions of
// all other automata to limit the number of successors.
if (global_automaton)
{
bdd varused = bdd_support(succ_set);
bdd global_conds = global_automaton->support_conditions(global_state);
succ_set = bdd_appexcomp(succ_set, global_conds, bddop_and, varused);
}
return new tgba_succ_iterator_concrete(data_, succ_set);
}
bdd
tgba_bdd_concrete::compute_support_conditions(const state* st) const
{
const state_bdd* s = dynamic_cast<const state_bdd*>(st);
assert(s);
return bdd_relprod(s->as_bdd(), data_.relation, data_.notvar_set);
}
bdd
tgba_bdd_concrete::compute_support_variables(const state* st) const
{
const state_bdd* s = dynamic_cast<const state_bdd*>(st);
assert(s);
bdd succ_set = data_.relation & s->as_bdd();
// bdd_support must be called BEFORE bdd_exist
// because bdd_exist(bdd_support((a&Next[f])|(!a&Next[g])),Next[*])
// is obviously not the same as bdd_support(a|!a).
// In other words: we can reuse compute_support_conditions() for
// this computation.
return bdd_exist(bdd_support(succ_set), data_.notvar_set);
}
std::string
tgba_bdd_concrete::format_state(const state* state) const
{
......
......@@ -21,12 +21,12 @@ namespace spot
/// \brief Construct a tgba_bdd_concrete with known initial state.
tgba_bdd_concrete(const tgba_bdd_factory& fact, bdd init);
~tgba_bdd_concrete();
virtual ~tgba_bdd_concrete();
/// \brief Set the initial state.
void set_init_state(bdd s);
virtual void set_init_state(bdd s);
state_bdd* get_init_state() const;
virtual state_bdd* get_init_state() const;
/// \brief Get the initial state directly as a BDD.
///
......@@ -39,9 +39,12 @@ namespace spot
/// \endcode
bdd get_init_bdd() const;
tgba_succ_iterator_concrete* succ_iter(const state* state) const;
virtual tgba_succ_iterator_concrete*
succ_iter(const state* local_state,
const state* global_state = 0,
const tgba* global_automaton = 0) const;
std::string format_state(const state* state) const;
virtual std::string format_state(const state* state) const;
bdd_dict* get_dict() const;
......@@ -56,6 +59,9 @@ namespace spot
virtual bdd neg_accepting_conditions() const;
protected:
virtual bdd compute_support_conditions(const state* state) const;
virtual bdd compute_support_variables(const state* state) const;
tgba_bdd_core_data data_; ///< Core data associated to the automaton.
bdd init_; ///< Initial state.
private:
......
......@@ -206,14 +206,46 @@ namespace spot
}
tgba_succ_iterator*
tgba_explicit::succ_iter(const spot::state* state) const
tgba_explicit::succ_iter(const spot::state* state,
const spot::state* global_state,
const tgba* global_automaton) const
{
const state_explicit* s = dynamic_cast<const state_explicit*>(state);
assert(s);
(void) global_state;
(void) global_automaton;
return new tgba_explicit_succ_iterator(s->get_state(),
all_accepting_conditions());
}
bdd
tgba_explicit::compute_support_conditions(const spot::state* in) const
{
const state_explicit* s = dynamic_cast<const state_explicit*>(in);
assert(s);
const state* st = s->get_state();
bdd res = bddtrue;
tgba_explicit::state::const_iterator i;
for (i = st->begin(); i != st->end(); ++i)
res |= (*i)->condition;
return res;
}
bdd
tgba_explicit::compute_support_variables(const spot::state* in) const
{
const state_explicit* s = dynamic_cast<const state_explicit*>(in);
assert(s);
const state* st = s->get_state();
bdd res = bddtrue;
tgba_explicit::state::const_iterator i;
for (i = st->begin(); i != st->end(); ++i)
res &= bdd_support((*i)->condition);
return res;
}
bdd_dict*
tgba_explicit::get_dict() const
{
......
......@@ -42,7 +42,9 @@ namespace spot
virtual ~tgba_explicit();
virtual spot::state* get_init_state() const;
virtual tgba_succ_iterator*
succ_iter(const spot::state* state) const;
succ_iter(const spot::state* local_state,
const spot::state* global_state = 0,
const tgba* global_automaton = 0) const;
virtual bdd_dict* get_dict() const;
virtual std::string format_state(const spot::state* state) const;