From 6d18623e4b1f35d3955a13e8289b6416208a21ff Mon Sep 17 00:00:00 2001 From: Guillaume Sadegh Date: Wed, 30 Sep 2009 17:19:06 +0200 Subject: [PATCH] * src/tgba/tgbacomplement.cc: Move functions related to shared_ptr on states... * src/tgba/state.hh: ... here. * src/tgbatest/complementation.test: Do not apply some tests on the new algorithm because it takes to much time to run. --- ChangeLog | 8 ++ src/tgba/state.hh | 93 +++++++++++++++++++++++- src/tgba/tgbacomplement.cc | 117 +++--------------------------- src/tgbatest/complementation.test | 6 ++ 4 files changed, 114 insertions(+), 110 deletions(-) diff --git a/ChangeLog b/ChangeLog index 69983a348..bc474da0f 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,11 @@ +2009-09-30 Guillaume Sadegh + + * src/tgba/tgbacomplement.cc: Move functions related to + shared_ptr on states... + * src/tgba/state.hh: ... here. + * src/tgbatest/complementation.test: Do not apply some tests on + the new algorithm because it takes to much time to run. + 2009-09-29 Guillaume Sadegh A new complementation construction based on ranking. diff --git a/src/tgba/state.hh b/src/tgba/state.hh index 90ecd7b05..3fc25d35b 100644 --- a/src/tgba/state.hh +++ b/src/tgba/state.hh @@ -1,6 +1,6 @@ -// Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), -// département Systèmes Répartis Coopératifs (SRC), Université Pierre -// et Marie Curie. +// Copyright (C) 2003, 2004, 2009 Laboratoire d'Informatique de Paris 6 +// (LIP6), département Systèmes Répartis Coopératifs (SRC), Université +// Pierre et Marie Curie. // // This file is part of Spot, a model checking library. // @@ -26,6 +26,7 @@ #include #include #include +#include namespace spot { @@ -148,6 +149,92 @@ namespace spot } }; + // Functions related to shared_ptr. + ////////////////////////////////////////////////// + + typedef boost::shared_ptr shared_state; + + /// \brief Strict Weak Ordering for \c shared_state + /// (shared_ptr). + /// \ingroup tgba_essentials + /// + /// This is meant to be used as a comparison functor for + /// STL \c map whose key are of type \c shared_state. + /// + /// For instance here is how one could declare + /// a map of \c shared_state. + /// \code + /// // Remember how many times each state has been visited. + /// std::map seen; + /// \endcode + struct state_shared_ptr_less_than: + public std::binary_function + { + bool + operator()(shared_state left, + shared_state right) const + { + assert(left); + return left->compare(right.get()) < 0; + } + }; + + /// \brief An Equivalence Relation for \c shared_state + /// (shared_ptr). + /// \ingroup tgba_essentials + /// + /// This is meant to be used as a comparison functor for + /// Sgi \c hash_map whose key are of type \c shared_state. + /// + /// For instance here is how one could declare + /// a map of \c shared_state + /// \code + /// // Remember how many times each state has been visited. + /// Sgi::hash_map seen; + /// \endcode + struct state_shared_ptr_equal: + public std::binary_function + { + bool + operator()(shared_state left, + shared_state right) const + { + assert(left); + return 0 == left->compare(right.get()); + } + }; + + /// \brief Hash Function for \c shared_state (shared_ptr). + /// \ingroup tgba_essentials + /// \ingroup hash_funcs + /// + /// This is meant to be used as a hash functor for + /// Sgi's \c hash_map whose key are of type + /// \c shared_state. + /// + /// For instance here is how one could declare + /// a map of \c shared_state. + /// \code + /// // Remember how many times each state has been visited. + /// Sgi::hash_map seen; + /// \endcode + struct state_shared_ptr_hash: + public std::unary_function + { + size_t + operator()(shared_state that) const + { + assert(that); + return that->hash(); + } + }; + } #endif // SPOT_TGBA_STATE_HH diff --git a/src/tgba/tgbacomplement.cc b/src/tgba/tgbacomplement.cc index 394bb4ff0..223a62950 100644 --- a/src/tgba/tgbacomplement.cc +++ b/src/tgba/tgbacomplement.cc @@ -1,8 +1,8 @@ #include #include #include -#include #include "bdd.h" +#include "bddprint.hh" #include "state.hh" #include "tgbacomplement.hh" #include "misc/hash.hh" @@ -10,64 +10,10 @@ #include "misc/hashfunc.hh" #include "ltlast/formula.hh" #include "ltlast/constant.hh" +#include "tgbaalgos/stats.hh" namespace spot { - /// \brief An Equivalence Relation for \c boost::shared_ptr. - /// \ingroup tgba_essentials - /// - /// This is meant to be used as a comparison functor for - /// Sgi \c hash_map whose key are of type \c boost::shared_ptr. - /// - /// For instance here is how one could declare - /// a map of \c boost::shared_ptr - /// \code - /// // Remember how many times each state has been visited. - /// Sgi::hash_map, int, - /// spot::state_shared_ptr_hash, - /// spot::state_shared_ptr_equal> seen; - /// \endcode - struct state_shared_ptr_equal: - public std::binary_function, - boost::shared_ptr, bool> - { - bool - operator()(boost::shared_ptr left, - boost::shared_ptr right) const - { - assert(left); - return 0 == left->compare(right.get()); - } - }; - - - /// \brief Hash Function for \c boost::shared_ptr. - /// \ingroup tgba_essentials - /// \ingroup hash_funcs - /// - /// This is meant to be used as a hash functor for - /// Sgi's \c hash_map whose key are of type - /// \c boost::shared_ptr. - /// - /// For instance here is how one could declare - /// a map of \c boost::shared_ptr. - /// \code - /// // Remember how many times each state has been visited. - /// Sgi::hash_map, int, - /// spot::state_shared_ptr_hash, - /// spot::state_shared_ptr_equal> seen; - /// \endcode - struct state_shared_ptr_hash: - public std::unary_function, size_t> - { - size_t - operator()(boost::shared_ptr that) const - { - assert(that); - return that->hash(); - } - }; - namespace { //////////////////////////////////////// @@ -107,14 +53,15 @@ namespace spot return hash; } - std::string format() const + std::string format(const tgba* a) const { std::ostringstream ss; ss << "{rank: " << rank; if (rank & 1) { - ss << ", bdd: {" << condition.order() << ", " << - bddset << condition.get_bdd() << "} "; + ss << ", bdd: {" << condition.order() << ", " + << bdd_format_accset(a->get_dict(), condition.get_bdd()) + << "} "; } ss << "}"; return ss.str(); @@ -122,7 +69,6 @@ namespace spot }; // typedefs. - typedef boost::shared_ptr shared_state; typedef Sgi::hash_map state_rank_map; @@ -130,47 +76,6 @@ namespace spot state_shared_ptr_hash, state_shared_ptr_equal> state_set; - //////////////////////////////////////// - // count_states - - /// \brief Count the number of states in a tgba. - class count_states : public bfs_steps - { - public: - count_states(const tgba* a) - : bfs_steps(a) - { - shared_state s(a->get_init_state()); - states_.insert(s); - - tgba_run::steps l; - search(s.get(), l); - } - - virtual const state* filter(const state* s) - { - shared_state _s(s); - if (states_.find(_s) == states_.end()) - { - states_.insert(_s); - return s; - } - return 0; - } - - virtual bool match(tgba_run::step&, const state*) - { - return false; - } - - size_t size() const - { - return states_.size(); - } - private: - state_set states_; - }; - //////////////////////////////////////// // state_complement @@ -459,6 +364,7 @@ namespace spot return false; } } + return true; } @@ -685,8 +591,8 @@ namespace spot ->register_acceptance_variable(ltl::constant::true_instance(), this); the_acceptance_cond_ = bdd_ithvar(v); { - count_states count(automaton_); - nb_states_ = count.size(); + spot::tgba_statistics a_size = spot::stats_reachable(automaton_); + nb_states_ = a_size.states; } get_acc_list(); } @@ -742,17 +648,14 @@ namespace spot ++i) { ss << " {" << automaton_->format_state(i->first.get()) - << ", " << i->second.format() << "}" << std::endl; + << ", " << i->second.format(this) << "}" << std::endl; } ss << "} odd-less: {"; for (state_set::const_iterator i = state_filter.begin(); i != state_filter.end(); ++i) - { ss << " " << automaton_->format_state(i->get()) << std::endl; - } - ss << "} }"; return ss.str(); } diff --git a/src/tgbatest/complementation.test b/src/tgbatest/complementation.test index aea8f12ca..136620aa4 100755 --- a/src/tgbatest/complementation.test +++ b/src/tgbatest/complementation.test @@ -32,6 +32,12 @@ GFa FGa <>p1->(p0Up1) [](p0-><>p3) +a U b +EOF + +while read f; do + run 0 ../complement -S -f "$f" +done < (p0 U (p1 || [] p0))) [] (p2 -> ((! p0 && ! p1) U (p1 || ((p0 && ! p1) U (p1 || ((! p0 && ! p1) \