diff --git a/ChangeLog b/ChangeLog index d3193a993..a113e88ed 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,6 +1,45 @@ 2003-07-17 Alexandre Duret-Lutz - * 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 diff --git a/iface/gspn/dottygspn.cc b/iface/gspn/dottygspn.cc index 4821d48a2..5d079328b 100644 --- a/iface/gspn/dottygspn.cc +++ b/iface/gspn/dottygspn.cc @@ -1,26 +1,25 @@ #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; } - diff --git a/iface/gspn/gspn.cc b/iface/gspn/gspn.cc index 9a63fc7d8..c68c913f1 100644 --- a/iface/gspn/gspn.cc +++ b/iface/gspn/gspn.cc @@ -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,74 +28,6 @@ namespace spot } - // tgba_gspn_private_ - ////////////////////////////////////////////////////////////////////// - - struct tgba_gspn_private_ - { - int refs; // reference count - - bdd_dict* dict; - typedef std::pair ab_pair; - typedef std::map prop_map; - prop_map prop_dict; - AtomicProp *all_indexes; - size_t index_count; - - tgba_gspn_private_(bdd_dict* dict, const gspn_environment& env) - : refs(0), dict(dict) - { - const gspn_environment::prop_map& p = env.get_prop_map(); - - try - { - for (gspn_environment::prop_map::const_iterator i = p.begin(); - i != p.end(); ++i) - { - int var = dict->register_proposition(i->second, this); - AtomicProp index; - int err = prop_index(i->first.c_str(), &index); - if (err) - throw gspn_exeption("prop_index()", err); - AtomicPropKind kind; - err = prop_kind(index, &kind); - if (err) - throw gspn_exeption("prop_kind()", err); - - prop_dict[index] = ab_pair(kind, bdd_ithvar(var)); - } - - index_count = prop_dict.size(); - all_indexes = new AtomicProp[index_count]; - - unsigned idx = 0; - for (prop_map::const_iterator i = prop_dict.begin(); - i != prop_dict.end(); ++i) - all_indexes[idx++] = i->first; - } - catch (...) - { - // If an exception occurs during the loop, we need to clean - // all BDD variables which have been registered so far. - dict->unregister_all_my_variables(this); - } - } - - tgba_gspn_private_::~tgba_gspn_private_() - { - dict->unregister_all_my_variables(this); - } - - bdd index_to_bdd(AtomicProp index) const - { - if (index == EVENT_TRUE) - return bddtrue; - prop_map::const_iterator i = prop_dict.find(index); - assert(i != prop_dict.end()); - return i->second.second; - } - }; - // state_gspn ////////////////////////////////////////////////////////////////////// @@ -137,6 +69,110 @@ namespace spot }; // state_gspn + // tgba_gspn_private_ + ////////////////////////////////////////////////////////////////////// + + struct tgba_gspn_private_ + { + int refs; // reference count + + bdd_dict* dict; + typedef std::pair ab_pair; + typedef std::map prop_map; + 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), last_state_conds_input(0) + { + const gspn_environment::prop_map& p = env.get_prop_map(); + + try + { + for (gspn_environment::prop_map::const_iterator i = p.begin(); + i != p.end(); ++i) + { + int var = dict->register_proposition(i->second, this); + AtomicProp index; + int err = prop_index(i->first.c_str(), &index); + if (err) + throw gspn_exeption("prop_index()", err); + AtomicPropKind kind; + err = prop_kind(index, &kind); + if (err) + throw gspn_exeption("prop_kind()", err); + + prop_dict[index] = ab_pair(kind, bdd_ithvar(var)); + } + + index_count = prop_dict.size(); + all_indexes = new AtomicProp[index_count]; + + unsigned idx = 0; + for (prop_map::const_iterator i = prop_dict.begin(); + i != prop_dict.end(); ++i) + all_indexes[idx++] = i->first; + } + catch (...) + { + // If an exception occurs during the loop, we need to clean + // all BDD variables which have been registered so far. + dict->unregister_all_my_variables(this); + } + } + + 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 + { + if (index == EVENT_TRUE) + return bddtrue; + prop_map::const_iterator i = prop_dict.find(index); + assert(i != prop_dict.end()); + return i->second.second; + } + + bdd state_conds(const state_gspn* s) + { + // 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); + + if (last_state_conds_input) + delete last_state_conds_input; + last_state_conds_input = s->clone(); + } + return last_state_conds_output; + } + }; + + // tgba_succ_iterator_gspn ////////////////////////////////////////////////////////////////////// @@ -302,31 +338,46 @@ 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(state); assert(s); - - // 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); - + (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_); } + bdd + tgba_gspn::compute_support_conditions(const spot::state* state) const + { + const state_gspn* s = dynamic_cast(state); + assert(s); + return data_->state_conds(s); + } + + 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* tgba_gspn::get_dict() const { diff --git a/iface/gspn/gspn.hh b/iface/gspn/gspn.hh index 7e84be871..5112b8e51 100644 --- a/iface/gspn/gspn.hh +++ b/iface/gspn/gspn.hh @@ -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_; }; diff --git a/src/tgba/Makefile.am b/src/tgba/Makefile.am index 24ec0d0cb..604b4e5e1 100644 --- a/src/tgba/Makefile.am +++ b/src/tgba/Makefile.am @@ -26,6 +26,7 @@ libtgba_la_SOURCES = \ bddprint.cc \ statebdd.cc \ succiterconcrete.cc \ + tgba.cc \ tgbabddconcrete.cc \ tgbabddconcretefactory.cc \ tgbabddconcreteproduct.cc \ diff --git a/src/tgba/tgba.cc b/src/tgba/tgba.cc new file mode 100644 index 000000000..b2042add9 --- /dev/null +++ b/src/tgba/tgba.cc @@ -0,0 +1,49 @@ +#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_; + } + +} diff --git a/src/tgba/tgba.hh b/src/tgba/tgba.hh index f3ee66368..4dc64bbdc 100644 --- a/src/tgba/tgba.hh +++ b/src/tgba/tgba.hh @@ -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 /// Acc[b] and Acc[c] to describe accepting sets, /// this function should return !Acc[a]\&!Acc[b]\&!Acc[c]. /// - /// 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_; }; } diff --git a/src/tgba/tgbabddconcrete.cc b/src/tgba/tgbabddconcrete.cc index 8cc3a7c5a..7face2997 100644 --- a/src/tgba/tgbabddconcrete.cc +++ b/src/tgba/tgbabddconcrete.cc @@ -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(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(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(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 { diff --git a/src/tgba/tgbabddconcrete.hh b/src/tgba/tgbabddconcrete.hh index 6136f6dd2..1e5ef807d 100644 --- a/src/tgba/tgbabddconcrete.hh +++ b/src/tgba/tgbabddconcrete.hh @@ -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: diff --git a/src/tgba/tgbaexplicit.cc b/src/tgba/tgbaexplicit.cc index e6e31be20..f00c1e7b9 100644 --- a/src/tgba/tgbaexplicit.cc +++ b/src/tgba/tgbaexplicit.cc @@ -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(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(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(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 { diff --git a/src/tgba/tgbaexplicit.hh b/src/tgba/tgbaexplicit.hh index 14f0d8423..74be2164b 100644 --- a/src/tgba/tgbaexplicit.hh +++ b/src/tgba/tgbaexplicit.hh @@ -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; @@ -50,6 +52,9 @@ namespace spot 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; + state* add_state(const std::string& name); bdd get_condition(ltl::formula* f); bdd get_accepting_condition(ltl::formula* f); diff --git a/src/tgba/tgbaproduct.cc b/src/tgba/tgbaproduct.cc index 5d90d2984..4b71490f5 100644 --- a/src/tgba/tgbaproduct.cc +++ b/src/tgba/tgbaproduct.cc @@ -171,18 +171,53 @@ namespace spot } tgba_product_succ_iterator* - tgba_product::succ_iter(const state* state) const + tgba_product::succ_iter(const state* local_state, + const state* global_state, + const tgba* global_automaton) const { - const state_bdd_product* s = dynamic_cast(state); + const state_bdd_product* s = + dynamic_cast(local_state); assert(s); - tgba_succ_iterator* li = left_->succ_iter(s->left()); - tgba_succ_iterator* ri = right_->succ_iter(s->right()); + // If global_automaton is not specified, THIS is the root of a + // product tree. + if (! global_automaton) + { + global_automaton = this; + global_state = local_state; + } + + tgba_succ_iterator* li = left_->succ_iter(s->left(), + global_state, global_automaton); + tgba_succ_iterator* ri = right_->succ_iter(s->right(), + global_state, global_automaton); return new tgba_product_succ_iterator(li, ri, left_->neg_accepting_conditions(), right_->neg_accepting_conditions()); } + bdd + tgba_product::compute_support_conditions(const state* in) const + { + const state_bdd_product* s = + dynamic_cast(in); + assert(s); + bdd lsc = left_->support_conditions(s->left()); + bdd rsc = right_->support_conditions(s->right()); + return lsc & rsc; + } + + bdd + tgba_product::compute_support_variables(const state* in) const + { + const state_bdd_product* s = + dynamic_cast(in); + assert(s); + bdd lsc = left_->support_variables(s->left()); + bdd rsc = right_->support_variables(s->right()); + return lsc & rsc; + } + bdd_dict* tgba_product::get_dict() const { diff --git a/src/tgba/tgbaproduct.hh b/src/tgba/tgbaproduct.hh index 9da14ca5d..e2f063d6b 100644 --- a/src/tgba/tgbaproduct.hh +++ b/src/tgba/tgbaproduct.hh @@ -101,7 +101,9 @@ namespace spot virtual state* get_init_state() const; virtual tgba_product_succ_iterator* - succ_iter(const state* state) const; + succ_iter(const state* local_state, + const state* global_state = 0, + const tgba* global_automaton = 0) const; virtual bdd_dict* get_dict() const; @@ -110,6 +112,10 @@ namespace spot virtual bdd all_accepting_conditions() const; 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; + private: bdd_dict* dict_; const tgba* left_;