From eec3a12f80da53b717648c0afb9de1a63241bd55 Mon Sep 17 00:00:00 2001 From: Pierre PARUTTO Date: Thu, 5 Apr 2012 16:20:28 +0200 Subject: [PATCH] Implement sba_explicit class, add tests * src/tgba/tgbaexplicit.hh: Add sba_explicit implementation * src/tgbatest/explicit2.cc: Add test to check the good instantiation of sba_explicit_* --- src/tgba/tgbaexplicit.hh | 118 ++++++++++++++++++++++++++------------ src/tgbatest/explicit2.cc | 84 +++++++++++++++++++++++++++ 2 files changed, 165 insertions(+), 37 deletions(-) diff --git a/src/tgba/tgbaexplicit.hh b/src/tgba/tgbaexplicit.hh index 66b153319..296ad538e 100644 --- a/src/tgba/tgbaexplicit.hh +++ b/src/tgba/tgbaexplicit.hh @@ -61,7 +61,7 @@ namespace spot public: /// A State in an SBA (State-based Buchi Automaton) is accepting /// iff all outgoing transitions are accepting. - virtual bool is_accepting(const spot::state* s) = 0; + virtual bool is_accepting(const spot::state* s) const = 0; }; /// States used by spot::explicit_graph implementation @@ -305,7 +305,10 @@ namespace spot : ls_(), sl_(), init_(0), - dict_(dict) + dict_(dict), + all_acceptance_conditions_(bddfalse), + all_acceptance_conditions_computed_(false), + neg_acceptance_conditions_(bddtrue) { } @@ -486,6 +489,12 @@ namespace spot destroy_key dest; dest.destroy(s); } + + this->dict_->unregister_all_my_variables(this); + // These have already been destroyed by subclasses. + // Prevent destroying by tgba::~tgba. + this->last_support_conditions_input_ = 0; + this->last_support_variables_input_ = 0; } virtual State* get_init_state() const @@ -532,29 +541,6 @@ namespace spot ls_[alias] = *(add_state(real)); } - protected: - - ls_map ls_; - sl_map sl_; - State* init_; - - bdd_dict* dict_; - }; - - template - class tgba_explicit: public explicit_graph - { - public: - typedef typename State::transition transition; - typedef State state; - - tgba_explicit(bdd_dict* dict): - explicit_graph(dict), - all_acceptance_conditions_(bddfalse), - all_acceptance_conditions_computed_(false), - neg_acceptance_conditions_(bddtrue) - { - } /// \brief Copy the acceptance conditions of a tgba. /// @@ -569,7 +555,8 @@ namespace spot neg_acceptance_conditions_ = f; } - /// The acceptance conditions. + + /// Acceptance conditions handlingx void set_acceptance_conditions(bdd acc) { assert(neg_acceptance_conditions_ == bddtrue); @@ -601,17 +588,6 @@ namespace spot t->acceptance_conditions |= f; } - /// tgba interface - virtual ~tgba_explicit() - { - this->dict_->unregister_all_my_variables(this); - // These have already been destroyed by subclasses. - // Prevent destroying by tgba::~tgba. - this->last_support_conditions_input_ = 0; - this->last_support_variables_input_ = 0; - - } - virtual bdd all_acceptance_conditions() const { if (!all_acceptance_conditions_computed_) @@ -696,9 +672,32 @@ namespace spot return res; } + ls_map ls_; + sl_map sl_; + State* init_; + + bdd_dict* dict_; + mutable bdd all_acceptance_conditions_; mutable bool all_acceptance_conditions_computed_; bdd neg_acceptance_conditions_; + }; + + template + class tgba_explicit: public explicit_graph + { + public: + typedef typename State::transition transition; + typedef State state; + + tgba_explicit(bdd_dict* dict): + explicit_graph(dict) + { + } + + virtual ~tgba_explicit() + { + } private: // Disallow copy. @@ -706,10 +705,55 @@ namespace spot tgba_explicit& operator=(const tgba_explicit& other); }; + template + class sba_explicit: public explicit_graph + { + public: + typedef typename State::transition transition; + typedef State state; + sba_explicit(bdd_dict* dict): + explicit_graph(dict) + { + } + + virtual ~sba_explicit() + { + } + + virtual bool is_accepting(const spot::state* s) const + { + bdd acc = bddtrue; + bool transition = false; + + tgba_explicit_succ_iterator* it = this->succ_iter(s); + for (it->first(); !it->done() && acc != bddfalse; it->next()) + { + transition = true; + acc &= it->current_acceptance_conditions(); + } + + delete it; + + return acc != bddfalse && transition; + } + + private: + // Disallow copy. + sba_explicit(const sba_explicit& other); + sba_explicit& operator=(const sba_explicit& other); + }; + + + /// Typedefs for tgba typedef tgba_explicit tgba_explicit_string; typedef tgba_explicit tgba_explicit_formula; typedef tgba_explicit tgba_explicit_number; + + /// Typedefs for sba + typedef sba_explicit sba_explicit_string; + typedef sba_explicit sba_explicit_formula; + typedef sba_explicit sba_explicit_number; } #endif // SPOT_TGBA_TGBAEXPLICIT_HH diff --git a/src/tgbatest/explicit2.cc b/src/tgbatest/explicit2.cc index cfc344ef2..87fa19d7a 100644 --- a/src/tgbatest/explicit2.cc +++ b/src/tgbatest/explicit2.cc @@ -104,6 +104,78 @@ create_tgba_explicit_formula(bdd_dict* d, spot::ltl::default_environment& e) delete tgba; } +void create_sba_explicit_string(bdd_dict* d) +{ + sba_explicit* sba = + new sba_explicit(d); + + state_explicit_string* s1 = sba->add_state("STATE1"); + state_explicit_string* s2 = sba->add_state("STATE2"); + state_explicit_string* s3 = sba->add_state("STATE3"); + + int v = d->register_acceptance_variable(ltl::constant::true_instance(), sba); + + state_explicit_string::transition* t = + sba->create_transition(s1, s2); + + t = sba->create_transition(s1, s3); + sba->add_acceptance_conditions(t, bdd_ithvar(v)); + + std::cout << "S1 ACCEPTING? " << sba->is_accepting (s1) << std::endl; + std::cout << "S2 ACCEPTING? " << sba->is_accepting (s2) << std::endl; + std::cout << "S3 ACCEPTING? " << sba->is_accepting (s3) << std::endl; + + delete sba; +} + +void create_sba_explicit_number(bdd_dict* d) +{ + sba_explicit* sba = + new sba_explicit(d); + + state_explicit_number* s1 = sba->add_state(1); + state_explicit_number* s2 = sba->add_state(2); + + //state 1 is accepting + int v = d->register_acceptance_variable(ltl::constant::true_instance(), sba); + + state_explicit_number::transition* t = + sba->create_transition(s1, s2); + sba->add_acceptance_conditions(t, bdd_ithvar(v)); + + std::cout << "S1 ACCEPTING? " << sba->is_accepting (s1) << std::endl; + std::cout << "S2 ACCEPTING? " << sba->is_accepting (s2) << std::endl; + + delete sba; +} + +void +create_sba_explicit_formula(bdd_dict* d, spot::ltl::default_environment& e) +{ + sba_explicit* sba = + new sba_explicit(d); + + state_explicit_formula* s1 = sba->add_state(e.require("a")); + state_explicit_formula* s2 = sba->add_state(e.require("b")); + state_explicit_formula* s3 = sba->add_state(e.require("c")); + + int v = d->register_acceptance_variable(ltl::constant::true_instance(), sba); + + state_explicit_formula::transition* t = + sba->create_transition(s1, s2); + + sba->add_acceptance_conditions(t, bdd_ithvar(v)); + + t = sba->create_transition(s1, s3); + sba->add_acceptance_conditions(t, bdd_ithvar(v)); + + std::cout << "S1 ACCEPTING? " << sba->is_accepting (s1) << std::endl; + std::cout << "S2 ACCEPTING? " << sba->is_accepting (s2) << std::endl; + std::cout << "S3 ACCEPTING? " << sba->is_accepting (s3) << std::endl; + + delete sba; +} + int main(int argc, char** argv) { @@ -114,10 +186,22 @@ main(int argc, char** argv) spot::ltl::default_environment& e = spot::ltl::default_environment::instance(); + //check tgba creation + std::cout << "* TGBA explicit string" << std::endl; create_tgba_explicit_string(d); + std::cout << "* TGBA explicit number" << std::endl; create_tgba_explicit_number(d); + std::cout << "* TGBA explicit formula" << std::endl; create_tgba_explicit_formula(d, e); + //check sba creation + std::cout << "* SBA explicit string, no accepting state" << std::endl; + create_sba_explicit_string(d); + std::cout << "* SBA explicit number, 1 accepting state" << std::endl; + create_sba_explicit_number(d); + std::cout << "* SBA explicit formula, 1 accepting state" << std::endl; + create_sba_explicit_formula(d, e); + delete d; assert(spot::ltl::atomic_prop::instance_count() == 0); assert(spot::ltl::unop::instance_count() == 0);