From 24099078d62895104589235629563448cbeae377 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 30 Jul 2003 12:41:48 +0000 Subject: [PATCH] * src/tgba/tgba.hh, src/tgba/tgba.cc (tgba::project_state): New method. * src/tgba/tgbaproduct.hh, src/tgba/tgbaproduct.cc (tgba_product::project_state): New method. * src/tgba/tgbabta.hh, src/tgba/tgbabta.cc (tgba_bta_proxy::project_state): New method. * src/tgbaalgos/magic.cc (magic_search::print_result): Take a restrict argument. --- ChangeLog | 11 +++++++++++ src/tgba/tgba.cc | 18 +++++++++++++----- src/tgba/tgba.hh | 15 +++++++++++++++ src/tgba/tgbabddconcrete.hh | 2 +- src/tgba/tgbaproduct.cc | 13 +++++++++++++ src/tgba/tgbaproduct.hh | 2 ++ src/tgba/tgbatba.cc | 14 ++++++++++++-- src/tgba/tgbatba.hh | 2 ++ src/tgbaalgos/magic.cc | 29 ++++++++++++++++++++++++++--- src/tgbaalgos/magic.hh | 18 +++++++++++------- 10 files changed, 106 insertions(+), 18 deletions(-) diff --git a/ChangeLog b/ChangeLog index 5749daac5..114dc438d 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,14 @@ +2003-07-30 Alexandre Duret-Lutz + + * src/tgba/tgba.hh, src/tgba/tgba.cc + (tgba::project_state): New method. + * src/tgba/tgbaproduct.hh, src/tgba/tgbaproduct.cc + (tgba_product::project_state): New method. + * src/tgba/tgbabta.hh, src/tgba/tgbabta.cc + (tgba_bta_proxy::project_state): New method. + * src/tgbaalgos/magic.cc (magic_search::print_result): Take + a restrict argument. + 2003-07-29 Alexandre Duret-Lutz * src/ltlparse/ltlscan.ll: Allow /\, \/, and xor, used in LBTT. diff --git a/src/tgba/tgba.cc b/src/tgba/tgba.cc index b2042add9..80629d9cc 100644 --- a/src/tgba/tgba.cc +++ b/src/tgba/tgba.cc @@ -7,7 +7,7 @@ namespace spot last_support_variables_input_(0) { } - + tgba::~tgba() { if (last_support_conditions_input_) @@ -15,14 +15,14 @@ namespace spot if (last_support_variables_input_) delete last_support_variables_input_; } - - bdd + + bdd tgba::support_conditions(const state* state) const { if (! last_support_conditions_input_ || last_support_conditions_input_->compare(state) != 0) { - last_support_conditions_output_ = + last_support_conditions_output_ = compute_support_conditions(state); if (last_support_conditions_input_) delete last_support_conditions_input_; @@ -37,7 +37,7 @@ namespace spot if (! last_support_variables_input_ || last_support_variables_input_->compare(state) != 0) { - last_support_variables_output_ = + last_support_variables_output_ = compute_support_variables(state); if (last_support_variables_input_) delete last_support_variables_input_; @@ -46,4 +46,12 @@ namespace spot return last_support_variables_output_; } + state* + tgba::project_state(const state* s, const tgba* t) const + { + if (t == this) + return s->clone(); + return 0; + } + } diff --git a/src/tgba/tgba.hh b/src/tgba/tgba.hh index 7fad18bdd..a2e0bacc5 100644 --- a/src/tgba/tgba.hh +++ b/src/tgba/tgba.hh @@ -117,6 +117,21 @@ namespace spot /// who owns the state. virtual std::string format_state(const state* state) const = 0; + /// \brief Project a state on an automata. + /// + /// This converts \a s, into that corresponding spot::state for \a + /// t. This is useful when you have the state of a product, and + /// want restrict this state to a specific automata occuring in + /// the product. + /// + /// It goes without saying that \a s and \a t should be compatible + /// (i.e., \a s is a state of \a t). + /// + /// \return 0 if the projection fails (\a s is unrelated to \a t), + /// or a new \c state* (the projected state) that must be + /// deleted by the caller. + virtual state* project_state(const state* s, const tgba* t) const; + /// \brief Return the set of all accepting conditions used /// by this automaton. /// diff --git a/src/tgba/tgbabddconcrete.hh b/src/tgba/tgbabddconcrete.hh index 1e5ef807d..79ea0ae26 100644 --- a/src/tgba/tgbabddconcrete.hh +++ b/src/tgba/tgbabddconcrete.hh @@ -46,7 +46,7 @@ namespace spot virtual std::string format_state(const state* state) const; - bdd_dict* get_dict() const; + virtual bdd_dict* get_dict() const; /// \brief Get the core data associated to this automaton. /// diff --git a/src/tgba/tgbaproduct.cc b/src/tgba/tgbaproduct.cc index 4b71490f5..8c6aee71b 100644 --- a/src/tgba/tgbaproduct.cc +++ b/src/tgba/tgbaproduct.cc @@ -234,6 +234,19 @@ namespace spot + right_->format_state(s->right())); } + state* + tgba_product::project_state(const state* s, const tgba* t) const + { + const state_bdd_product* s2 = dynamic_cast(s); + assert(s2); + if (t == this) + return s2->clone(); + state* res = left_->project_state(s2->left(), t); + if (res) + return res; + return right_->project_state(s2->right(), t); + } + bdd tgba_product::all_accepting_conditions() const { diff --git a/src/tgba/tgbaproduct.hh b/src/tgba/tgbaproduct.hh index e2f063d6b..e6ddecc25 100644 --- a/src/tgba/tgbaproduct.hh +++ b/src/tgba/tgbaproduct.hh @@ -109,6 +109,8 @@ namespace spot virtual std::string format_state(const state* state) const; + virtual state* project_state(const state* s, const tgba* t) const; + virtual bdd all_accepting_conditions() const; virtual bdd neg_accepting_conditions() const; diff --git a/src/tgba/tgbatba.cc b/src/tgba/tgbatba.cc index 5d19724c6..d3b04289f 100644 --- a/src/tgba/tgbatba.cc +++ b/src/tgba/tgbatba.cc @@ -213,13 +213,23 @@ namespace spot std::string tgba_tba_proxy::format_state(const state* state) const { - const state_tba_proxy* s = - dynamic_cast(state); + const state_tba_proxy* s = dynamic_cast(state); assert(s); return a_->format_state(s->real_state()) + "(" + bdd_format_set(get_dict(), s->accepting_cond()) + ")"; } + state* + tgba_tba_proxy::project_state(const state* s, const tgba* t) const + { + const state_tba_proxy* s2 = dynamic_cast(s); + assert(s2); + if (t == this) + return s2->clone(); + return a_->project_state(s2->real_state(), t); + } + + bdd tgba_tba_proxy::all_accepting_conditions() const { diff --git a/src/tgba/tgbatba.hh b/src/tgba/tgbatba.hh index 46946eacd..1d4119718 100644 --- a/src/tgba/tgbatba.hh +++ b/src/tgba/tgbatba.hh @@ -41,6 +41,8 @@ namespace spot virtual std::string format_state(const state* state) const; + virtual state* project_state(const state* s, const tgba* t) const; + virtual bdd all_accepting_conditions() const; virtual bdd neg_accepting_conditions() const; diff --git a/src/tgbaalgos/magic.cc b/src/tgbaalgos/magic.cc index 604840d46..cd4c1cb3d 100644 --- a/src/tgbaalgos/magic.cc +++ b/src/tgbaalgos/magic.cc @@ -122,7 +122,7 @@ namespace spot } std::ostream& - magic_search::print_result(std::ostream& os) const + magic_search::print_result(std::ostream& os, const tgba* restrict) const { stack_type::const_reverse_iterator i; tstack_type::const_reverse_iterator ti; @@ -133,10 +133,33 @@ namespace spot { if (i->first.s->compare(x) == 0) os <<"Cycle:" <format_state(i->first.s) << std::endl; + + const state* s = i->first.s; + if (restrict) + { + s = a->project_state(s, restrict); + assert(s); + os << " " << restrict->format_state(s) << std::endl; + delete s; + } + else + { + os << " " << a->format_state(s) << std::endl; + } os << " | " << bdd_format_set(d, *ti) << std::endl; } - os << " " << a->format_state(x) << std::endl; + + if (restrict) + { + const state* s = a->project_state(x, restrict); + assert(s); + os << " " << restrict->format_state(s) << std::endl; + delete s; + } + else + { + os << " " << a->format_state(x) << std::endl; + } return os; } diff --git a/src/tgbaalgos/magic.hh b/src/tgbaalgos/magic.hh index 9cfd8a131..482929889 100644 --- a/src/tgbaalgos/magic.hh +++ b/src/tgbaalgos/magic.hh @@ -9,7 +9,7 @@ namespace spot { /// \brief Emptiness check on spot::tgba_tba_proxy automata using - /// the Magic Search algorithm. + /// the Magic Search algorithm. /// /// This algorithm comes from /// \verbatim @@ -38,7 +38,7 @@ namespace spot ~magic_search(); /// \brief Perform a Magic Search. - /// + /// /// \return true iff the algorithm has found a new accepting /// path. /// @@ -46,8 +46,12 @@ namespace spot /// to enumerate all accepting paths. bool check(); - /// Print the last accepting path found. - std::ostream& print_result(std::ostream& os) const; + /// \brief Print the last accepting path found. + /// + /// Restrict printed states to \a the state space of restrict if + /// supplied. + std::ostream& print_result(std::ostream& os, + const tgba* restrict = 0) const; private: @@ -60,7 +64,7 @@ namespace spot bool seen_without : 1; bool seen_with : 1; }; - + /// \brief A state for the spot::magic_search algorithm. struct magic_state { @@ -73,7 +77,7 @@ namespace spot stack_type stack; ///< Stack of visited states on the path. typedef std::list tstack_type; - /// \brief Stack of transitions. + /// \brief Stack of transitions. /// /// This is an addition to the data from the paper. tstack_type tstack; @@ -89,7 +93,7 @@ namespace spot const tgba_tba_proxy* a; ///< The automata to check. /// The state for which we are currently seeking an SCC. - const state* x; + const state* x; };