diff --git a/ChangeLog b/ChangeLog index 9da0df4c0..104cbf510 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,22 @@ +2004-10-18 Alexandre Duret-Lutz + + * iface/gspn/gspn.cc, src/ltlvisit/basicreduce.cc, + src/ltlvisit/destroy.cc, src/ltlvisit/dotty.cc, + src/ltlvisit/dump.cc, src/ltlvisit/length.cc, + src/ltlvisit/nenoform.cc, src/ltlvisit/reduce.cc, + src/ltlvisit/syntimpl.cc, src/ltlvisit/tostring.cc, + src/tgba/formula2bdd.cc, src/tgba/tgbabddconcreteproduct.cc, + src/tgba/tgbatba.cc, src/tgbaalgos/dotty.cc, + src/tgbaalgos/dupexp.cc, src/tgbaalgos/lbtt.cc, + src/tgbaalgos/ltl2tgba_lacim.cc, src/tgbaalgos/neverclaim.cc, + src/tgbaalgos/save.cc, src/tgbaalgos/stats.cc, + src/tgbaalgos/gtec/nsheap.cc, src/tgbaalgos/gtec/nsheap.hh: + Declare private classes and helper function in anonymous namespaces. + * HACKING, src/sanity/style.test: Document and check this. + Also check for trailing { after namespace or class. + * src/ltlast/predecl.hh, src/ltlast/visitor.hh, + src/tgba/tgbareduc.hh: Fix trailing {. + 2004-10-15 Alexandre Duret-Lutz * src/tgbaalgos/gtec/ce.cc: Reinstall change from 2004-09-21. diff --git a/HACKING b/HACKING index 3c1b4651e..0f5c03c72 100644 --- a/HACKING +++ b/HACKING @@ -249,3 +249,9 @@ Other style recommandations Prefer when predeclarations are sufficient, and then use for instance use just in the corresponding .cc file. (A plain is needed when using std::cout, std::cerr, etc.) + + * Always declare helper functions and other local class definitions + (used in a single .cc files) in anonymous namespaces. (The risk + otherwise is to declare two classes with the same name: the linker + will ignore one of the two silently. The resulting bugs are often + difficult to understand.) diff --git a/iface/gspn/gspn.cc b/iface/gspn/gspn.cc index 10b8723ee..931833513 100644 --- a/iface/gspn/gspn.cc +++ b/iface/gspn/gspn.cc @@ -27,439 +27,443 @@ namespace spot { - // state_gspn - ////////////////////////////////////////////////////////////////////// - - class state_gspn: public state + namespace { - public: - state_gspn(State s) - : state_(s) + // 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(other); + assert(o); + return reinterpret_cast(o->get_state()) + - reinterpret_cast(get_state()); + } + + virtual size_t + hash() const + { + return reinterpret_cast(get_state()) - static_cast(0); + } + + 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_ + ////////////////////////////////////////////////////////////////////// + + 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; + bdd alive_prop; + bdd dead_prop; + + tgba_gspn_private_(bdd_dict* dict, ltl::declarative_environment& env, + const std::string& dead) + : refs(1), dict(dict), all_indexes(0), last_state_conds_input(0) + { + const ltl::declarative_environment::prop_map& p = env.get_prop_map(); + + try + { + for (ltl::declarative_environment::prop_map::const_iterator i + = p.begin(); i != p.end(); ++i) + { + // Skip the DEAD proposition, GreatSPN knows nothing + // about it. + if (i->first == dead) + continue; + + 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(" + i->first + ")", err); + AtomicPropKind kind; + err = prop_kind(index, &kind); + if (err) + throw gspn_exeption("prop_kind(" + i->first + ")", 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); + throw; + } + + // Register the "dead" proposition. There are three cases to + // consider: + // * If DEAD is "false", it means we are not interested in finite + // sequences of the system. + // * If DEAD is "true", we want to check finite sequences as well + // as infinite sequences, but do not need to distinguish them. + // * If DEAD is any other string, this is the name a property + // that should be true when looping on a dead state, and false + // otherwise. + // We handle these three cases by setting ALIVE_PROP and DEAD_PROP + // appropriately. ALIVE_PROP is the bdd that should be ANDed + // to all transitions leaving a live state, while DEAD_PROP should + // be ANDed to all transitions leaving a dead state. + if (!strcasecmp(dead.c_str(), "false")) + { + alive_prop = bddtrue; + dead_prop = bddfalse; + } + else if (!strcasecmp(dead.c_str(), "true")) + { + alive_prop = bddtrue; + dead_prop = bddtrue; + } + else + { + ltl::formula* f = env.require(dead); + assert(f); + int var = dict->register_proposition(f, this); + dead_prop = bdd_ithvar(var); + alive_prop = bdd_nithvar(var); + } + } + + tgba_gspn_private_::~tgba_gspn_private_() + { + dict->unregister_all_my_variables(this); + if (last_state_conds_input) + delete last_state_conds_input; + if (all_indexes) + delete[] all_indexes; + } + + 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; + // FIXME: 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 + ////////////////////////////////////////////////////////////////////// + + class tgba_succ_iterator_gspn: public tgba_succ_iterator + { + public: + tgba_succ_iterator_gspn(bdd state_conds, State state, + tgba_gspn_private_* data) + : state_conds_(state_conds), + successors_(0), + size_(0), + current_(0), + data_(data), + from_state_(state) + { + int res = succ(state, &successors_, &size_); + if (res) + throw gspn_exeption("succ()", res); + // GreatSPN should return successors_ == 0 and size_ == 0 when a + // state has no successors. + assert((size_ <= 0) ^ (successors_ != 0)); + // If we have to stutter on a dead state, we have one successor. + if (size_ <= 0 && data_->dead_prop != bddfalse) + size_ = 1; + } + + virtual + ~tgba_succ_iterator_gspn() + { + if (successors_) + succ_free(successors_); + } + + virtual void + first() + { + current_ = 0; + } + + virtual void + next() + { + assert(!done()); + ++current_; + } + + virtual bool + done() const + { + return current_ >= size_; + } + + virtual state* + current_state() const + { + // If GreatSPN returned no successor, we stutter on the dead state. + return + new state_gspn(successors_ ? successors_[current_].s : from_state_); + } + + virtual bdd + current_condition() const + { + if (successors_) + { + bdd p = data_->index_to_bdd(successors_[current_].p); + return state_conds_ & p & data_->alive_prop; + } + else + { + return state_conds_ & data_->dead_prop; + } + } + + virtual bdd + current_acceptance_conditions() const + { + // There is no acceptance conditions in GSPN systems. + return bddfalse; + } + private: + bdd state_conds_; /// All conditions known on STATE. + EventPropSucc* successors_; /// array of successors + size_t size_; /// size of successors_ + size_t current_; /// current position in successors_ + tgba_gspn_private_* data_; + State from_state_; + }; // tgba_succ_iterator_gspn + + + // tgba_gspn + ////////////////////////////////////////////////////////////////////// + + + + + /// Data private to tgba_gspn. + struct tgba_gspn_private_; + + class tgba_gspn: public tgba + { + public: + tgba_gspn(bdd_dict* dict, ltl::declarative_environment& env, + const std::string& dead); + tgba_gspn(const tgba_gspn& other); + tgba_gspn& operator=(const tgba_gspn& other); + virtual ~tgba_gspn(); + virtual state* get_init_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_acceptance_conditions() const; + virtual bdd neg_acceptance_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_; + }; + + + tgba_gspn::tgba_gspn(bdd_dict* dict, ltl::declarative_environment& env, + const std::string& dead) + { + data_ = new tgba_gspn_private_(dict, env, dead); } - virtual - ~state_gspn() + tgba_gspn::tgba_gspn(const tgba_gspn& other) + : tgba() { + data_ = other.data_; + ++data_->refs; } - virtual int - compare(const state* other) const + tgba_gspn::~tgba_gspn() { - const state_gspn* o = dynamic_cast(other); - assert(o); - return reinterpret_cast(o->get_state()) - - reinterpret_cast(get_state()); + if (--data_->refs == 0) + delete data_; } - virtual size_t - hash() const + tgba_gspn& + tgba_gspn::operator=(const tgba_gspn& other) { - return reinterpret_cast(get_state()) - static_cast(0); + if (&other == this) + return *this; + this->~tgba_gspn(); + new (this) tgba_gspn(other); + return *this; } - virtual state_gspn* clone() const + state* tgba_gspn::get_init_state() const { - return new state_gspn(get_state()); + State s; + int err = initial_state(&s); + if (err) + throw gspn_exeption("initial_state()", err); + return new state_gspn(s); } - State - get_state() const + tgba_succ_iterator* + tgba_gspn::succ_iter(const state* state, + const state* global_state, + const tgba* global_automaton) const { - return state_; + const state_gspn* s = dynamic_cast(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_); } - private: - State state_; - }; // 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; - bdd alive_prop; - bdd dead_prop; - - tgba_gspn_private_(bdd_dict* dict, ltl::declarative_environment& env, - const std::string& dead) - : refs(1), dict(dict), all_indexes(0), last_state_conds_input(0) + bdd + tgba_gspn::compute_support_conditions(const spot::state* state) const { - const ltl::declarative_environment::prop_map& p = env.get_prop_map(); - - try - { - for (ltl::declarative_environment::prop_map::const_iterator i - = p.begin(); i != p.end(); ++i) - { - // Skip the DEAD proposition, GreatSPN knows nothing - // about it. - if (i->first == dead) - continue; - - 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(" + i->first + ")", err); - AtomicPropKind kind; - err = prop_kind(index, &kind); - if (err) - throw gspn_exeption("prop_kind(" + i->first + ")", 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); - throw; - } - - // Register the "dead" proposition. There are three cases to - // consider: - // * If DEAD is "false", it means we are not interested in finite - // sequences of the system. - // * If DEAD is "true", we want to check finite sequences as well - // as infinite sequences, but do not need to distinguish them. - // * If DEAD is any other string, this is the name a property - // that should be true when looping on a dead state, and false - // otherwise. - // We handle these three cases by setting ALIVE_PROP and DEAD_PROP - // appropriately. ALIVE_PROP is the bdd that should be ANDed - // to all transitions leaving a live state, while DEAD_PROP should - // be ANDed to all transitions leaving a dead state. - if (!strcasecmp(dead.c_str(), "false")) - { - alive_prop = bddtrue; - dead_prop = bddfalse; - } - else if (!strcasecmp(dead.c_str(), "true")) - { - alive_prop = bddtrue; - dead_prop = bddtrue; - } - else - { - ltl::formula* f = env.require(dead); - assert(f); - int var = dict->register_proposition(f, this); - dead_prop = bdd_ithvar(var); - alive_prop = bdd_nithvar(var); - } + const state_gspn* s = dynamic_cast(state); + assert(s); + return data_->state_conds(s); } - tgba_gspn_private_::~tgba_gspn_private_() + bdd + tgba_gspn::compute_support_variables(const spot::state* state) const { - dict->unregister_all_my_variables(this); - if (last_state_conds_input) - delete last_state_conds_input; - if (all_indexes) - delete[] all_indexes; + // 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 index_to_bdd(AtomicProp index) const + bdd_dict* + tgba_gspn::get_dict() 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; + return data_->dict; } - bdd state_conds(const state_gspn* s) + std::string + tgba_gspn::format_state(const state* state) const { - // 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; - // FIXME: 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 - ////////////////////////////////////////////////////////////////////// - - class tgba_succ_iterator_gspn: public tgba_succ_iterator - { - public: - tgba_succ_iterator_gspn(bdd state_conds, State state, - tgba_gspn_private_* data) - : state_conds_(state_conds), - successors_(0), - size_(0), - current_(0), - data_(data), - from_state_(state) - { - int res = succ(state, &successors_, &size_); - if (res) - throw gspn_exeption("succ()", res); - // GreatSPN should return successors_ == 0 and size_ == 0 when a - // state has no successors. - assert((size_ <= 0) ^ (successors_ != 0)); - // If we have to stutter on a dead state, we have one successor. - if (size_ <= 0 && data_->dead_prop != bddfalse) - size_ = 1; + const state_gspn* s = dynamic_cast(state); + assert(s); + char* str; + int err = print_state(s->get_state(), &str); + if (err) + throw gspn_exeption("print_state()", err); + // Strip trailing \n... + unsigned len = strlen(str); + while (str[--len] == '\n') + str[len] = 0; + std::string res(str); + free(str); + return res; } - virtual - ~tgba_succ_iterator_gspn() - { - if (successors_) - succ_free(successors_); - } - - virtual void - first() - { - current_ = 0; - } - - virtual void - next() - { - assert(!done()); - ++current_; - } - - virtual bool - done() const - { - return current_ >= size_; - } - - virtual state* - current_state() const - { - // If GreatSPN returned no successor, we stutter on the dead state. - return - new state_gspn(successors_ ? successors_[current_].s : from_state_); - } - - virtual bdd - current_condition() const - { - if (successors_) - { - bdd p = data_->index_to_bdd(successors_[current_].p); - return state_conds_ & p & data_->alive_prop; - } - else - { - return state_conds_ & data_->dead_prop; - } - } - - virtual bdd - current_acceptance_conditions() const + bdd + tgba_gspn::all_acceptance_conditions() const { // There is no acceptance conditions in GSPN systems. return bddfalse; } - private: - bdd state_conds_; /// All conditions known on STATE. - EventPropSucc* successors_; /// array of successors - size_t size_; /// size of successors_ - size_t current_; /// current position in successors_ - tgba_gspn_private_* data_; - State from_state_; - }; // tgba_succ_iterator_gspn + bdd + tgba_gspn::neg_acceptance_conditions() const + { + // There is no acceptance conditions in GSPN systems. + return bddtrue; + } - // tgba_gspn - ////////////////////////////////////////////////////////////////////// - - - - - /// Data private to tgba_gspn. - struct tgba_gspn_private_; - - class tgba_gspn: public tgba - { - public: - tgba_gspn(bdd_dict* dict, ltl::declarative_environment& env, - const std::string& dead); - tgba_gspn(const tgba_gspn& other); - tgba_gspn& operator=(const tgba_gspn& other); - virtual ~tgba_gspn(); - virtual state* get_init_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_acceptance_conditions() const; - virtual bdd neg_acceptance_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_; - }; - - - tgba_gspn::tgba_gspn(bdd_dict* dict, ltl::declarative_environment& env, - const std::string& dead) - { - data_ = new tgba_gspn_private_(dict, env, dead); - } - - tgba_gspn::tgba_gspn(const tgba_gspn& other) - : tgba() - { - data_ = other.data_; - ++data_->refs; - } - - tgba_gspn::~tgba_gspn() - { - if (--data_->refs == 0) - delete data_; - } - - tgba_gspn& - tgba_gspn::operator=(const tgba_gspn& other) - { - if (&other == this) - return *this; - this->~tgba_gspn(); - new (this) tgba_gspn(other); - return *this; - } - - state* tgba_gspn::get_init_state() const - { - State s; - int err = initial_state(&s); - if (err) - throw gspn_exeption("initial_state()", err); - return new state_gspn(s); - } - - tgba_succ_iterator* - 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); - (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 - { - return data_->dict; - } - - std::string - tgba_gspn::format_state(const state* state) const - { - const state_gspn* s = dynamic_cast(state); - assert(s); - char* str; - int err = print_state(s->get_state(), &str); - if (err) - throw gspn_exeption("print_state()", err); - // Strip trailing \n... - unsigned len = strlen(str); - while (str[--len] == '\n') - str[len] = 0; - std::string res(str); - free(str); - return res; - } - - bdd - tgba_gspn::all_acceptance_conditions() const - { - // There is no acceptance conditions in GSPN systems. - return bddfalse; - } - - bdd - tgba_gspn::neg_acceptance_conditions() const - { - // There is no acceptance conditions in GSPN systems. - return bddtrue; - } + } // anonymous // gspn_interface ////////////////////////////////////////////////////////////////////// diff --git a/src/ltlast/predecl.hh b/src/ltlast/predecl.hh index b28b80aa8..121c9ef5d 100644 --- a/src/ltlast/predecl.hh +++ b/src/ltlast/predecl.hh @@ -29,8 +29,10 @@ #ifndef SPOT_LTLAST_PREDECL_HH # define SPOT_LTLAST_PREDECL_HH -namespace spot { - namespace ltl { +namespace spot +{ + namespace ltl + { struct visitor; struct const_visitor; diff --git a/src/ltlast/visitor.hh b/src/ltlast/visitor.hh index ba0445595..5d7e77eb2 100644 --- a/src/ltlast/visitor.hh +++ b/src/ltlast/visitor.hh @@ -26,9 +26,10 @@ #include "predecl.hh" -namespace spot { - namespace ltl { - +namespace spot +{ + namespace ltl + { /// \brief Formula visitor that can modify the formula. /// /// Writing visitors is the prefered way diff --git a/src/ltlvisit/basicreduce.cc b/src/ltlvisit/basicreduce.cc index 222a52a9c..a49e161f1 100644 --- a/src/ltlvisit/basicreduce.cc +++ b/src/ltlvisit/basicreduce.cc @@ -31,7 +31,6 @@ namespace spot { namespace ltl { - bool is_GF(const formula* f) { @@ -58,527 +57,532 @@ namespace spot return false; } - formula* basic_reduce(const formula* f); - - class basic_reduce_visitor : public visitor + namespace { - public: - - basic_reduce_visitor(){} - - virtual ~basic_reduce_visitor(){} - - formula* - result() const + class basic_reduce_visitor: public visitor { - return result_; - } + public: - void - visit(atomic_prop* ap) - { - formula* f = ap->ref(); - result_ = f; - } + basic_reduce_visitor(){} - void - visit(constant* c) - { - result_ = c; - } + virtual ~basic_reduce_visitor(){} - formula* - param_case(multop* mo, unop::type op, multop::type op_child) - { - formula* result; - multop::vec* res1 = new multop::vec; - multop::vec* resGF = new multop::vec; - unsigned mos = mo->size(); - for (unsigned i = 0; i < mos; ++i) - if (is_GF(mo->nth(i))) - resGF->push_back(clone(mo->nth(i))); + formula* + result() const + { + return result_; + } + + void + visit(atomic_prop* ap) + { + formula* f = ap->ref(); + result_ = f; + } + + void + visit(constant* c) + { + result_ = c; + } + + formula* + param_case(multop* mo, unop::type op, multop::type op_child) + { + formula* result; + multop::vec* res1 = new multop::vec; + multop::vec* resGF = new multop::vec; + unsigned mos = mo->size(); + for (unsigned i = 0; i < mos; ++i) + if (is_GF(mo->nth(i))) + resGF->push_back(clone(mo->nth(i))); + else + res1->push_back(clone(mo->nth(i))); + destroy(mo); + multop::vec* res3 = new multop::vec; + if (!res1->empty()) + res3->push_back(unop::instance(op, + multop::instance(op_child, res1))); else - res1->push_back(clone(mo->nth(i))); - destroy(mo); - multop::vec* res3 = new multop::vec; - if (!res1->empty()) - res3->push_back(unop::instance(op, - multop::instance(op_child, res1))); - else - delete res1; - if (!resGF->empty()) - res3->push_back(multop::instance(op_child, resGF)); - else - delete resGF; - result = multop::instance(op_child, res3); - return result; - } + delete res1; + if (!resGF->empty()) + res3->push_back(multop::instance(op_child, resGF)); + else + delete resGF; + result = multop::instance(op_child, res3); + return result; + } - void - visit(unop* uo) - { - formula* f = uo->child(); - result_ = basic_reduce(f); - multop* mo = 0; - unop* u = 0; - binop* bo = 0; - switch (uo->op()) - { - case unop::Not: - result_ = unop::instance(unop::Not, result_); - return; - - case unop::X: - // X(true) = true - // X(false) = false - if (dynamic_cast(result_)) + void + visit(unop* uo) + { + formula* f = uo->child(); + result_ = basic_reduce(f); + multop* mo = 0; + unop* u = 0; + binop* bo = 0; + switch (uo->op()) + { + case unop::Not: + result_ = unop::instance(unop::Not, result_); return; - // XGF(f) = GF(f) - if (is_GF(result_)) + case unop::X: + // X(true) = true + // X(false) = false + if (dynamic_cast(result_)) + return; + + // XGF(f) = GF(f) + if (is_GF(result_)) + return; + + // X(f1 & GF(f2)) = X(f1) & GF(F2) + // X(f1 | GF(f2)) = X(f1) | GF(F2) + mo = dynamic_cast(result_); + if (mo) + { + result_ = param_case(mo, unop::X, mo->op()); + return; + } + + result_ = unop::instance(unop::X, result_); return; - // X(f1 & GF(f2)) = X(f1) & GF(F2) - // X(f1 | GF(f2)) = X(f1) | GF(F2) - mo = dynamic_cast(result_); - if (mo) - { - result_ = param_case(mo, unop::X, mo->op()); + case unop::F: + // F(true) = true + // F(false) = false + if (dynamic_cast(result_)) + return; + + // FX(a) = XF(a) + u = dynamic_cast(result_); + if (u && u->op() == unop::X) + { + result_ = + unop::instance(unop::X, + unop::instance(unop::F, + basic_reduce(u->child()))); + destroy(u); return; } - result_ = unop::instance(unop::X, result_); - return; + // F(f1 & GF(f2)) = F(f1) & GF(F2) + mo = dynamic_cast(result_); + if (mo && mo->op() == multop::And) + { + result_ = param_case(mo, unop::F, multop::And); + return; + } - case unop::F: - // F(true) = true - // F(false) = false - if (dynamic_cast(result_)) + result_ = unop::instance(unop::F, result_); return; - // FX(a) = XF(a) - u = dynamic_cast(result_); - if (u && u->op() == unop::X) - { - result_ = - unop::instance(unop::X, - unop::instance(unop::F, - basic_reduce(u->child()))); - destroy(u); + case unop::G: + // G(true) = true + // G(false) = false + if (dynamic_cast(result_)) + return; + + // G(a R b) = G(b) + bo = dynamic_cast(result_); + if (bo && bo->op() == binop::R) + { + result_ = unop::instance(unop::G, + basic_reduce(bo->second())); + destroy(bo); + return; + } + + // GX(a) = XG(a) + u = dynamic_cast(result_); + if (u && u->op() == unop::X) + { + result_ = + unop::instance(unop::X, + unop::instance(unop::G, + basic_reduce(u->child()))); + destroy(u); + return; + } + + // G(f1 | GF(f2)) = G(f1) | GF(F2) + mo = dynamic_cast(result_); + if (mo && mo->op() == multop::Or) + { + result_ = param_case(mo, unop::G, multop::Or); + return; + } + + result_ = unop::instance(unop::G, result_); return; } + /* Unreachable code. */ + assert(0); + } - // F(f1 & GF(f2)) = F(f1) & GF(F2) - mo = dynamic_cast(result_); - if (mo && mo->op() == multop::And) - { - result_ = param_case(mo, unop::F, multop::And); - return; - } - - result_ = unop::instance(unop::F, result_); - return; - - case unop::G: - // G(true) = true - // G(false) = false - if (dynamic_cast(result_)) + void + visit(binop* bo) + { + formula* f1 = bo->first(); + formula* f2 = bo->second(); + unop* fu1; + unop* fu2; + switch (bo->op()) + { + case binop::Xor: + case binop::Equiv: + case binop::Implies: + result_ = binop::instance(bo->op(), + basic_reduce(f1), + basic_reduce(f2)); return; + case binop::U: + case binop::R: + f2 = basic_reduce(f2); - // G(a R b) = G(b) - bo = dynamic_cast(result_); - if (bo && bo->op() == binop::R) - { - result_ = unop::instance(unop::G, - basic_reduce(bo->second())); - destroy(bo); - return; + // a U false = false + // a U true = true + // a R false = false + // a R true = true + if (dynamic_cast(f2)) + { + result_ = f2; + return; + } + + f1 = basic_reduce(f1); + + // X(a) U X(b) = X(a U b) + // X(a) R X(b) = X(a R b) + fu1 = dynamic_cast(f1); + fu2 = dynamic_cast(f2); + if (fu1 && fu2 + && fu1->op() == unop::X + && fu2->op() == unop::X) + { + formula* ftmp = binop::instance(bo->op(), + basic_reduce(fu1->child()), + basic_reduce(fu2->child())); + result_ = unop::instance(unop::X, basic_reduce(ftmp)); + destroy(f1); + destroy(f2); + destroy(ftmp); + return; } - // GX(a) = XG(a) - u = dynamic_cast(result_); - if (u && u->op() == unop::X) - { - result_ = - unop::instance(unop::X, - unop::instance(unop::G, - basic_reduce(u->child()))); - destroy(u); - return; - } - - // G(f1 | GF(f2)) = G(f1) | GF(F2) - mo = dynamic_cast(result_); - if (mo && mo->op() == multop::Or) - { - result_ = param_case(mo, unop::G, multop::Or); - return; - } - - result_ = unop::instance(unop::G, result_); - return; - } - /* Unreachable code. */ - assert(0); - } - - void - visit(binop* bo) - { - formula* f1 = bo->first(); - formula* f2 = bo->second(); - unop* fu1; - unop* fu2; - switch (bo->op()) - { - case binop::Xor: - case binop::Equiv: - case binop::Implies: - result_ = binop::instance(bo->op(), - basic_reduce(f1), - basic_reduce(f2)); - return; - case binop::U: - case binop::R: - f2 = basic_reduce(f2); - - // a U false = false - // a U true = true - // a R false = false - // a R true = true - if (dynamic_cast(f2)) - { - result_ = f2; - return; - } - - f1 = basic_reduce(f1); - - // X(a) U X(b) = X(a U b) - // X(a) R X(b) = X(a R b) - fu1 = dynamic_cast(f1); - fu2 = dynamic_cast(f2); - if (fu1 && fu2 - && fu1->op() == unop::X - && fu2->op() == unop::X) - { - formula* ftmp = binop::instance(bo->op(), - basic_reduce(fu1->child()), - basic_reduce(fu2->child())); - result_ = unop::instance(unop::X, basic_reduce(ftmp)); - destroy(f1); - destroy(f2); - destroy(ftmp); - return; + result_ = binop::instance(bo->op(), f1, f2); + return; } + /* Unreachable code. */ + assert(0); + } - result_ = binop::instance(bo->op(), f1, f2); - return; - } - /* Unreachable code. */ - assert(0); - } + void + visit(multop* mo) + { + multop::type op = mo->op(); + unsigned mos = mo->size(); + multop::vec* res = new multop::vec; - void - visit(multop* mo) - { - multop::type op = mo->op(); - unsigned mos = mo->size(); - multop::vec* res = new multop::vec; + multop::vec* tmpX = new multop::vec; + multop::vec* tmpU = new multop::vec; + multop::vec* tmpR = new multop::vec; + multop::vec* tmpFG = new multop::vec; + multop::vec* tmpGF = new multop::vec; - multop::vec* tmpX = new multop::vec; - multop::vec* tmpU = new multop::vec; - multop::vec* tmpR = new multop::vec; - multop::vec* tmpFG = new multop::vec; - multop::vec* tmpGF = new multop::vec; + multop::vec* tmpOther = new multop::vec; - multop::vec* tmpOther = new multop::vec; + for (unsigned i = 0; i < mos; ++i) + res->push_back(basic_reduce(mo->nth(i))); - for (unsigned i = 0; i < mos; ++i) - res->push_back(basic_reduce(mo->nth(i))); + switch (op) + { + case multop::And: - switch (op) - { - case multop::And: - - for (multop::vec::iterator i = res->begin(); i != res->end(); i++) - { - // FIXME: why would *i be 0 ? - if (!*i) - continue; - unop* uo = dynamic_cast(*i); - binop* bo = dynamic_cast(*i); - if (uo) - { - if (uo && uo->op() == unop::X) - { - // Xa & Xb = X(a & b) - tmpX->push_back(clone(uo->child())); - } - else if (is_FG(*i)) - { - // FG(a) & FG(b) = FG(a & b) - unop* uo2 = dynamic_cast(uo->child()); - tmpFG->push_back(clone(uo2->child())); - } - else - { - tmpOther->push_back(clone(*i)); - } - } - else if (bo) - { - if (bo->op() == binop::U) - { - // (a U b) & (c U b) = (a & c) U b - formula* ftmp = dynamic_cast(*i)->second(); - multop::vec* tmpUright = new multop::vec; - for (multop::vec::iterator j = i; j != res->end(); j++) - { - if (!*j) - continue; - binop* bo2 = dynamic_cast(*j); - if (bo2 && bo2->op() == binop::U - && ftmp == bo2->second()) - { - tmpUright - ->push_back(clone(bo2->first())); - if (j != i) - { - destroy(*j); - *j = 0; - } - } - } - tmpU - ->push_back(binop::instance(binop::U, - multop:: - instance(multop:: - And, - tmpUright), - clone(ftmp))); - } - else if (bo->op() == binop::R) - { - // (a R b) & (a R c) = a R (b & c) - formula* ftmp = dynamic_cast(*i)->first(); - multop::vec* tmpRright = new multop::vec; - for (multop::vec::iterator j = i; j != res->end(); j++) - { - if (!*j) - continue; - binop* bo2 = dynamic_cast(*j); - if (bo2 && bo2->op() == binop::R - && ftmp == bo2->first()) - { - tmpRright - ->push_back(clone(bo2->second())); - if (j != i) - { - destroy(*j); - *j = 0; - } - } - } - tmpR - ->push_back(binop::instance(binop::R, - clone(ftmp), - multop:: - instance(multop::And, - tmpRright))); - } - else - { - tmpOther->push_back(clone(*i)); - } - } - else - { - tmpOther->push_back(clone(*i)); - } - destroy(*i); - } - - delete tmpGF; - tmpGF = 0; - - break; - - case multop::Or: - - for (multop::vec::iterator i = res->begin(); i != res->end(); i++) - { - if (!*i) - continue; - unop* uo = dynamic_cast(*i); - binop* bo = dynamic_cast(*i); - if (uo) - { - if (uo && uo->op() == unop::X) - { - // Xa | Xb = X(a | b) - tmpX->push_back(clone(uo->child())); - } - else if (is_GF(*i)) - { - // GF(a) | GF(b) = GF(a | b) - unop* uo2 = dynamic_cast(uo->child()); - tmpGF->push_back(clone(uo2->child())); - } - else if (is_FG(*i)) - { - // FG(a) | FG(b) = F(Ga | Gb) - tmpFG->push_back(clone(uo->child())); - } - else - { - tmpOther->push_back(clone(*i)); - } - } - else if (bo) - { - if (bo->op() == binop::U) - { - // (a U b) | (a U c) = a U (b | c) - formula* ftmp = bo->first(); - multop::vec* tmpUright = new multop::vec; - for (multop::vec::iterator j = i; j != res->end(); j++) - { - if (!*j) - continue; - binop* bo2 = dynamic_cast(*j); - if (bo2 && bo2->op() == binop::U - && ftmp == bo2->first()) - { - tmpUright - ->push_back(clone(bo2->second())); - if (j != i) - { - destroy(*j); - *j = 0; - } - } - } - tmpU->push_back(binop::instance(binop::U, + for (multop::vec::iterator i = res->begin(); i != res->end(); i++) + { + // FIXME: why would *i be 0 ? + if (!*i) + continue; + unop* uo = dynamic_cast(*i); + binop* bo = dynamic_cast(*i); + if (uo) + { + if (uo && uo->op() == unop::X) + { + // Xa & Xb = X(a & b) + tmpX->push_back(clone(uo->child())); + } + else if (is_FG(*i)) + { + // FG(a) & FG(b) = FG(a & b) + unop* uo2 = dynamic_cast(uo->child()); + tmpFG->push_back(clone(uo2->child())); + } + else + { + tmpOther->push_back(clone(*i)); + } + } + else if (bo) + { + if (bo->op() == binop::U) + { + // (a U b) & (c U b) = (a & c) U b + formula* ftmp = dynamic_cast(*i)->second(); + multop::vec* tmpUright = new multop::vec; + for (multop::vec::iterator j = i; j != res->end(); + j++) + { + if (!*j) + continue; + binop* bo2 = dynamic_cast(*j); + if (bo2 && bo2->op() == binop::U + && ftmp == bo2->second()) + { + tmpUright + ->push_back(clone(bo2->first())); + if (j != i) + { + destroy(*j); + *j = 0; + } + } + } + tmpU + ->push_back(binop::instance(binop::U, + multop:: + instance(multop:: + And, + tmpUright), + clone(ftmp))); + } + else if (bo->op() == binop::R) + { + // (a R b) & (a R c) = a R (b & c) + formula* ftmp = dynamic_cast(*i)->first(); + multop::vec* tmpRright = new multop::vec; + for (multop::vec::iterator j = i; j != res->end(); + j++) + { + if (!*j) + continue; + binop* bo2 = dynamic_cast(*j); + if (bo2 && bo2->op() == binop::R + && ftmp == bo2->first()) + { + tmpRright + ->push_back(clone(bo2->second())); + if (j != i) + { + destroy(*j); + *j = 0; + } + } + } + tmpR + ->push_back(binop::instance(binop::R, clone(ftmp), + multop:: + instance(multop::And, + tmpRright))); + } + else + { + tmpOther->push_back(clone(*i)); + } + } + else + { + tmpOther->push_back(clone(*i)); + } + destroy(*i); + } + + delete tmpGF; + tmpGF = 0; + + break; + + case multop::Or: + + for (multop::vec::iterator i = res->begin(); i != res->end(); i++) + { + if (!*i) + continue; + unop* uo = dynamic_cast(*i); + binop* bo = dynamic_cast(*i); + if (uo) + { + if (uo && uo->op() == unop::X) + { + // Xa | Xb = X(a | b) + tmpX->push_back(clone(uo->child())); + } + else if (is_GF(*i)) + { + // GF(a) | GF(b) = GF(a | b) + unop* uo2 = dynamic_cast(uo->child()); + tmpGF->push_back(clone(uo2->child())); + } + else if (is_FG(*i)) + { + // FG(a) | FG(b) = F(Ga | Gb) + tmpFG->push_back(clone(uo->child())); + } + else + { + tmpOther->push_back(clone(*i)); + } + } + else if (bo) + { + if (bo->op() == binop::U) + { + // (a U b) | (a U c) = a U (b | c) + formula* ftmp = bo->first(); + multop::vec* tmpUright = new multop::vec; + for (multop::vec::iterator j = i; j != res->end(); + j++) + { + if (!*j) + continue; + binop* bo2 = dynamic_cast(*j); + if (bo2 && bo2->op() == binop::U + && ftmp == bo2->first()) + { + tmpUright + ->push_back(clone(bo2->second())); + if (j != i) + { + destroy(*j); + *j = 0; + } + } + } + tmpU->push_back(binop::instance(binop::U, + clone(ftmp), + multop:: + instance(multop::Or, + tmpUright))); + } + else if (bo->op() == binop::R) + { + // (a R b) | (c R b) = (a | c) R b + formula* ftmp = dynamic_cast(*i)->second(); + multop::vec* tmpRright = new multop::vec; + for (multop::vec::iterator j = i; j != res->end(); + j++) + { + if (!*j) + continue; + binop* bo2 = dynamic_cast(*j); + if (bo2 && bo2->op() == binop::R + && ftmp == bo2->second()) + { + tmpRright + ->push_back(clone(bo2->first())); + if (j != i) + { + destroy(*j); + *j = 0; + } + } + } + tmpR + ->push_back(binop::instance(binop::R, multop:: instance(multop::Or, - tmpUright))); - } - else if (bo->op() == binop::R) - { - // (a R b) | (c R b) = (a | c) R b - formula* ftmp = dynamic_cast(*i)->second(); - multop::vec* tmpRright = new multop::vec; - for (multop::vec::iterator j = i; j != res->end(); j++) - { - if (!*j) - continue; - binop* bo2 = dynamic_cast(*j); - if (bo2 && bo2->op() == binop::R - && ftmp == bo2->second()) - { - tmpRright - ->push_back(clone(bo2->first())); - if (j != i) - { - destroy(*j); - *j = 0; - } - } - } - tmpR - ->push_back(binop::instance(binop::R, - multop:: - instance(multop::Or, - tmpRright), - clone(ftmp))); - } - else - { - tmpOther->push_back(clone(*i)); - } - } - else - { - tmpOther->push_back(clone(*i)); - } - destroy(*i); - } + tmpRright), + clone(ftmp))); + } + else + { + tmpOther->push_back(clone(*i)); + } + } + else + { + tmpOther->push_back(clone(*i)); + } + destroy(*i); + } - /* - delete tmpFG; - tmpFG = 0; - */ + /* + delete tmpFG; + tmpFG = 0; + */ - break; - } + break; + } - res->clear(); - delete res; + res->clear(); + delete res; - if (tmpX && !tmpX->empty()) - tmpOther->push_back(unop::instance(unop::X, - multop::instance(mo->op(), - tmpX))); - else if (tmpX) - delete tmpX; + if (tmpX && !tmpX->empty()) + tmpOther->push_back(unop::instance(unop::X, + multop::instance(mo->op(), + tmpX))); + else if (tmpX) + delete tmpX; - if (tmpU && !tmpU->empty()) - tmpOther->push_back(multop::instance(mo->op(), tmpU)); - else if (tmpU) - delete tmpU; + if (tmpU && !tmpU->empty()) + tmpOther->push_back(multop::instance(mo->op(), tmpU)); + else if (tmpU) + delete tmpU; - if (tmpR && !tmpR->empty()) - tmpOther->push_back(multop::instance(mo->op(), tmpR)); - else if (tmpR) - delete tmpR; + if (tmpR && !tmpR->empty()) + tmpOther->push_back(multop::instance(mo->op(), tmpR)); + else if (tmpR) + delete tmpR; - if (tmpGF && !tmpGF->empty()) - { - formula* ftmp - = unop::instance(unop::G, - unop::instance(unop::F, - multop::instance(mo->op(), - tmpGF))); - tmpOther->push_back(ftmp); - } - else if (tmpGF) - delete tmpGF; - - - if (tmpFG && !tmpFG->empty()) - { - formula* ftmp = 0; - if (mo->op() == multop::And) - ftmp - = unop::instance(unop::F, - unop::instance(unop::G, + if (tmpGF && !tmpGF->empty()) + { + formula* ftmp + = unop::instance(unop::G, + unop::instance(unop::F, multop::instance(mo->op(), - tmpFG))); - else - ftmp - = unop::instance(unop::F, - multop::instance(mo->op(), tmpFG)); - tmpOther->push_back(ftmp); - } - else if (tmpFG) - delete tmpFG; + tmpGF))); + tmpOther->push_back(ftmp); + } + else if (tmpGF) + delete tmpGF; - result_ = multop::instance(op, tmpOther); + if (tmpFG && !tmpFG->empty()) + { + formula* ftmp = 0; + if (mo->op() == multop::And) + ftmp + = unop::instance(unop::F, + unop::instance(unop::G, + multop::instance(mo->op(), + tmpFG))); + else + ftmp + = unop::instance(unop::F, + multop::instance(mo->op(), tmpFG)); + tmpOther->push_back(ftmp); + } + else if (tmpFG) + delete tmpFG; - return; - } + result_ = multop::instance(op, tmpOther); - protected: - formula* result_; - }; + return; + + } + + protected: + formula* result_; + }; + } formula* basic_reduce(const formula* f) diff --git a/src/ltlvisit/destroy.cc b/src/ltlvisit/destroy.cc index 11f5f8ce5..131136d42 100644 --- a/src/ltlvisit/destroy.cc +++ b/src/ltlvisit/destroy.cc @@ -1,4 +1,4 @@ -// Copyright (C) 2003 Laboratoire d'Informatique de Paris 6 (LIP6), +// 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. // @@ -25,16 +25,18 @@ namespace spot { namespace ltl { - - class destroy_visitor : public postfix_visitor + namespace { - public: - virtual void - doit_default(formula* c) + class destroy_visitor: public postfix_visitor { - formula::unref(c); - } - }; + public: + virtual void + doit_default(formula* c) + { + formula::unref(c); + } + }; + } void destroy(const formula* f) diff --git a/src/ltlvisit/dotty.cc b/src/ltlvisit/dotty.cc index c16e831d3..67611b00c 100644 --- a/src/ltlvisit/dotty.cc +++ b/src/ltlvisit/dotty.cc @@ -29,99 +29,101 @@ namespace spot { namespace ltl { - - class dotty_visitor : public const_visitor + namespace { - public: - typedef Sgi::hash_map > map; - dotty_visitor(std::ostream& os, map& m) - : os_(os), father_(-1), node_(m) + class dotty_visitor: public const_visitor { - } + public: + typedef Sgi::hash_map > map; + dotty_visitor(std::ostream& os, map& m) + : os_(os), father_(-1), node_(m) + { + } - virtual - ~dotty_visitor() - { - } + virtual + ~dotty_visitor() + { + } - void - visit(const atomic_prop* ap) - { - draw_node_(ap, ap->name(), true); - } + void + visit(const atomic_prop* ap) + { + draw_node_(ap, ap->name(), true); + } - void - visit(const constant* c) - { - draw_node_(c, c->val_name(), true); - } + void + visit(const constant* c) + { + draw_node_(c, c->val_name(), true); + } - void - visit(const binop* bo) - { - if (draw_node_(bo, bo->op_name())) - { - dotty_visitor v(*this); - bo->first()->accept(v); - bo->second()->accept(*this); - } - } + void + visit(const binop* bo) + { + if (draw_node_(bo, bo->op_name())) + { + dotty_visitor v(*this); + bo->first()->accept(v); + bo->second()->accept(*this); + } + } - void - visit(const unop* uo) - { - if (draw_node_(uo, uo->op_name())) - uo->child()->accept(*this); - } + void + visit(const unop* uo) + { + if (draw_node_(uo, uo->op_name())) + uo->child()->accept(*this); + } - void - visit(const multop* mo) - { - if (!draw_node_(mo, mo->op_name())) - return; - unsigned max = mo->size(); - for (unsigned n = 0; n < max; ++n) - { - dotty_visitor v(*this); - mo->nth(n)->accept(v); - } - } - private: - std::ostream& os_; - int father_; - map& node_; + void + visit(const multop* mo) + { + if (!draw_node_(mo, mo->op_name())) + return; + unsigned max = mo->size(); + for (unsigned n = 0; n < max; ++n) + { + dotty_visitor v(*this); + mo->nth(n)->accept(v); + } + } + private: + std::ostream& os_; + int father_; + map& node_; - bool - draw_node_(const formula* f, const std::string& str, bool rec = false) - { - map::iterator i = node_.find(f); - int node; - bool node_exists = false; - if (i != node_.end()) - { - node = i->second; - node_exists = true; - } - else - { - node = node_.size(); - node_[f] = node; - } - // the link - if (father_ >= 0) - os_ << " " << father_ << " -> " << node << ";" << std::endl; - father_ = node; - // the node - if (node_exists) - return false; - os_ << " " << node - << " [label=\"" << str << "\""; - if (rec) - os_ << ", shape=box"; - os_ << "];" << std::endl; - return true; - } - }; + bool + draw_node_(const formula* f, const std::string& str, bool rec = false) + { + map::iterator i = node_.find(f); + int node; + bool node_exists = false; + if (i != node_.end()) + { + node = i->second; + node_exists = true; + } + else + { + node = node_.size(); + node_[f] = node; + } + // the link + if (father_ >= 0) + os_ << " " << father_ << " -> " << node << ";" << std::endl; + father_ = node; + // the node + if (node_exists) + return false; + os_ << " " << node + << " [label=\"" << str << "\""; + if (rec) + os_ << ", shape=box"; + os_ << "];" << std::endl; + return true; + } + }; + } std::ostream& dotty(std::ostream& os, const formula* f) diff --git a/src/ltlvisit/dump.cc b/src/ltlvisit/dump.cc index 452bd5b5a..97f7b866b 100644 --- a/src/ltlvisit/dump.cc +++ b/src/ltlvisit/dump.cc @@ -28,66 +28,68 @@ namespace spot { namespace ltl { - - class dump_visitor : public const_visitor + namespace { - public: - dump_visitor(std::ostream& os) - : os_(os) + class dump_visitor: public const_visitor { - } + public: + dump_visitor(std::ostream& os) + : os_(os) + { + } - virtual - ~dump_visitor() - { - } + virtual + ~dump_visitor() + { + } - void - visit(const atomic_prop* ap) - { - os_ << "AP(" << ap->name() << ")"; - } + void + visit(const atomic_prop* ap) + { + os_ << "AP(" << ap->name() << ")"; + } - void - visit(const constant* c) - { - os_ << "constant(" << c->val_name() << ")"; - } + void + visit(const constant* c) + { + os_ << "constant(" << c->val_name() << ")"; + } - void - visit(const binop* bo) - { - os_ << "binop(" << bo->op_name() << ", "; - bo->first()->accept(*this); - os_ << ", "; - bo->second()->accept(*this); - os_ << ")"; - } + void + visit(const binop* bo) + { + os_ << "binop(" << bo->op_name() << ", "; + bo->first()->accept(*this); + os_ << ", "; + bo->second()->accept(*this); + os_ << ")"; + } - void - visit(const unop* uo) - { - os_ << "unop(" << uo->op_name() << ", "; - uo->child()->accept(*this); - os_ << ")"; - } + void + visit(const unop* uo) + { + os_ << "unop(" << uo->op_name() << ", "; + uo->child()->accept(*this); + os_ << ")"; + } - void - visit(const multop* mo) - { - os_ << "multop(" << mo->op_name() << ", "; - unsigned max = mo->size(); - mo->nth(0)->accept(*this); - for (unsigned n = 1; n < max; ++n) - { - os_ << ", "; - mo->nth(n)->accept(*this); - } - os_ << ")"; - } - private: - std::ostream& os_; - }; + void + visit(const multop* mo) + { + os_ << "multop(" << mo->op_name() << ", "; + unsigned max = mo->size(); + mo->nth(0)->accept(*this); + for (unsigned n = 1; n < max; ++n) + { + os_ << ", "; + mo->nth(n)->accept(*this); + } + os_ << ")"; + } + private: + std::ostream& os_; + }; + } std::ostream& dump(std::ostream& os, const formula* f) diff --git a/src/ltlvisit/length.cc b/src/ltlvisit/length.cc index 882431889..ed9fe9276 100644 --- a/src/ltlvisit/length.cc +++ b/src/ltlvisit/length.cc @@ -27,62 +27,64 @@ namespace spot { namespace ltl { - - class length_visitor : public const_visitor + namespace { - public: - - length_visitor() + class length_visitor: public const_visitor { - result_ = 0; - } + public: - virtual - ~length_visitor() - { - } + length_visitor() + { + result_ = 0; + } - int - result() const - { - return result_; - } + virtual + ~length_visitor() + { + } - void - visit(const atomic_prop*) - { - result_ = 1; - } + int + result() const + { + return result_; + } - void - visit(const constant*) - { - result_ = 1; - } + void + visit(const atomic_prop*) + { + result_ = 1; + } - void - visit(const unop* uo) - { - result_ = 1 + length(uo->child()); - } + void + visit(const constant*) + { + result_ = 1; + } - void - visit(const binop* bo) - { - result_ = 1 + length(bo->first()) + length(bo->second()); - } + void + visit(const unop* uo) + { + result_ = 1 + length(uo->child()); + } - void - visit(const multop* mo) - { - unsigned mos = mo->size(); - for (unsigned i = 0; i < mos; ++i) - result_ += length(mo->nth(i)); - } + void + visit(const binop* bo) + { + result_ = 1 + length(bo->first()) + length(bo->second()); + } - protected: - int result_; // size of the formula - }; + void + visit(const multop* mo) + { + unsigned mos = mo->size(); + for (unsigned i = 0; i < mos; ++i) + result_ += length(mo->nth(i)); + } + + protected: + int result_; // size of the formula + }; + } int length(const formula* f) diff --git a/src/ltlvisit/nenoform.cc b/src/ltlvisit/nenoform.cc index 302c3ab06..208992461 100644 --- a/src/ltlvisit/nenoform.cc +++ b/src/ltlvisit/nenoform.cc @@ -27,166 +27,170 @@ namespace spot { namespace ltl { - - class negative_normal_form_visitor : public visitor + namespace { - public: - negative_normal_form_visitor(bool negated) - : negated_(negated) + class negative_normal_form_visitor: public visitor { - } + public: + negative_normal_form_visitor(bool negated) + : negated_(negated) + { + } - virtual - ~negative_normal_form_visitor() - { - } + virtual + ~negative_normal_form_visitor() + { + } - formula* result() const - { - return result_; - } + formula* result() const + { + return result_; + } - void - visit(atomic_prop* ap) - { - formula* f = ap->ref(); - if (negated_) - result_ = unop::instance(unop::Not, f); - else - result_ = f; - } + void + visit(atomic_prop* ap) + { + formula* f = ap->ref(); + if (negated_) + result_ = unop::instance(unop::Not, f); + else + result_ = f; + } - void - visit(constant* c) - { - if (!negated_) - { - result_ = c; - return; - } - - switch (c->val()) - { - case constant::True: - result_ = constant::false_instance(); - return; - case constant::False: - result_ = constant::true_instance(); - return; - } - /* Unreachable code. */ - assert(0); - } - - void - visit(unop* uo) - { - formula* f = uo->child(); - switch (uo->op()) - { - case unop::Not: - result_ = recurse_(f, negated_ ^ true); - return; - case unop::X: - /* !Xa == X!a */ - result_ = unop::instance(unop::X, recurse(f)); - return; - case unop::F: - /* !Fa == G!a */ - result_ = unop::instance(negated_ ? unop::G : unop::F, recurse(f)); - return; - case unop::G: - /* !Ga == F!a */ - result_ = unop::instance(negated_ ? unop::F : unop::G, recurse(f)); - return; - } - /* Unreachable code. */ - assert(0); - } - - void - visit(binop* bo) - { - formula* f1 = bo->first(); - formula* f2 = bo->second(); - switch (bo->op()) - { - case binop::Xor: - /* !(a ^ b) == a <=> b */ - result_ = binop::instance(negated_ ? binop::Equiv : binop::Xor, - recurse_(f1, false), - recurse_(f2, false)); - return; - case binop::Equiv: - /* !(a <=> b) == a ^ b */ - result_ = binop::instance(negated_ ? binop::Xor : binop::Equiv, - recurse_(f1, false), - recurse_(f2, false)); - return; - case binop::Implies: - if (negated_) - /* !(a => b) == a & !b */ - result_ = multop::instance(multop::And, - recurse_(f1, false), - recurse_(f2, true)); - else - result_ = binop::instance(binop::Implies, - recurse(f1), recurse(f2)); - return; - case binop::U: - /* !(a U b) == !a R !b */ - result_ = binop::instance(negated_ ? binop::R : binop::U, - recurse(f1), recurse(f2)); - return; - case binop::R: - /* !(a R b) == !a U !b */ - result_ = binop::instance(negated_ ? binop::U : binop::R, - recurse(f1), recurse(f2)); - return; - } - /* Unreachable code. */ - assert(0); - } - - void - visit(multop* mo) - { - /* !(a & b & c) == !a | !b | !c */ - /* !(a | b | c) == !a & !b & !c */ - multop::type op = mo->op(); - if (negated_) - switch (op) + void + visit(constant* c) + { + if (!negated_) { - case multop::And: - op = multop::Or; - break; - case multop::Or: - op = multop::And; - break; + result_ = c; + return; } - multop::vec* res = new multop::vec; - unsigned mos = mo->size(); - for (unsigned i = 0; i < mos; ++i) - res->push_back(recurse(mo->nth(i))); - result_ = multop::instance(op, res); - } - formula* - recurse_(formula* f, bool negated) - { - return negative_normal_form(f, negated); - } + switch (c->val()) + { + case constant::True: + result_ = constant::false_instance(); + return; + case constant::False: + result_ = constant::true_instance(); + return; + } + /* Unreachable code. */ + assert(0); + } - formula* - recurse(formula* f) - { - return recurse_(f, negated_); - } + void + visit(unop* uo) + { + formula* f = uo->child(); + switch (uo->op()) + { + case unop::Not: + result_ = recurse_(f, negated_ ^ true); + return; + case unop::X: + /* !Xa == X!a */ + result_ = unop::instance(unop::X, recurse(f)); + return; + case unop::F: + /* !Fa == G!a */ + result_ = unop::instance(negated_ ? unop::G : unop::F, + recurse(f)); + return; + case unop::G: + /* !Ga == F!a */ + result_ = unop::instance(negated_ ? unop::F : unop::G, + recurse(f)); + return; + } + /* Unreachable code. */ + assert(0); + } - protected: - formula* result_; - bool negated_; - }; + void + visit(binop* bo) + { + formula* f1 = bo->first(); + formula* f2 = bo->second(); + switch (bo->op()) + { + case binop::Xor: + /* !(a ^ b) == a <=> b */ + result_ = binop::instance(negated_ ? binop::Equiv : binop::Xor, + recurse_(f1, false), + recurse_(f2, false)); + return; + case binop::Equiv: + /* !(a <=> b) == a ^ b */ + result_ = binop::instance(negated_ ? binop::Xor : binop::Equiv, + recurse_(f1, false), + recurse_(f2, false)); + return; + case binop::Implies: + if (negated_) + /* !(a => b) == a & !b */ + result_ = multop::instance(multop::And, + recurse_(f1, false), + recurse_(f2, true)); + else + result_ = binop::instance(binop::Implies, + recurse(f1), recurse(f2)); + return; + case binop::U: + /* !(a U b) == !a R !b */ + result_ = binop::instance(negated_ ? binop::R : binop::U, + recurse(f1), recurse(f2)); + return; + case binop::R: + /* !(a R b) == !a U !b */ + result_ = binop::instance(negated_ ? binop::U : binop::R, + recurse(f1), recurse(f2)); + return; + } + /* Unreachable code. */ + assert(0); + } + + void + visit(multop* mo) + { + /* !(a & b & c) == !a | !b | !c */ + /* !(a | b | c) == !a & !b & !c */ + multop::type op = mo->op(); + if (negated_) + switch (op) + { + case multop::And: + op = multop::Or; + break; + case multop::Or: + op = multop::And; + break; + } + multop::vec* res = new multop::vec; + unsigned mos = mo->size(); + for (unsigned i = 0; i < mos; ++i) + res->push_back(recurse(mo->nth(i))); + result_ = multop::instance(op, res); + } + + formula* + recurse_(formula* f, bool negated) + { + return negative_normal_form(f, negated); + } + + formula* + recurse(formula* f) + { + return recurse_(f, negated_); + } + + protected: + formula* result_; + bool negated_; + }; + } formula* negative_normal_form(const formula* f, bool negated) diff --git a/src/ltlvisit/reduce.cc b/src/ltlvisit/reduce.cc index ffbb03332..de9372a25 100644 --- a/src/ltlvisit/reduce.cc +++ b/src/ltlvisit/reduce.cc @@ -34,258 +34,261 @@ namespace spot { namespace ltl { - - class reduce_visitor : public visitor + namespace { - public: - - reduce_visitor(int opt) - : opt_(opt) + class reduce_visitor: public visitor { - } + public: - virtual ~reduce_visitor() - { - } + reduce_visitor(int opt) + : opt_(opt) + { + } - formula* - result() const - { - return result_; - } + virtual ~reduce_visitor() + { + } - void - visit(atomic_prop* ap) - { - formula* f = ap->ref(); - result_ = f; - } + formula* + result() const + { + return result_; + } - void - visit(constant* c) - { - result_ = c; - } + void + visit(atomic_prop* ap) + { + formula* f = ap->ref(); + result_ = f; + } - void - visit(unop* uo) - { - result_ = recurse(uo->child()); + void + visit(constant* c) + { + result_ = c; + } - switch (uo->op()) - { - case unop::Not: - result_ = unop::instance(unop::Not, result_); - return; + void + visit(unop* uo) + { + result_ = recurse(uo->child()); - case unop::X: - result_ = unop::instance(unop::X, result_); - return; + switch (uo->op()) + { + case unop::Not: + result_ = unop::instance(unop::Not, result_); + return; - case unop::F: - /* If f is a pure eventuality formula then F(f)=f. */ - if (!(opt_ & Reduce_Eventuality_And_Universality) - || !is_eventual(result_)) - result_ = unop::instance(unop::F, result_); - return; + case unop::X: + result_ = unop::instance(unop::X, result_); + return; - case unop::G: - /* If f is a pure universality formula then G(f)=f. */ - if (!(opt_ & Reduce_Eventuality_And_Universality) - || !is_universal(result_)) - result_ = unop::instance(unop::G, result_); - return; - } - /* Unreachable code. */ - assert(0); - } + case unop::F: + /* If f is a pure eventuality formula then F(f)=f. */ + if (!(opt_ & Reduce_Eventuality_And_Universality) + || !is_eventual(result_)) + result_ = unop::instance(unop::F, result_); + return; - void - visit(binop* bo) - { - formula* f2 = recurse(bo->second()); + case unop::G: + /* If f is a pure universality formula then G(f)=f. */ + if (!(opt_ & Reduce_Eventuality_And_Universality) + || !is_universal(result_)) + result_ = unop::instance(unop::G, result_); + return; + } + /* Unreachable code. */ + assert(0); + } - /* If b is a pure eventuality formula then a U b = b. - If b is a pure universality formula a R b = b. */ - if ((opt_ & Reduce_Eventuality_And_Universality) - && ((is_eventual(f2) && ((bo->op()) == binop::U)) - || (is_universal(f2) && ((bo->op()) == binop::R)))) - { - result_ = f2; - return; - } - /* case of implies */ - formula* f1 = recurse(bo->first()); + void + visit(binop* bo) + { + formula* f2 = recurse(bo->second()); - if (opt_ & Reduce_Syntactic_Implications) - { - // FIXME: These should be done only when needed. - bool inf = syntactic_implication(f1, f2); - bool infinv = syntactic_implication(f2, f1); - bool infnegleft = syntactic_implication_neg(f2, f1, false); - bool infnegright = syntactic_implication_neg(f2, f1, true); + /* If b is a pure eventuality formula then a U b = b. + If b is a pure universality formula a R b = b. */ + if ((opt_ & Reduce_Eventuality_And_Universality) + && ((is_eventual(f2) && ((bo->op()) == binop::U)) + || (is_universal(f2) && ((bo->op()) == binop::R)))) + { + result_ = f2; + return; + } + /* case of implies */ + formula* f1 = recurse(bo->first()); - switch (bo->op()) - { - case binop::Xor: - case binop::Equiv: - case binop::Implies: - break; + if (opt_ & Reduce_Syntactic_Implications) + { + // FIXME: These should be done only when needed. + bool inf = syntactic_implication(f1, f2); + bool infinv = syntactic_implication(f2, f1); + bool infnegleft = syntactic_implication_neg(f2, f1, false); + bool infnegright = syntactic_implication_neg(f2, f1, true); - case binop::U: - /* a < b => a U b = b */ - if (inf) - { - result_ = f2; - destroy(f1); - return; - } - /* !b < a => a U b = Fb */ - if (infnegleft) - { - result_ = unop::instance(unop::F, f2); - destroy(f1); - return; - } - /* a < b => a U (b U c) = (b U c) */ + switch (bo->op()) { - binop* bo = dynamic_cast(f2); - if (bo && bo->op() == binop::U - && syntactic_implication(f1, bo->first())) + case binop::Xor: + case binop::Equiv: + case binop::Implies: + break; + + case binop::U: + /* a < b => a U b = b */ + if (inf) { result_ = f2; destroy(f1); return; } - } - break; + /* !b < a => a U b = Fb */ + if (infnegleft) + { + result_ = unop::instance(unop::F, f2); + destroy(f1); + return; + } + /* a < b => a U (b U c) = (b U c) */ + { + binop* bo = dynamic_cast(f2); + if (bo && bo->op() == binop::U + && syntactic_implication(f1, bo->first())) + { + result_ = f2; + destroy(f1); + return; + } + } + break; - case binop::R: - /* b < a => a R b = b */ - if (infinv) - { - result_ = f2; - destroy(f1); - return; - } - /* b < !a => a R b = Gb */ - if (infnegright) - { - result_ = unop::instance(unop::G, f2); - destroy(f1); - return; - } - /* b < a => a R (b R c) = b R c */ - { - binop* bo = dynamic_cast(f2); - if (bo && bo->op() == binop::R - && syntactic_implication(bo->first(), f1)) + case binop::R: + /* b < a => a R b = b */ + if (infinv) { result_ = f2; destroy(f1); return; } + /* b < !a => a R b = Gb */ + if (infnegright) + { + result_ = unop::instance(unop::G, f2); + destroy(f1); + return; + } + /* b < a => a R (b R c) = b R c */ + { + binop* bo = dynamic_cast(f2); + if (bo && bo->op() == binop::R + && syntactic_implication(bo->first(), f1)) + { + result_ = f2; + destroy(f1); + return; + } + } + break; } - break; - } - } - result_ = binop::instance(bo->op(), f1, f2); - } + } + result_ = binop::instance(bo->op(), f1, f2); + } - void - visit(multop* mo) - { - unsigned mos = mo->size(); - multop::vec* res = new multop::vec; + void + visit(multop* mo) + { + unsigned mos = mo->size(); + multop::vec* res = new multop::vec; - for (unsigned i = 0; i < mos; ++i) - res->push_back(recurse(mo->nth(i))); + for (unsigned i = 0; i < mos; ++i) + res->push_back(recurse(mo->nth(i))); - if (opt_ & Reduce_Syntactic_Implications) - { + if (opt_ & Reduce_Syntactic_Implications) + { - bool removed = true; - multop::vec::iterator f1; - multop::vec::iterator f2; + bool removed = true; + multop::vec::iterator f1; + multop::vec::iterator f2; - while (removed) - { - removed = false; - f2 = f1 = res->begin(); - ++f1; - while (f1 != res->end()) - { - assert(f1 != f2); - // a < b => a + b = b - // a < b => a & b = a - if ((syntactic_implication(*f1, *f2) && // f1 < f2 - (mo->op() == multop::Or)) || - ((syntactic_implication(*f2, *f1)) && // f2 < f1 - (mo->op() == multop::And))) - { - // We keep f2 - destroy(*f1); - res->erase(f1); - removed = true; - break; - } - else if ((syntactic_implication(*f2, *f1) && // f2 < f1 - (mo->op() == multop::Or)) || - ((syntactic_implication(*f1, *f2)) && // f1 < f2 - (mo->op() == multop::And))) - { - // We keep f1 - destroy(*f2); - res->erase(f2); - removed = true; - break; - } - else - ++f1; - } - } + while (removed) + { + removed = false; + f2 = f1 = res->begin(); + ++f1; + while (f1 != res->end()) + { + assert(f1 != f2); + // a < b => a + b = b + // a < b => a & b = a + if ((syntactic_implication(*f1, *f2) && // f1 < f2 + (mo->op() == multop::Or)) || + ((syntactic_implication(*f2, *f1)) && // f2 < f1 + (mo->op() == multop::And))) + { + // We keep f2 + destroy(*f1); + res->erase(f1); + removed = true; + break; + } + else if ((syntactic_implication(*f2, *f1) && // f2 < f1 + (mo->op() == multop::Or)) || + ((syntactic_implication(*f1, *f2)) && // f1 < f2 + (mo->op() == multop::And))) + { + // We keep f1 + destroy(*f2); + res->erase(f2); + removed = true; + break; + } + else + ++f1; + } + } - // FIXME - /* f1 < !f2 => f1 & f2 = false - !f1 < f2 => f1 | f2 = true */ - for (f1 = res->begin(); f1 != res->end(); f1++) - for (f2 = res->begin(); f2 != res->end(); f2++) - if (f1 != f2 && - syntactic_implication_neg(*f1, *f2, - mo->op() != multop::Or)) - { - for (multop::vec::iterator j = res->begin(); - j != res->end(); j++) - destroy(*j); - res->clear(); - delete res; - if (mo->op() == multop::Or) - result_ = constant::true_instance(); - else - result_ = constant::false_instance(); - return; - } + // FIXME + /* f1 < !f2 => f1 & f2 = false + !f1 < f2 => f1 | f2 = true */ + for (f1 = res->begin(); f1 != res->end(); f1++) + for (f2 = res->begin(); f2 != res->end(); f2++) + if (f1 != f2 && + syntactic_implication_neg(*f1, *f2, + mo->op() != multop::Or)) + { + for (multop::vec::iterator j = res->begin(); + j != res->end(); j++) + destroy(*j); + res->clear(); + delete res; + if (mo->op() == multop::Or) + result_ = constant::true_instance(); + else + result_ = constant::false_instance(); + return; + } - } + } - if (!res->empty()) - { - result_ = multop::instance(mo->op(), res); - return; - } - assert(0); - } + if (!res->empty()) + { + result_ = multop::instance(mo->op(), res); + return; + } + assert(0); + } - formula* - recurse(formula* f) - { - return reduce(f, opt_); - } + formula* + recurse(formula* f) + { + return reduce(f, opt_); + } - protected: - formula* result_; - int opt_; - }; + protected: + formula* result_; + int opt_; + }; + + } // anonymous formula* reduce(const formula* f, int opt) diff --git a/src/ltlvisit/syntimpl.cc b/src/ltlvisit/syntimpl.cc index 58a08b807..9efb99c9a 100644 --- a/src/ltlvisit/syntimpl.cc +++ b/src/ltlvisit/syntimpl.cc @@ -32,135 +32,489 @@ namespace spot { namespace ltl { - - class eventual_universal_visitor : public const_visitor + namespace { - public: - eventual_universal_visitor() - : eventual(false), universal(false) + class eventual_universal_visitor: public const_visitor { - } + public: - virtual - ~eventual_universal_visitor() - { - } + eventual_universal_visitor() + : eventual(false), universal(false) + { + } - bool - is_eventual() const - { - return eventual; - } + virtual + ~eventual_universal_visitor() + { + } - bool - is_universal() const - { - return universal; - } + bool + is_eventual() const + { + return eventual; + } - void - visit(const atomic_prop*) - { - } + bool + is_universal() const + { + return universal; + } - void - visit(const constant*) - { - } + void + visit(const atomic_prop*) + { + } - void - visit(const unop* uo) - { - const formula* f1 = uo->child(); - if (uo->op() == unop::F) - { - eventual = true; - universal = recurse_un(f1); - return; - } - if (uo->op() == unop::G) - { - universal = true; - eventual = recurse_ev(f1); - } - } + void + visit(const constant*) + { + } - void - visit(const binop* bo) - { - const formula* f1 = bo->first(); - const formula* f2 = bo->second(); - switch (bo->op()) - { - case binop::Xor: - case binop::Equiv: - case binop::Implies: - universal = recurse_un(f1) & recurse_un(f2); - eventual = recurse_ev(f1) & recurse_ev(f2); - return; - case binop::U: - universal = recurse_un(f1) & recurse_un(f2); - if ((f1 == constant::true_instance()) || - (recurse_ev(f1))) + void + visit(const unop* uo) + { + const formula* f1 = uo->child(); + if (uo->op() == unop::F) + { eventual = true; - return; - case binop::R: - eventual = recurse_ev(f1) & recurse_ev(f2); - if ((f1 == constant::false_instance())) - //|| - //(recurse_un(f1))) + universal = recurse_un(f1); + return; + } + if (uo->op() == unop::G) + { universal = true; - if (!universal) + eventual = recurse_ev(f1); + } + } + + void + visit(const binop* bo) + { + const formula* f1 = bo->first(); + const formula* f2 = bo->second(); + switch (bo->op()) + { + case binop::Xor: + case binop::Equiv: + case binop::Implies: universal = recurse_un(f1) & recurse_un(f2); - return; - } - /* Unreachable code. */ - assert(0); - } + eventual = recurse_ev(f1) & recurse_ev(f2); + return; + case binop::U: + universal = recurse_un(f1) & recurse_un(f2); + if ((f1 == constant::true_instance()) || + (recurse_ev(f1))) + eventual = true; + return; + case binop::R: + eventual = recurse_ev(f1) & recurse_ev(f2); + if ((f1 == constant::false_instance())) + //|| + //(recurse_un(f1))) + universal = true; + if (!universal) + universal = recurse_un(f1) & recurse_un(f2); + return; + } + /* Unreachable code. */ + assert(0); + } - void - visit(const multop* mo) + void + visit(const multop* mo) + { + unsigned mos = mo->size(); + + eventual = true; + universal = true; + for (unsigned i = 0; i < mos; ++i) + if (!recurse_ev(mo->nth(i))) + { + eventual = false; + break; + } + for (unsigned i = 0; i < mos; ++i) + if (!recurse_un(mo->nth(i))) + { + universal = false; + break; + } + } + + bool + recurse_ev(const formula* f) + { + eventual_universal_visitor v; + const_cast(f)->accept(v); + return v.is_eventual(); + } + + bool + recurse_un(const formula* f) + { + eventual_universal_visitor v; + const_cast(f)->accept(v); + return v.is_universal(); + } + + protected: + bool eventual; + bool universal; + }; + + + ///////////////////////////////////////////////////////////////////////// + + + class inf_right_recurse_visitor: public const_visitor { - unsigned mos = mo->size(); + public: - eventual = true; - universal = true; - for (unsigned i = 0; i < mos; ++i) - if (!recurse_ev(mo->nth(i))) + inf_right_recurse_visitor(const formula *f) + : result_(false), f(f) + { + } + + virtual + ~inf_right_recurse_visitor() + { + } + + int + result() const + { + return result_; + } + + void + visit(const atomic_prop* ap) + { + if (dynamic_cast(f) == ap) + result_ = true; + } + + void + visit(const constant* c) + { + switch (c->val()) { - eventual = false; + case constant::True: + result_ = true; + return; + case constant::False: + result_ = false; + return; + } + } + + void + visit(const unop* uo) + { + const formula* f1 = uo->child(); + switch (uo->op()) + { + case unop::Not: + if (uo == f) + result_ = true; + return; + case unop::X: + { + const unop* op = dynamic_cast(f); + if (op && op->op() == unop::X) + result_ = syntactic_implication(op->child(), f1); + } + return; + case unop::F: + /* F(a) = true U a */ + result_ = syntactic_implication(f, f1); + return; + case unop::G: + /* G(a) = false R a */ + if (syntactic_implication(f, constant::false_instance())) + result_ = true; + return; + } + /* Unreachable code. */ + assert(0); + } + + void + visit(const binop* bo) + { + const formula* f1 = bo->first(); + const formula* f2 = bo->second(); + const binop* fb = dynamic_cast(f); + const unop* fu = dynamic_cast(f); + switch (bo->op()) + { + case binop::Xor: + case binop::Equiv: + case binop::Implies: + return; + case binop::U: + if (syntactic_implication(f, f2)) + result_ = true; + return; + case binop::R: + if (fb && fb->op() == binop::R) + if (syntactic_implication(fb->first(), f1) && + syntactic_implication(fb->second(), f2)) + { + result_ = true; + return; + } + if (fu && fu->op() == unop::G) + if (f1 == constant::false_instance() && + syntactic_implication(fu->child(), f2)) + { + result_ = true; + return; + } + if (syntactic_implication(f, f1) + && syntactic_implication(f, f2)) + result_ = true; + return; + } + /* Unreachable code. */ + assert(0); + } + + void + visit(const multop* mo) + { + multop::type op = mo->op(); + unsigned mos = mo->size(); + switch (op) + { + case multop::And: + for (unsigned i = 0; i < mos; ++i) + if (!syntactic_implication(f, mo->nth(i))) + return; + result_ = true; + break; + case multop::Or: + for (unsigned i = 0; i < mos && !result_; ++i) + if (syntactic_implication(f, mo->nth(i))) + result_ = true; break; } - for (unsigned i = 0; i < mos; ++i) - if (!recurse_un(mo->nth(i))) + } + + bool + recurse(const formula* f1, const formula* f2) + { + if (f1 == f2) + return true; + inf_right_recurse_visitor v(f2); + const_cast(f1)->accept(v); + return v.result(); + } + + protected: + bool result_; /* true if f < f1, false otherwise. */ + const formula* f; + }; + + ///////////////////////////////////////////////////////////////////////// + + class inf_left_recurse_visitor: public const_visitor + { + public: + + inf_left_recurse_visitor(const formula *f) + : result_(false), f(f) + { + } + + virtual + ~inf_left_recurse_visitor() + { + } + + bool + special_case(const formula* f2) + { + const binop* fb = dynamic_cast(f); + const binop* f2b = dynamic_cast(f2); + if (fb && f2b && fb->op() == f2b->op() + && syntactic_implication(f2b->first(), fb->first()) + && syntactic_implication(f2b->second(), fb->second())) + return true; + return false; + } + + int + result() const + { + return result_; + } + + void + visit(const atomic_prop* ap) + { + inf_right_recurse_visitor v(ap); + const_cast(f)->accept(v); + result_ = v.result(); + } + + void + visit(const constant* c) + { + inf_right_recurse_visitor v(c); + switch (c->val()) { - universal = false; + case constant::True: + const_cast(f)->accept(v); + result_ = v.result(); + return; + case constant::False: + result_ = true; + return; + } + /* Unreachable code. */ + assert(0); + } + + void + visit(const unop* uo) + { + const formula* f1 = uo->child(); + inf_right_recurse_visitor v(uo); + switch (uo->op()) + { + case unop::Not: + if (uo == f) + result_ = true; + return; + case unop::X: + { + const unop* op = dynamic_cast(f); + if (op && op->op() == unop::X) + result_ = syntactic_implication(f1, op->child()); + } + return; + case unop::F: + { + /* F(a) = true U a */ + const formula* tmp = binop::instance(binop::U, + constant::true_instance(), + clone(f1)); + if (special_case(tmp)) + { + result_ = true; + destroy(tmp); + return; + } + if (syntactic_implication(tmp, f)) + result_ = true; + destroy(tmp); + return; + } + case unop::G: + { + /* G(a) = false R a */ + const formula* tmp = binop::instance(binop::R, + constant::false_instance(), + clone(f1)); + if (special_case(tmp)) + { + result_ = true; + destroy(tmp); + return; + } + if (syntactic_implication(tmp, f)) + result_ = true; + destroy(tmp); + return; + } + } + /* Unreachable code. */ + assert(0); + } + + void + visit(const binop* bo) + { + if (special_case(bo)) + { + result_ = true; + return; + } + + const formula* f1 = bo->first(); + const formula* f2 = bo->second(); + const binop* fb = dynamic_cast(f); + const unop* fu = dynamic_cast(f); + switch (bo->op()) + { + case binop::Xor: + case binop::Equiv: + case binop::Implies: + return; + case binop::U: + /* (a < c) && (c < d) => a U b < c U d */ + if (fb && fb->op() == binop::U) + if (syntactic_implication(f1, fb->first()) && + syntactic_implication(f2, fb->second())) + { + result_ = true; + return; + } + if (fu && fu->op() == unop::F) + if (f1 == constant::true_instance() && + syntactic_implication(f2, fu->child())) + { + result_ = true; + return; + } + if (syntactic_implication(f1, f) + && syntactic_implication(f2, f)) + result_ = true; + return; + case binop::R: + if (fu && fu->op() == unop::G) + if (f1 == constant::false_instance() && + syntactic_implication(f2, fu->child())) + { + result_ = true; + return; + } + if (syntactic_implication(f2, f)) + result_ = true; + return; + } + /* Unreachable code. */ + assert(0); + } + + void + visit(const multop* mo) + { + multop::type op = mo->op(); + unsigned mos = mo->size(); + switch (op) + { + case multop::And: + for (unsigned i = 0; (i < mos) && !result_; ++i) + if (syntactic_implication(mo->nth(i), f)) + result_ = true; + break; + case multop::Or: + for (unsigned i = 0; i < mos; ++i) + if (!syntactic_implication(mo->nth(i), f)) + return; + result_ = true; break; } - } + } - bool - recurse_ev(const formula* f) - { - eventual_universal_visitor v; - const_cast(f)->accept(v); - return v.is_eventual(); - } - - bool - recurse_un(const formula* f) - { - eventual_universal_visitor v; - const_cast(f)->accept(v); - return v.is_universal(); - } - - protected: - bool eventual; - bool universal; - }; + protected: + bool result_; /* true if f1 < f, 1 otherwise. */ + const formula* f; + }; + } // anonymous bool is_eventual(const formula* f) @@ -178,356 +532,6 @@ namespace spot return v.is_universal(); } - ///////////////////////////////////////////////////////////////////////// - - - class inf_right_recurse_visitor : public const_visitor - { - public: - - inf_right_recurse_visitor(const formula *f) - : result_(false), f(f) - { - } - - virtual - ~inf_right_recurse_visitor() - { - } - - int - result() const - { - return result_; - } - - void - visit(const atomic_prop* ap) - { - if (dynamic_cast(f) == ap) - result_ = true; - } - - void - visit(const constant* c) - { - switch (c->val()) - { - case constant::True: - result_ = true; - return; - case constant::False: - result_ = false; - return; - } - } - - void - visit(const unop* uo) - { - const formula* f1 = uo->child(); - switch (uo->op()) - { - case unop::Not: - if (uo == f) - result_ = true; - return; - case unop::X: - { - const unop* op = dynamic_cast(f); - if (op && op->op() == unop::X) - result_ = syntactic_implication(op->child(), f1); - } - return; - case unop::F: - /* F(a) = true U a */ - result_ = syntactic_implication(f, f1); - return; - case unop::G: - /* G(a) = false R a */ - if (syntactic_implication(f, constant::false_instance())) - result_ = true; - return; - } - /* Unreachable code. */ - assert(0); - } - - void - visit(const binop* bo) - { - const formula* f1 = bo->first(); - const formula* f2 = bo->second(); - const binop* fb = dynamic_cast(f); - const unop* fu = dynamic_cast(f); - switch (bo->op()) - { - case binop::Xor: - case binop::Equiv: - case binop::Implies: - return; - case binop::U: - if (syntactic_implication(f, f2)) - result_ = true; - return; - case binop::R: - if (fb && fb->op() == binop::R) - if (syntactic_implication(fb->first(), f1) && - syntactic_implication(fb->second(), f2)) - { - result_ = true; - return; - } - if (fu && fu->op() == unop::G) - if (f1 == constant::false_instance() && - syntactic_implication(fu->child(), f2)) - { - result_ = true; - return; - } - if (syntactic_implication(f, f1) - && syntactic_implication(f, f2)) - result_ = true; - return; - } - /* Unreachable code. */ - assert(0); - } - - void - visit(const multop* mo) - { - multop::type op = mo->op(); - unsigned mos = mo->size(); - switch (op) - { - case multop::And: - for (unsigned i = 0; i < mos; ++i) - if (!syntactic_implication(f, mo->nth(i))) - return; - result_ = true; - break; - case multop::Or: - for (unsigned i = 0; i < mos && !result_; ++i) - if (syntactic_implication(f, mo->nth(i))) - result_ = true; - break; - } - } - - bool - recurse(const formula* f1, const formula* f2) - { - if (f1 == f2) - return true; - inf_right_recurse_visitor v(f2); - const_cast(f1)->accept(v); - return v.result(); - } - - protected: - bool result_; /* true if f < f1, false otherwise. */ - const formula* f; - }; - - ///////////////////////////////////////////////////////////////////////// - - class inf_left_recurse_visitor : public const_visitor - { - public: - - inf_left_recurse_visitor(const formula *f) - : result_(false), f(f) - { - } - - virtual - ~inf_left_recurse_visitor() - { - } - - bool - special_case(const formula* f2) - { - const binop* fb = dynamic_cast(f); - const binop* f2b = dynamic_cast(f2); - if (fb && f2b && fb->op() == f2b->op() - && syntactic_implication(f2b->first(), fb->first()) - && syntactic_implication(f2b->second(), fb->second())) - return true; - return false; - } - - int - result() const - { - return result_; - } - - void - visit(const atomic_prop* ap) - { - inf_right_recurse_visitor v(ap); - const_cast(f)->accept(v); - result_ = v.result(); - } - - void - visit(const constant* c) - { - inf_right_recurse_visitor v(c); - switch (c->val()) - { - case constant::True: - const_cast(f)->accept(v); - result_ = v.result(); - return; - case constant::False: - result_ = true; - return; - } - /* Unreachable code. */ - assert(0); - } - - void - visit(const unop* uo) - { - const formula* f1 = uo->child(); - inf_right_recurse_visitor v(uo); - switch (uo->op()) - { - case unop::Not: - if (uo == f) - result_ = true; - return; - case unop::X: - { - const unop* op = dynamic_cast(f); - if (op && op->op() == unop::X) - result_ = syntactic_implication(f1, op->child()); - } - return; - case unop::F: - { - /* F(a) = true U a */ - const formula* tmp = binop::instance(binop::U, - constant::true_instance(), - clone(f1)); - if (special_case(tmp)) - { - result_ = true; - destroy(tmp); - return; - } - if (syntactic_implication(tmp, f)) - result_ = true; - destroy(tmp); - return; - } - case unop::G: - { - /* G(a) = false R a */ - const formula* tmp = binop::instance(binop::R, - constant::false_instance(), - clone(f1)); - if (special_case(tmp)) - { - result_ = true; - destroy(tmp); - return; - } - if (syntactic_implication(tmp, f)) - result_ = true; - destroy(tmp); - return; - } - } - /* Unreachable code. */ - assert(0); - } - - void - visit(const binop* bo) - { - if (special_case(bo)) - { - result_ = true; - return; - } - - const formula* f1 = bo->first(); - const formula* f2 = bo->second(); - const binop* fb = dynamic_cast(f); - const unop* fu = dynamic_cast(f); - switch (bo->op()) - { - case binop::Xor: - case binop::Equiv: - case binop::Implies: - return; - case binop::U: - /* (a < c) && (c < d) => a U b < c U d */ - if (fb && fb->op() == binop::U) - if (syntactic_implication(f1, fb->first()) && - syntactic_implication(f2, fb->second())) - { - result_ = true; - return; - } - if (fu && fu->op() == unop::F) - if (f1 == constant::true_instance() && - syntactic_implication(f2, fu->child())) - { - result_ = true; - return; - } - if (syntactic_implication(f1, f) - && syntactic_implication(f2, f)) - result_ = true; - return; - case binop::R: - if (fu && fu->op() == unop::G) - if (f1 == constant::false_instance() && - syntactic_implication(f2, fu->child())) - { - result_ = true; - return; - } - if (syntactic_implication(f2, f)) - result_ = true; - return; - } - /* Unreachable code. */ - assert(0); - } - - void - visit(const multop* mo) - { - multop::type op = mo->op(); - unsigned mos = mo->size(); - switch (op) - { - case multop::And: - for (unsigned i = 0; (i < mos) && !result_; ++i) - if (syntactic_implication(mo->nth(i), f)) - result_ = true; - break; - case multop::Or: - for (unsigned i = 0; i < mos; ++i) - if (!syntactic_implication(mo->nth(i), f)) - return; - result_ = true; - break; - } - } - - protected: - bool result_; /* true if f1 < f, 1 otherwise. */ - const formula* f; - }; - // This is called by syntactic_implication() after the // formulae have been normalized. bool diff --git a/src/ltlvisit/tostring.cc b/src/ltlvisit/tostring.cc index d7dfaafc9..732d269d2 100644 --- a/src/ltlvisit/tostring.cc +++ b/src/ltlvisit/tostring.cc @@ -32,159 +32,161 @@ namespace spot { namespace ltl { - - static bool - is_bare_word(const char* str) + namespace { - // Bare words cannot be empty, start with the letter of a unary - // operator, or be the name of an existing constant. Also they - // should start with an letter. - if (!*str - || *str == 'F' - || *str == 'G' - || *str == 'X' - || !(isalpha(*str) || *str == '_') - || !strcasecmp(str, "true") - || !strcasecmp(str, "false")) - return false; - // The remaining of the word must be alphanumeric. - while (*++str) - if (!(isalnum(*str) || *str == '_')) + static bool + is_bare_word(const char* str) + { + // Bare words cannot be empty, start with the letter of a unary + // operator, or be the name of an existing constant. Also they + // should start with an letter. + if (!*str + || *str == 'F' + || *str == 'G' + || *str == 'X' + || !(isalpha(*str) || *str == '_') + || !strcasecmp(str, "true") + || !strcasecmp(str, "false")) return false; - return true; + // The remaining of the word must be alphanumeric. + while (*++str) + if (!(isalnum(*str) || *str == '_')) + return false; + return true; + } + + class to_string_visitor: public const_visitor + { + public: + to_string_visitor(std::ostream& os) + : os_(os), top_level_(true) + { + } + + virtual + ~to_string_visitor() + { + } + + void + visit(const atomic_prop* ap) + { + std::string str = ap->name(); + if (!is_bare_word(str.c_str())) + { + os_ << '"' << str << '"'; + } + else + { + os_ << str; + } + } + + void + visit(const constant* c) + { + os_ << c->val_name(); + } + + void + visit(const binop* bo) + { + bool top_level = top_level_; + top_level_ = false; + if (!top_level) + os_ << "("; + + bo->first()->accept(*this); + + switch (bo->op()) + { + case binop::Xor: + os_ << " ^ "; + break; + case binop::Implies: + os_ << " => "; + break; + case binop::Equiv: + os_ << " <=> "; + break; + case binop::U: + os_ << " U "; + break; + case binop::R: + os_ << " R "; + break; + } + + bo->second()->accept(*this); + if (!top_level) + os_ << ")"; + } + + void + visit(const unop* uo) + { + // The parser treats F0, F1, G0, G1, X0, and X1 as atomic + // propositions. So make sure we output F(0), G(1), etc. + bool need_parent = !!dynamic_cast(uo->child()); + switch (uo->op()) + { + case unop::Not: + os_ << "!"; + need_parent = false; + break; + case unop::X: + os_ << "X"; + break; + case unop::F: + os_ << "F"; + break; + case unop::G: + os_ << "G"; + break; + } + + top_level_ = false; + if (need_parent) + os_ << "("; + uo->child()->accept(*this); + if (need_parent) + os_ << ")"; + } + + void + visit(const multop* mo) + { + bool top_level = top_level_; + top_level_ = false; + if (!top_level) + os_ << "("; + unsigned max = mo->size(); + mo->nth(0)->accept(*this); + const char* ch = " "; + switch (mo->op()) + { + case multop::Or: + ch = " | "; + break; + case multop::And: + ch = " & "; + break; + } + + for (unsigned n = 1; n < max; ++n) + { + os_ << ch; + mo->nth(n)->accept(*this); + } + if (!top_level) + os_ << ")"; + } + protected: + std::ostream& os_; + bool top_level_; + }; } - class to_string_visitor : public const_visitor - { - public: - to_string_visitor(std::ostream& os) - : os_(os), top_level_(true) - { - } - - virtual - ~to_string_visitor() - { - } - - void - visit(const atomic_prop* ap) - { - std::string str = ap->name(); - if (!is_bare_word(str.c_str())) - { - os_ << '"' << str << '"'; - } - else - { - os_ << str; - } - } - - void - visit(const constant* c) - { - os_ << c->val_name(); - } - - void - visit(const binop* bo) - { - bool top_level = top_level_; - top_level_ = false; - if (!top_level) - os_ << "("; - - bo->first()->accept(*this); - - switch (bo->op()) - { - case binop::Xor: - os_ << " ^ "; - break; - case binop::Implies: - os_ << " => "; - break; - case binop::Equiv: - os_ << " <=> "; - break; - case binop::U: - os_ << " U "; - break; - case binop::R: - os_ << " R "; - break; - } - - bo->second()->accept(*this); - if (!top_level) - os_ << ")"; - } - - void - visit(const unop* uo) - { - // The parser treats F0, F1, G0, G1, X0, and X1 as atomic - // propositions. So make sure we output F(0), G(1), etc. - bool need_parent = !!dynamic_cast(uo->child()); - switch (uo->op()) - { - case unop::Not: - os_ << "!"; - need_parent = false; - break; - case unop::X: - os_ << "X"; - break; - case unop::F: - os_ << "F"; - break; - case unop::G: - os_ << "G"; - break; - } - - top_level_ = false; - if (need_parent) - os_ << "("; - uo->child()->accept(*this); - if (need_parent) - os_ << ")"; - } - - void - visit(const multop* mo) - { - bool top_level = top_level_; - top_level_ = false; - if (!top_level) - os_ << "("; - unsigned max = mo->size(); - mo->nth(0)->accept(*this); - const char* ch = " "; - switch (mo->op()) - { - case multop::Or: - ch = " | "; - break; - case multop::And: - ch = " & "; - break; - } - - for (unsigned n = 1; n < max; ++n) - { - os_ << ch; - mo->nth(n)->accept(*this); - } - if (!top_level) - os_ << ")"; - } - protected: - std::ostream& os_; - bool top_level_; - }; - std::ostream& to_string(const formula* f, std::ostream& os) { diff --git a/src/sanity/style.test b/src/sanity/style.test index 50fd31083..e89d56647 100755 --- a/src/sanity/style.test +++ b/src/sanity/style.test @@ -72,6 +72,12 @@ for dir in "${INCDIR-..}" "${INCDIR-..}"/../iface; do grep '[ ]switch (.*).*{' $tmp && diag 'Opening { should be on its own line.' + grep 'namespace .*{' $tmp && + diag 'Opening { should be on its own line.' + + grep 'class .*{' $tmp && + diag 'Opening { should be on its own line.' + grep '( ' $tmp && diag 'No space after opening (.' @@ -137,6 +143,15 @@ for dir in "${INCDIR-..}" "${INCDIR-..}"/../iface; do diag 'Avoid in headers, better use .' fi ;; + *.cc) + if grep 'namespace$' $tmp >/dev/null; then + : + else + # We only check classes, but the rule should apply to functions too + grep '^[ ]*class[ ]' $tmp && + diag 'Private definitions must be in anonymous namespace.' + fi + ;; esac diff --git a/src/tgba/formula2bdd.cc b/src/tgba/formula2bdd.cc index 062d4c8a9..edc42922e 100644 --- a/src/tgba/formula2bdd.cc +++ b/src/tgba/formula2bdd.cc @@ -1,4 +1,4 @@ -// Copyright (C) 2003 Laboratoire d'Informatique de Paris 6 (LIP6), +// 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. // @@ -30,125 +30,161 @@ namespace spot { using namespace ltl; - class formula_to_bdd_visitor : public ltl::const_visitor + namespace { - public: - formula_to_bdd_visitor(bdd_dict* d, void* owner) - : d_(d), owner_(owner) + class formula_to_bdd_visitor: public ltl::const_visitor { - } + public: + formula_to_bdd_visitor(bdd_dict* d, void* owner) + : d_(d), owner_(owner) + { + } - virtual - ~formula_to_bdd_visitor() - { - } + virtual + ~formula_to_bdd_visitor() + { + } - virtual void - visit(const atomic_prop* node) - { - res_ = bdd_ithvar(d_->register_proposition(node, owner_)); - } + virtual void + visit(const atomic_prop* node) + { + res_ = bdd_ithvar(d_->register_proposition(node, owner_)); + } - virtual void - visit(const constant* node) - { - switch (node->val()) - { - case constant::True: - res_ = bddtrue; - return; - case constant::False: - res_ = bddfalse; - return; - } - /* Unreachable code. */ - assert(0); - } - - virtual void - visit(const unop* node) - { - switch (node->op()) - { - case unop::F: - case unop::G: - case unop::X: - assert(!"unsupported operator"); - case unop::Not: + virtual void + visit(const constant* node) + { + switch (node->val()) { - res_ = bdd_not(recurse(node->child())); + case constant::True: + res_ = bddtrue; + return; + case constant::False: + res_ = bddfalse; return; } - } - /* Unreachable code. */ - assert(0); - } + /* Unreachable code. */ + assert(0); + } - virtual void - visit(const binop* node) + virtual void + visit(const unop* node) + { + switch (node->op()) + { + case unop::F: + case unop::G: + case unop::X: + assert(!"unsupported operator"); + case unop::Not: + { + res_ = bdd_not(recurse(node->child())); + return; + } + } + /* Unreachable code. */ + assert(0); + } + + virtual void + visit(const binop* node) + { + bdd f1 = recurse(node->first()); + bdd f2 = recurse(node->second()); + + switch (node->op()) + { + case binop::Xor: + res_ = bdd_apply(f1, f2, bddop_xor); + return; + case binop::Implies: + res_ = bdd_apply(f1, f2, bddop_imp); + return; + case binop::Equiv: + res_ = bdd_apply(f1, f2, bddop_biimp); + return; + case binop::U: + case binop::R: + assert(!"unsupported operator"); + } + /* Unreachable code. */ + assert(0); + } + + virtual void + visit(const multop* node) + { + int op = -1; + switch (node->op()) + { + case multop::And: + op = bddop_and; + res_ = bddtrue; + break; + case multop::Or: + op = bddop_or; + res_ = bddfalse; + break; + } + assert(op != -1); + unsigned s = node->size(); + for (unsigned n = 0; n < s; ++n) + { + res_ = bdd_apply(res_, recurse(node->nth(n)), op); + } + } + + bdd + result() const + { + return res_; + } + + bdd + recurse(const formula* f) const + { + return formula_to_bdd(f, d_, owner_); + } + + private: + bdd_dict* d_; + void* owner_; + bdd res_; + }; + + // Convert a BDD which is known to be a conjonction into a formula. + static ltl::formula* + conj_to_formula(bdd b, const bdd_dict* d) { - bdd f1 = recurse(node->first()); - bdd f2 = recurse(node->second()); - - switch (node->op()) + if (b == bddfalse) + return constant::false_instance(); + multop::vec* v = new multop::vec; + while (b != bddtrue) { - case binop::Xor: - res_ = bdd_apply(f1, f2, bddop_xor); - return; - case binop::Implies: - res_ = bdd_apply(f1, f2, bddop_imp); - return; - case binop::Equiv: - res_ = bdd_apply(f1, f2, bddop_biimp); - return; - case binop::U: - case binop::R: - assert(!"unsupported operator"); + int var = bdd_var(b); + bdd_dict::vf_map::const_iterator isi = d->var_formula_map.find(var); + assert(isi != d->var_formula_map.end()); + formula* res = clone(isi->second); + + bdd high = bdd_high(b); + if (high == bddfalse) + { + res = unop::instance(unop::Not, res); + b = bdd_low(b); + } + else + { + // If bdd_low is not false, then b was not a conjunction. + assert(bdd_low(b) == bddfalse); + b = high; + } + assert(b != bddfalse); + v->push_back(res); } - /* Unreachable code. */ - assert(0); + return multop::instance(multop::And, v); } - virtual void - visit(const multop* node) - { - int op = -1; - switch (node->op()) - { - case multop::And: - op = bddop_and; - res_ = bddtrue; - break; - case multop::Or: - op = bddop_or; - res_ = bddfalse; - break; - } - assert(op != -1); - unsigned s = node->size(); - for (unsigned n = 0; n < s; ++n) - { - res_ = bdd_apply(res_, recurse(node->nth(n)), op); - } - } - - bdd - result() const - { - return res_; - } - - bdd - recurse(const formula* f) const - { - return formula_to_bdd(f, d_, owner_); - } - - private: - bdd_dict* d_; - void* owner_; - bdd res_; - }; + } // anonymous bdd formula_to_bdd(const formula* f, bdd_dict* d, void* for_me) @@ -158,38 +194,6 @@ namespace spot return v.result(); } - // Convert a BDD which is known to be a conjonction into a formula. - static ltl::formula* - conj_to_formula(bdd b, const bdd_dict* d) - { - if (b == bddfalse) - return constant::false_instance(); - multop::vec* v = new multop::vec; - while (b != bddtrue) - { - int var = bdd_var(b); - bdd_dict::vf_map::const_iterator isi = d->var_formula_map.find(var); - assert(isi != d->var_formula_map.end()); - formula* res = clone(isi->second); - - bdd high = bdd_high(b); - if (high == bddfalse) - { - res = unop::instance(unop::Not, res); - b = bdd_low(b); - } - else - { - // If bdd_low is not false, then b was not a conjunction. - assert(bdd_low(b) == bddfalse); - b = high; - } - assert(b != bddfalse); - v->push_back(res); - } - return multop::instance(multop::And, v); - } - const formula* bdd_to_formula(bdd f, const bdd_dict* d) { diff --git a/src/tgba/tgbabddconcreteproduct.cc b/src/tgba/tgbabddconcreteproduct.cc index de4ba1aeb..8cffb3d81 100644 --- a/src/tgba/tgbabddconcreteproduct.cc +++ b/src/tgba/tgbabddconcreteproduct.cc @@ -1,4 +1,4 @@ -// Copyright (C) 2003 Laboratoire d'Informatique de Paris 6 (LIP6), +// 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. // @@ -24,55 +24,58 @@ namespace spot { - /// \brief Helper class for product(). - /// - /// As both automata are encoded using BDD, we just have - /// to homogenize the variable numbers before ANDing the - /// relations and initial states. - class tgba_bdd_product_factory: public tgba_bdd_factory + namespace { - public: - tgba_bdd_product_factory(const tgba_bdd_concrete* left, - const tgba_bdd_concrete* right) - : dict_(left->get_dict()), - left_(left), - right_(right), - data_(left_->get_core_data(), right_->get_core_data()), - init_(left_->get_init_bdd() & right_->get_init_bdd()) + /// \brief Helper class for product(). + /// + /// As both automata are encoded using BDD, we just have + /// to homogenize the variable numbers before ANDing the + /// relations and initial states. + class tgba_bdd_product_factory: public tgba_bdd_factory { - assert(dict_ == right->get_dict()); - } + public: + tgba_bdd_product_factory(const tgba_bdd_concrete* left, + const tgba_bdd_concrete* right) + : dict_(left->get_dict()), + left_(left), + right_(right), + data_(left_->get_core_data(), right_->get_core_data()), + init_(left_->get_init_bdd() & right_->get_init_bdd()) + { + assert(dict_ == right->get_dict()); + } - virtual - ~tgba_bdd_product_factory() - { - } + virtual + ~tgba_bdd_product_factory() + { + } - const tgba_bdd_core_data& - get_core_data() const - { - return data_; - } + const tgba_bdd_core_data& + get_core_data() const + { + return data_; + } - bdd_dict* - get_dict() const - { - return dict_; - } + bdd_dict* + get_dict() const + { + return dict_; + } - bdd - get_init_state() const - { - return init_; - } + bdd + get_init_state() const + { + return init_; + } - private: - bdd_dict* dict_; - const tgba_bdd_concrete* left_; - const tgba_bdd_concrete* right_; - tgba_bdd_core_data data_; - bdd init_; - }; + private: + bdd_dict* dict_; + const tgba_bdd_concrete* left_; + const tgba_bdd_concrete* right_; + tgba_bdd_core_data data_; + bdd init_; + }; + } tgba_bdd_concrete* product(const tgba_bdd_concrete* left, const tgba_bdd_concrete* right) diff --git a/src/tgba/tgbareduc.hh b/src/tgba/tgbareduc.hh index 29b6b557a..e27f424db 100644 --- a/src/tgba/tgbareduc.hh +++ b/src/tgba/tgbareduc.hh @@ -39,8 +39,12 @@ namespace spot typedef Sgi::vector delayed_simulation_relation; */ - class direct_simulation_relation : public simulation_relation{}; - class delayed_simulation_relation : public simulation_relation{}; + class direct_simulation_relation: public simulation_relation + { + }; + class delayed_simulation_relation: public simulation_relation + { + }; class tgba_reduc: public tgba_explicit, diff --git a/src/tgba/tgbatba.cc b/src/tgba/tgbatba.cc index 2e638da05..7d92fa93c 100644 --- a/src/tgba/tgbatba.cc +++ b/src/tgba/tgbatba.cc @@ -26,171 +26,174 @@ namespace spot { - - /// \brief A state for spot::tgba_tba_proxy. - /// - /// This state is in fact a pair of state: the state from the tgba - /// automaton, and a state of the "counter" (we use a pointer - /// to the position in the cycle_acc_ list). - class state_tba_proxy : public state + namespace { - typedef tgba_tba_proxy::cycle_list::const_iterator iterator; - public: - state_tba_proxy(state* s, iterator acc) - : s_(s), acc_(acc) + /// \brief A state for spot::tgba_tba_proxy. + /// + /// This state is in fact a pair of state: the state from the tgba + /// automaton, and a state of the "counter" (we use a pointer + /// to the position in the cycle_acc_ list). + class state_tba_proxy: public state { - } + typedef tgba_tba_proxy::cycle_list::const_iterator iterator; + public: + state_tba_proxy(state* s, iterator acc) + : s_(s), acc_(acc) + { + } - /// Copy constructor - state_tba_proxy(const state_tba_proxy& o) - : state(), - s_(o.real_state()->clone()), - acc_(o.acceptance_iterator()) + /// Copy constructor + state_tba_proxy(const state_tba_proxy& o) + : state(), + s_(o.real_state()->clone()), + acc_(o.acceptance_iterator()) + { + } + + virtual + ~state_tba_proxy() + { + delete s_; + } + + state* + real_state() const + { + return s_; + } + + bdd + acceptance_cond() const + { + return *acc_; + } + + iterator + acceptance_iterator() const + { + return acc_; + } + + virtual int + compare(const state* other) const + { + const state_tba_proxy* o = dynamic_cast(other); + assert(o); + int res = s_->compare(o->real_state()); + if (res != 0) + return res; + return acc_->id() - o->acceptance_cond().id(); + } + + virtual size_t + hash() const + { + // We expect to have many more states than acceptance conditions. + // Hence we keep only 8 bits for acceptance conditions. + return (s_->hash() << 8) + (acc_->id() & 0xFF); + } + + virtual + state_tba_proxy* clone() const + { + return new state_tba_proxy(*this); + } + + private: + state* s_; + iterator acc_; + }; + + + /// \brief Iterate over the successors of tgba_tba_proxy computed + /// on the fly. + class tgba_tba_proxy_succ_iterator: public tgba_succ_iterator { - } + typedef tgba_tba_proxy::cycle_list list; + typedef tgba_tba_proxy::cycle_list::const_iterator iterator; + public: + tgba_tba_proxy_succ_iterator(tgba_succ_iterator* it, + iterator expected, iterator end, + bdd the_acceptance_cond) + : it_(it), expected_(expected), end_(end), + the_acceptance_cond_(the_acceptance_cond) + { + } - virtual - ~state_tba_proxy() - { - delete s_; - } + virtual + ~tgba_tba_proxy_succ_iterator() + { + delete it_; + } - state* - real_state() const - { - return s_; - } + // iteration - bdd - acceptance_cond() const - { - return *acc_; - } + void + first() + { + it_->first(); + } - iterator - acceptance_iterator() const - { - return acc_; - } + void + next() + { + it_->next(); + } - virtual int - compare(const state* other) const - { - const state_tba_proxy* o = dynamic_cast(other); - assert(o); - int res = s_->compare(o->real_state()); - if (res != 0) - return res; - return acc_->id() - o->acceptance_cond().id(); - } + bool + done() const + { + return it_->done(); + } - virtual size_t - hash() const - { - // We expect to have many more states than acceptance conditions. - // Hence we keep only 8 bits for acceptance conditions. - return (s_->hash() << 8) + (acc_->id() & 0xFF); - } + // inspection - virtual - state_tba_proxy* clone() const - { - return new state_tba_proxy(*this); - } + state_tba_proxy* + current_state() const + { + // A transition in the *EXPECTED acceptance set should be directed + // to the next acceptance set. If the current transition is also + // in the next acceptance set, then go the one after, etc. + // + // See Denis Oddoux's PhD thesis for a nice explanation (in French). + // @PhDThesis{ oddoux.03.phd, + // author = {Denis Oddoux}, + // title = {Utilisation des automates alternants pour un + // model-checking efficace des logiques temporelles + // lin{\'e}aires.}, + // school = {Universit{\'e}e Paris 7}, + // year = {2003}, + // address = {Paris, France}, + // month = {December} + // } + // + iterator next = expected_; + bdd acc = it_->current_acceptance_conditions(); + while ((acc & *next) == *next && next != end_) + ++next; + return new state_tba_proxy(it_->current_state(), next); + } - private: - state* s_; - iterator acc_; - }; + bdd + current_condition() const + { + return it_->current_condition(); + } + bdd + current_acceptance_conditions() const + { + return the_acceptance_cond_; + } - /// \brief Iterate over the successors of tgba_tba_proxy computed on the fly. - class tgba_tba_proxy_succ_iterator: public tgba_succ_iterator - { - typedef tgba_tba_proxy::cycle_list list; - typedef tgba_tba_proxy::cycle_list::const_iterator iterator; - public: - tgba_tba_proxy_succ_iterator(tgba_succ_iterator* it, - iterator expected, iterator end, - bdd the_acceptance_cond) - : it_(it), expected_(expected), end_(end), - the_acceptance_cond_(the_acceptance_cond) - { - } - - virtual - ~tgba_tba_proxy_succ_iterator() - { - delete it_; - } - - // iteration - - void - first() - { - it_->first(); - } - - void - next() - { - it_->next(); - } - - bool - done() const - { - return it_->done(); - } - - // inspection - - state_tba_proxy* - current_state() const - { - // A transition in the *EXPECTED acceptance set should be directed - // to the next acceptance set. If the current transition is also - // in the next acceptance set, then go the one after, etc. - // - // See Denis Oddoux's PhD thesis for a nice explanation (in French). - // @PhDThesis{ oddoux.03.phd, - // author = {Denis Oddoux}, - // title = {Utilisation des automates alternants pour un - // model-checking efficace des logiques temporelles - // lin{\'e}aires.}, - // school = {Universit{\'e}e Paris 7}, - // year = {2003}, - // address = {Paris, France}, - // month = {December} - // } - // - iterator next = expected_; - bdd acc = it_->current_acceptance_conditions(); - while ((acc & *next) == *next && next != end_) - ++next; - return new state_tba_proxy(it_->current_state(), next); - } - - bdd - current_condition() const - { - return it_->current_condition(); - } - - bdd - current_acceptance_conditions() const - { - return the_acceptance_cond_; - } - - protected: - tgba_succ_iterator* it_; - const iterator expected_; - const iterator end_; - const bdd the_acceptance_cond_; - }; + protected: + tgba_succ_iterator* it_; + const iterator expected_; + const iterator end_; + const bdd the_acceptance_cond_; + }; + } // anonymous tgba_tba_proxy::tgba_tba_proxy(const tgba* a) : a_(a) diff --git a/src/tgbaalgos/dotty.cc b/src/tgbaalgos/dotty.cc index 8b245d802..cb4bf0e0f 100644 --- a/src/tgbaalgos/dotty.cc +++ b/src/tgbaalgos/dotty.cc @@ -28,51 +28,53 @@ namespace spot { - - class dotty_bfs : public tgba_reachable_iterator_breadth_first + namespace { - public: - dotty_bfs(const tgba* a, std::ostream& os) - : tgba_reachable_iterator_breadth_first(a), os_(os) + class dotty_bfs : public tgba_reachable_iterator_breadth_first { - } + public: + dotty_bfs(const tgba* a, std::ostream& os) + : tgba_reachable_iterator_breadth_first(a), os_(os) + { + } - void - start() - { - os_ << "digraph G {" << std::endl; - os_ << " 0 [label=\"\", style=invis, height=0]" << std::endl; - os_ << " 0 -> 1" << std::endl; - } + void + start() + { + os_ << "digraph G {" << std::endl; + os_ << " 0 [label=\"\", style=invis, height=0]" << std::endl; + os_ << " 0 -> 1" << std::endl; + } - void - end() - { - os_ << "}" << std::endl; - } + void + end() + { + os_ << "}" << std::endl; + } - void - process_state(const state* s, int n, tgba_succ_iterator*) - { - os_ << " " << n << " [label=\""; - escape_str(os_, automata_->format_state(s)) << "\"]" << std::endl; - } + void + process_state(const state* s, int n, tgba_succ_iterator*) + { + os_ << " " << n << " [label=\""; + escape_str(os_, automata_->format_state(s)) << "\"]" << std::endl; + } - void - process_link(int in, int out, const tgba_succ_iterator* si) - { - os_ << " " << in << " -> " << out << " [label=\""; - escape_str(os_, bdd_format_formula(automata_->get_dict(), - si->current_condition())) << "\\n"; - escape_str(os_, - bdd_format_accset(automata_->get_dict(), - si->current_acceptance_conditions())) - << "\"]" << std::endl; - } + void + process_link(int in, int out, const tgba_succ_iterator* si) + { + os_ << " " << in << " -> " << out << " [label=\""; + escape_str(os_, bdd_format_formula(automata_->get_dict(), + si->current_condition())) << "\\n"; + escape_str(os_, + bdd_format_accset(automata_->get_dict(), + si->current_acceptance_conditions())) + << "\"]" << std::endl; + } - private: - std::ostream& os_; - }; + private: + std::ostream& os_; + }; + } std::ostream& dotty_reachable(std::ostream& os, const tgba* g) diff --git a/src/tgbaalgos/dupexp.cc b/src/tgbaalgos/dupexp.cc index 54c2923ad..e81e72300 100644 --- a/src/tgbaalgos/dupexp.cc +++ b/src/tgbaalgos/dupexp.cc @@ -25,73 +25,77 @@ #include #include "reachiter.hh" -namespace spot { - - template - class dupexp_iter: public T +namespace spot +{ + namespace { - public: - dupexp_iter(const tgba* a) - : T(a), out_(new tgba_explicit(a->get_dict())) + template + class dupexp_iter: public T { - } + public: + dupexp_iter(const tgba* a) + : T(a), out_(new tgba_explicit(a->get_dict())) + { + } - tgba_explicit* - result() - { - return out_; - } + tgba_explicit* + result() + { + return out_; + } - void - process_state(const state* s, int n, tgba_succ_iterator*) - { - std::ostringstream os; - os << "(#" << n << ") " << this->automata_->format_state(s); - name_[n] = os.str(); - } + void + process_state(const state* s, int n, tgba_succ_iterator*) + { + std::ostringstream os; + os << "(#" << n << ") " << this->automata_->format_state(s); + name_[n] = os.str(); + } - std::string - declare_state(const state* s, int n) - { - std::string str; - name_map_::const_iterator i = name_.find(n); - if (i == name_.end()) - { - std::ostringstream os; - os << "(#" << n << ") " << this->automata_->format_state(s); - name_[n] = str = os.str(); - } - else - { - str = i->second; - } - delete s; - return str; - } + std::string + declare_state(const state* s, int n) + { + std::string str; + name_map_::const_iterator i = name_.find(n); + if (i == name_.end()) + { + std::ostringstream os; + os << "(#" << n << ") " << this->automata_->format_state(s); + name_[n] = str = os.str(); + } + else + { + str = i->second; + } + delete s; + return str; + } - void - process_link(int in, int out, const tgba_succ_iterator* si) - { - // We might need to format out before process_state is called. - name_map_::const_iterator i = name_.find(out); - if (i == name_.end()) - { - const state* s = si->current_state(); - process_state(s, out, 0); - delete s; - } + void + process_link(int in, int out, const tgba_succ_iterator* si) + { + // We might need to format out before process_state is called. + name_map_::const_iterator i = name_.find(out); + if (i == name_.end()) + { + const state* s = si->current_state(); + process_state(s, out, 0); + delete s; + } - tgba_explicit::transition* t = - out_->create_transition(name_[in], name_[out]); - out_->add_conditions(t, si->current_condition()); - out_->add_acceptance_conditions(t, si->current_acceptance_conditions()); - } + tgba_explicit::transition* t = + out_->create_transition(name_[in], name_[out]); + out_->add_conditions(t, si->current_condition()); + out_->add_acceptance_conditions(t, si->current_acceptance_conditions()); + } - private: - tgba_explicit* out_; - typedef std::map name_map_; - std::map name_; - }; + private: + tgba_explicit* out_; + typedef std::map name_map_; + std::map name_; + }; + + } // anonymous tgba_explicit* tgba_dupexp_bfs(const tgba* aut) diff --git a/src/tgbaalgos/gtec/nsheap.cc b/src/tgbaalgos/gtec/nsheap.cc index 47159096f..4335bd235 100644 --- a/src/tgbaalgos/gtec/nsheap.cc +++ b/src/tgbaalgos/gtec/nsheap.cc @@ -23,54 +23,57 @@ namespace spot { - class numbered_state_heap_hash_map_const_iterator : - public numbered_state_heap_const_iterator + namespace { - public: - numbered_state_heap_hash_map_const_iterator - (const numbered_state_heap_hash_map::hash_type& h) - : numbered_state_heap_const_iterator(), h(h) + class numbered_state_heap_hash_map_const_iterator: + public numbered_state_heap_const_iterator { - } + public: + numbered_state_heap_hash_map_const_iterator + (const numbered_state_heap_hash_map::hash_type& h) + : numbered_state_heap_const_iterator(), h(h) + { + } - ~numbered_state_heap_hash_map_const_iterator() - { - } + ~numbered_state_heap_hash_map_const_iterator() + { + } - virtual void - first() - { - i = h.begin(); - } + virtual void + first() + { + i = h.begin(); + } - virtual void - next() - { - ++i; - } + virtual void + next() + { + ++i; + } - virtual bool - done() const - { - return i == h.end(); - } + virtual bool + done() const + { + return i == h.end(); + } - virtual const state* - get_state() const - { - return i->first; - } + virtual const state* + get_state() const + { + return i->first; + } - virtual int - get_index() const - { - return i->second; - } + virtual int + get_index() const + { + return i->second; + } - private: - numbered_state_heap_hash_map::hash_type::const_iterator i; - const numbered_state_heap_hash_map::hash_type& h; - }; + private: + numbered_state_heap_hash_map::hash_type::const_iterator i; + const numbered_state_heap_hash_map::hash_type& h; + }; + } // anonymous numbered_state_heap_hash_map::~numbered_state_heap_hash_map() { diff --git a/src/tgbaalgos/gtec/nsheap.hh b/src/tgbaalgos/gtec/nsheap.hh index aab8294ca..4f3134667 100644 --- a/src/tgbaalgos/gtec/nsheap.hh +++ b/src/tgbaalgos/gtec/nsheap.hh @@ -119,12 +119,11 @@ namespace spot virtual int size() const; virtual numbered_state_heap_const_iterator* iterator() const; - protected: + typedef Sgi::hash_map hash_type; + protected: hash_type h; ///< Map of visited states. - - friend class numbered_state_heap_hash_map_const_iterator; }; /// \brief Factory for numbered_state_heap_hash_map. diff --git a/src/tgbaalgos/lbtt.cc b/src/tgbaalgos/lbtt.cc index e254e6d26..266666ea3 100644 --- a/src/tgbaalgos/lbtt.cc +++ b/src/tgbaalgos/lbtt.cc @@ -30,129 +30,132 @@ namespace spot { - // At some point we'll need to print an acceptance set into LBTT's - // format. LBTT expects numbered acceptance sets, so first we'll - // number each acceptance condition, and latter when we have to print - // them we'll just have to look up each of them. - class acceptance_cond_splitter + namespace { - public: - acceptance_cond_splitter(bdd all_acc) + // At some point we'll need to print an acceptance set into LBTT's + // format. LBTT expects numbered acceptance sets, so first we'll + // number each acceptance condition, and latter when we have to print + // them we'll just have to look up each of them. + class acceptance_cond_splitter { - unsigned count = 0; - while (all_acc != bddfalse) - { - bdd acc = bdd_satone(all_acc); - all_acc -= acc; - sm[acc] = count++; - } - } - - std::ostream& - split(std::ostream& os, bdd b) - { - while (b != bddfalse) - { - bdd acc = bdd_satone(b); - b -= acc; - os << sm[acc] << " "; - } - return os; - } - - unsigned - count() const - { - return sm.size(); - } - - private: - typedef std::map split_map; - split_map sm; - }; - - // Convert a BDD formula to the syntax used by LBTT's transition guards. - // Conjunctions are printed by bdd_format_sat, so we just have - // to handle the other cases. - static std::string - bdd_to_lbtt(bdd b, const bdd_dict* d) - { - if (b == bddfalse) - return "f"; - else if (b == bddtrue) - return "t"; - else + public: + acceptance_cond_splitter(bdd all_acc) { - bdd cube = bdd_satone(b); - b -= cube; - if (b != bddfalse) + unsigned count = 0; + while (all_acc != bddfalse) { - return "| " + bdd_to_lbtt(b, d) + " " + bdd_to_lbtt(cube, d); - } - else - { - std::string res = ""; - for (int count = bdd_nodecount(cube); count > 1; --count) - res += "& "; - return res + bdd_format_sat(d, cube); + bdd acc = bdd_satone(all_acc); + all_acc -= acc; + sm[acc] = count++; } } - } + std::ostream& + split(std::ostream& os, bdd b) + { + while (b != bddfalse) + { + bdd acc = bdd_satone(b); + b -= acc; + os << sm[acc] << " "; + } + return os; + } - class lbtt_bfs : public tgba_reachable_iterator_breadth_first - { - public: - lbtt_bfs(const tgba* a, std::ostream& os) - : tgba_reachable_iterator_breadth_first(a), - os_(os), - acc_count_(0), - acs_(a->all_acceptance_conditions()) + unsigned + count() const + { + return sm.size(); + } + private: + typedef std::map split_map; + split_map sm; + }; + + // Convert a BDD formula to the syntax used by LBTT's transition guards. + // Conjunctions are printed by bdd_format_sat, so we just have + // to handle the other cases. + static std::string + bdd_to_lbtt(bdd b, const bdd_dict* d) { - // Count the number of acceptance_conditions. - bdd all = a->all_acceptance_conditions(); - while (all != bddfalse) - { - bdd one = bdd_satone(all); - all -= one; - ++acc_count_; - } - } - - void - process_state(const state*, int n, tgba_succ_iterator*) - { - --n; - if (n == 0) - body_ << "0 1" << std::endl; + if (b == bddfalse) + return "f"; + else if (b == bddtrue) + return "t"; else - body_ << "-1" << std::endl << n << " 0" << std::endl; + { + bdd cube = bdd_satone(b); + b -= cube; + if (b != bddfalse) + { + return "| " + bdd_to_lbtt(b, d) + " " + bdd_to_lbtt(cube, d); + } + else + { + std::string res = ""; + for (int count = bdd_nodecount(cube); count > 1; --count) + res += "& "; + return res + bdd_format_sat(d, cube); + } + } + } - void - process_link(int, int out, const tgba_succ_iterator* si) + class lbtt_bfs : public tgba_reachable_iterator_breadth_first { - body_ << out - 1 << " "; - acs_.split(body_, si->current_acceptance_conditions()); - body_ << "-1 " << bdd_to_lbtt(si->current_condition(), - automata_->get_dict()) << std::endl; - } + public: + lbtt_bfs(const tgba* a, std::ostream& os) + : tgba_reachable_iterator_breadth_first(a), + os_(os), + acc_count_(0), + acs_(a->all_acceptance_conditions()) - void - end() - { - os_ << seen.size() << " " << acc_count_ << "t" << std::endl - << body_.str() << "-1" << std::endl; - } + { + // Count the number of acceptance_conditions. + bdd all = a->all_acceptance_conditions(); + while (all != bddfalse) + { + bdd one = bdd_satone(all); + all -= one; + ++acc_count_; + } + } - private: - std::ostream& os_; - std::ostringstream body_; - unsigned acc_count_; - acceptance_cond_splitter acs_; - }; + void + process_state(const state*, int n, tgba_succ_iterator*) + { + --n; + if (n == 0) + body_ << "0 1" << std::endl; + else + body_ << "-1" << std::endl << n << " 0" << std::endl; + } + void + process_link(int, int out, const tgba_succ_iterator* si) + { + body_ << out - 1 << " "; + acs_.split(body_, si->current_acceptance_conditions()); + body_ << "-1 " << bdd_to_lbtt(si->current_condition(), + automata_->get_dict()) << std::endl; + } + + void + end() + { + os_ << seen.size() << " " << acc_count_ << "t" << std::endl + << body_.str() << "-1" << std::endl; + } + + private: + std::ostream& os_; + std::ostringstream body_; + unsigned acc_count_; + acceptance_cond_splitter acs_; + }; + + } // anonymous std::ostream& lbtt_reachable(std::ostream& os, const tgba* g) @@ -161,6 +164,4 @@ namespace spot b.run(); return os; } - - } diff --git a/src/tgbaalgos/ltl2tgba_lacim.cc b/src/tgbaalgos/ltl2tgba_lacim.cc index f7c4293a4..fe6ce96b7 100644 --- a/src/tgbaalgos/ltl2tgba_lacim.cc +++ b/src/tgbaalgos/ltl2tgba_lacim.cc @@ -31,225 +31,228 @@ namespace spot { - using namespace ltl; - - /// \brief Recursively translate a formula into a BDD. - /// - /// The algorithm used here is adapted from Jean-Michel Couvreur's - /// Probataf tool. - class ltl_trad_visitor: public const_visitor + namespace { - public: - ltl_trad_visitor(tgba_bdd_concrete_factory& fact, bool root = false) - : fact_(fact), root_(root) - { - } + using namespace ltl; - virtual - ~ltl_trad_visitor() + /// \brief Recursively translate a formula into a BDD. + /// + /// The algorithm used here is adapted from Jean-Michel Couvreur's + /// Probataf tool. + class ltl_trad_visitor: public const_visitor { - } + public: + ltl_trad_visitor(tgba_bdd_concrete_factory& fact, bool root = false) + : fact_(fact), root_(root) + { + } - bdd - result() - { - return res_; - } + virtual + ~ltl_trad_visitor() + { + } - void - visit(const atomic_prop* node) - { - res_ = bdd_ithvar(fact_.create_atomic_prop(node)); - } + bdd + result() + { + return res_; + } - void - visit(const constant* node) - { - switch (node->val()) - { - case constant::True: - res_ = bddtrue; - return; - case constant::False: - res_ = bddfalse; - return; - } - /* Unreachable code. */ - assert(0); - } + void + visit(const atomic_prop* node) + { + res_ = bdd_ithvar(fact_.create_atomic_prop(node)); + } - void - visit(const unop* node) - { - switch (node->op()) - { - case unop::F: + void + visit(const constant* node) + { + switch (node->val()) { - /* - Fx <=> x | XFx - In other words: - now <=> x | next - */ - int v = fact_.create_state(node); - bdd now = bdd_ithvar(v); - bdd next = bdd_ithvar(v + 1); - bdd x = recurse(node->child()); - fact_.constrain_relation(bdd_apply(now, x | next, bddop_biimp)); - /* - `x | next', doesn't actually encode the fact that x - should be fulfilled eventually. We ensure this by - creating a new generalized Büchi acceptance set, Acc[x], - and leave out of this set any transition going off NOW - without checking X. Such acceptance conditions are - checked for during the emptiness check. - */ - fact_.declare_acceptance_condition(x | !now, node->child()); - res_ = now; + case constant::True: + res_ = bddtrue; + return; + case constant::False: + res_ = bddfalse; return; } - case unop::G: - { - bdd child = recurse(node->child()); - // If G occurs at the top of the formula we don't - // need Now/Next variables. We just constrain - // the relation so that the child always happens. - // This saves 2 BDD variables. - if (root_) - { - fact_.constrain_relation(child); - res_ = child; - return; - } - // Gx <=> x && XGx - int v = fact_.create_state(node); - bdd now = bdd_ithvar(v); - bdd next = bdd_ithvar(v + 1); - fact_.constrain_relation(bdd_apply(now, child & next, - bddop_biimp)); - res_ = now; - return; - } - case unop::Not: - { - res_ = bdd_not(recurse(node->child())); - return; - } - case unop::X: - { - int v = fact_.create_state(node->child()); - bdd now = bdd_ithvar(v); - bdd next = bdd_ithvar(v + 1); - fact_.constrain_relation(bdd_apply(now, recurse(node->child()), - bddop_biimp)); - res_ = next; - return; - } - } - /* Unreachable code. */ - assert(0); - } + /* Unreachable code. */ + assert(0); + } - void - visit(const binop* node) - { - bdd f1 = recurse(node->first()); - bdd f2 = recurse(node->second()); - - switch (node->op()) - { - case binop::Xor: - res_ = bdd_apply(f1, f2, bddop_xor); - return; - case binop::Implies: - res_ = bdd_apply(f1, f2, bddop_imp); - return; - case binop::Equiv: - res_ = bdd_apply(f1, f2, bddop_biimp); - return; - case binop::U: + void + visit(const unop* node) + { + switch (node->op()) { - /* - f1 U f2 <=> f2 | (f1 & X(f1 U f2)) - In other words: - now <=> f2 | (f1 & next) - */ - int v = fact_.create_state(node); - bdd now = bdd_ithvar(v); - bdd next = bdd_ithvar(v + 1); - fact_.constrain_relation(bdd_apply(now, f2 | (f1 & next), - bddop_biimp)); - /* - The rightmost conjunction, f1 & next, doesn't actually - encode the fact that f2 should be fulfilled eventually. - We declare an acceptance condition for this purpose (see - the comment in the unop::F case). - */ - fact_.declare_acceptance_condition(f2 | !now, node->second()); - res_ = now; - return; + case unop::F: + { + /* + Fx <=> x | XFx + In other words: + now <=> x | next + */ + int v = fact_.create_state(node); + bdd now = bdd_ithvar(v); + bdd next = bdd_ithvar(v + 1); + bdd x = recurse(node->child()); + fact_.constrain_relation(bdd_apply(now, x | next, bddop_biimp)); + /* + `x | next', doesn't actually encode the fact that x + should be fulfilled eventually. We ensure this by + creating a new generalized Büchi acceptance set, Acc[x], + and leave out of this set any transition going off NOW + without checking X. Such acceptance conditions are + checked for during the emptiness check. + */ + fact_.declare_acceptance_condition(x | !now, node->child()); + res_ = now; + return; + } + case unop::G: + { + bdd child = recurse(node->child()); + // If G occurs at the top of the formula we don't + // need Now/Next variables. We just constrain + // the relation so that the child always happens. + // This saves 2 BDD variables. + if (root_) + { + fact_.constrain_relation(child); + res_ = child; + return; + } + // Gx <=> x && XGx + int v = fact_.create_state(node); + bdd now = bdd_ithvar(v); + bdd next = bdd_ithvar(v + 1); + fact_.constrain_relation(bdd_apply(now, child & next, + bddop_biimp)); + res_ = now; + return; + } + case unop::Not: + { + res_ = bdd_not(recurse(node->child())); + return; + } + case unop::X: + { + int v = fact_.create_state(node->child()); + bdd now = bdd_ithvar(v); + bdd next = bdd_ithvar(v + 1); + fact_.constrain_relation(bdd_apply(now, recurse(node->child()), + bddop_biimp)); + res_ = next; + return; + } } - case binop::R: + /* Unreachable code. */ + assert(0); + } + + void + visit(const binop* node) + { + bdd f1 = recurse(node->first()); + bdd f2 = recurse(node->second()); + + switch (node->op()) { - /* - f1 R f2 <=> f2 & (f1 | X(f1 R f2)) - In other words: - now <=> f2 & (f1 | next) - */ - int v = fact_.create_state(node); - bdd now = bdd_ithvar(v); - bdd next = bdd_ithvar(v + 1); - fact_.constrain_relation(bdd_apply(now, f2 & (f1 | next), - bddop_biimp)); - res_ = now; + case binop::Xor: + res_ = bdd_apply(f1, f2, bddop_xor); return; + case binop::Implies: + res_ = bdd_apply(f1, f2, bddop_imp); + return; + case binop::Equiv: + res_ = bdd_apply(f1, f2, bddop_biimp); + return; + case binop::U: + { + /* + f1 U f2 <=> f2 | (f1 & X(f1 U f2)) + In other words: + now <=> f2 | (f1 & next) + */ + int v = fact_.create_state(node); + bdd now = bdd_ithvar(v); + bdd next = bdd_ithvar(v + 1); + fact_.constrain_relation(bdd_apply(now, f2 | (f1 & next), + bddop_biimp)); + /* + The rightmost conjunction, f1 & next, doesn't actually + encode the fact that f2 should be fulfilled eventually. + We declare an acceptance condition for this purpose (see + the comment in the unop::F case). + */ + fact_.declare_acceptance_condition(f2 | !now, node->second()); + res_ = now; + return; + } + case binop::R: + { + /* + f1 R f2 <=> f2 & (f1 | X(f1 R f2)) + In other words: + now <=> f2 & (f1 | next) + */ + int v = fact_.create_state(node); + bdd now = bdd_ithvar(v); + bdd next = bdd_ithvar(v + 1); + fact_.constrain_relation(bdd_apply(now, f2 & (f1 | next), + bddop_biimp)); + res_ = now; + return; + } } - } - /* Unreachable code. */ - assert(0); - } + /* Unreachable code. */ + assert(0); + } - void - visit(const multop* node) - { - int op = -1; - bool root = false; - switch (node->op()) - { - case multop::And: - op = bddop_and; - res_ = bddtrue; - // When the root formula is a conjunction it's ok to - // consider all children as root formulae. This allows the - // root-G trick to save many more variable. (See the - // translation of G.) - root = root_; - break; - case multop::Or: - op = bddop_or; - res_ = bddfalse; - break; - } - assert(op != -1); - unsigned s = node->size(); - for (unsigned n = 0; n < s; ++n) - { - res_ = bdd_apply(res_, recurse(node->nth(n), root), op); - } - } + void + visit(const multop* node) + { + int op = -1; + bool root = false; + switch (node->op()) + { + case multop::And: + op = bddop_and; + res_ = bddtrue; + // When the root formula is a conjunction it's ok to + // consider all children as root formulae. This allows the + // root-G trick to save many more variable. (See the + // translation of G.) + root = root_; + break; + case multop::Or: + op = bddop_or; + res_ = bddfalse; + break; + } + assert(op != -1); + unsigned s = node->size(); + for (unsigned n = 0; n < s; ++n) + { + res_ = bdd_apply(res_, recurse(node->nth(n), root), op); + } + } - bdd - recurse(const formula* f, bool root = false) - { - ltl_trad_visitor v(fact_, root); - f->accept(v); - return v.result(); - } + bdd + recurse(const formula* f, bool root = false) + { + ltl_trad_visitor v(fact_, root); + f->accept(v); + return v.result(); + } - private: - bdd res_; - tgba_bdd_concrete_factory& fact_; - bool root_; - }; + private: + bdd res_; + tgba_bdd_concrete_factory& fact_; + bool root_; + }; + } // anonymous tgba_bdd_concrete* ltl_to_tgba_lacim(const ltl::formula* f, bdd_dict* dict) diff --git a/src/tgbaalgos/neverclaim.cc b/src/tgbaalgos/neverclaim.cc index 74e29802e..6ade239a2 100644 --- a/src/tgbaalgos/neverclaim.cc +++ b/src/tgbaalgos/neverclaim.cc @@ -32,153 +32,155 @@ namespace spot { - - class never_claim_bfs : public tgba_reachable_iterator_breadth_first + namespace { - public: - never_claim_bfs(const tgba_tba_proxy* a, std::ostream& os, - const ltl::formula* f) - : tgba_reachable_iterator_breadth_first(a), - os_(os), f_(f), accept_all_(-1), fi_needed_(false) + class never_claim_bfs : public tgba_reachable_iterator_breadth_first { - } + public: + never_claim_bfs(const tgba_tba_proxy* a, std::ostream& os, + const ltl::formula* f) + : tgba_reachable_iterator_breadth_first(a), + os_(os), f_(f), accept_all_(-1), fi_needed_(false) + { + } - void - start() - { - os_ << "never {"; - if (f_) - { - os_ << " /* "; - to_string(f_, os_); - os_ << " */"; - } - os_ << std::endl; - init_ = automata_->get_init_state(); - } + void + start() + { + os_ << "never {"; + if (f_) + { + os_ << " /* "; + to_string(f_, os_); + os_ << " */"; + } + os_ << std::endl; + init_ = automata_->get_init_state(); + } - void - end() - { - if (fi_needed_) - os_ << " fi;" << std::endl; - if (accept_all_ != -1) - { - os_ << "accept_all:" << std::endl; - os_ << " skip" << std::endl; - } - os_ << "}" << std::endl; - delete init_; - } + void + end() + { + if (fi_needed_) + os_ << " fi;" << std::endl; + if (accept_all_ != -1) + { + os_ << "accept_all:" << std::endl; + os_ << " skip" << std::endl; + } + os_ << "}" << std::endl; + delete init_; + } - bool - state_is_accepting(const state *s) - { - return - dynamic_cast(automata_)->state_is_accepting(s); - } + bool + state_is_accepting(const state *s) + { + return + dynamic_cast(automata_)->state_is_accepting(s); + } - std::string - get_state_label(const state* s, int n) - { - std::string label; - if (s->compare(init_) == 0) - if (state_is_accepting(s)) - label = "accept_init"; - else - label = "T0_init"; - else - { - std::ostringstream ost; - ost << n; - std::string ns(ost.str()); + std::string + get_state_label(const state* s, int n) + { + std::string label; + if (s->compare(init_) == 0) + if (state_is_accepting(s)) + label = "accept_init"; + else + label = "T0_init"; + else + { + std::ostringstream ost; + ost << n; + std::string ns(ost.str()); - if (state_is_accepting(s)) - { - tgba_succ_iterator* it = automata_->succ_iter(s); - it->first(); - if (it->done()) - label = "accept_S" + ns; - else - { - state* current = it->current_state(); - if (it->current_condition() != bddtrue - || s->compare(current) != 0) - label = "accept_S" + ns; - else - label = "accept_all"; - delete current; - } - delete it; - } - else - label = "T0_S" + ns; - } - return label; - } + if (state_is_accepting(s)) + { + tgba_succ_iterator* it = automata_->succ_iter(s); + it->first(); + if (it->done()) + label = "accept_S" + ns; + else + { + state* current = it->current_state(); + if (it->current_condition() != bddtrue + || s->compare(current) != 0) + label = "accept_S" + ns; + else + label = "accept_all"; + delete current; + } + delete it; + } + else + label = "T0_S" + ns; + } + return label; + } - void - process_state(const state* s, int n, tgba_succ_iterator*) - { - tgba_succ_iterator* it = automata_->succ_iter(s); - it->first(); - if (it->done()) - { - if (fi_needed_ != 0) - os_ << " fi;" << std::endl; - os_ << get_state_label(s, n) << ": "; - os_ << "/* " << automata_->format_state(s) << " */"; - os_ << std::endl; - os_ << " if" << std::endl; - os_ << " :: (0) -> goto " << get_state_label(s, n) << std::endl; - fi_needed_ = true; - } - else - { - state* current =it->current_state(); - if (state_is_accepting(s) - && it->current_condition() == bddtrue - && s->compare(init_) != 0 - && s->compare(current) == 0) - accept_all_ = n; - else - { - if (fi_needed_) - os_ << " fi;" << std::endl; - os_ << get_state_label(s, n) << ": "; - os_ << "/* " << automata_->format_state(s) << " */"; - os_ << std::endl; - os_ << " if" << std::endl; - fi_needed_ = true; - } - delete current; - } - delete it; - } + void + process_state(const state* s, int n, tgba_succ_iterator*) + { + tgba_succ_iterator* it = automata_->succ_iter(s); + it->first(); + if (it->done()) + { + if (fi_needed_ != 0) + os_ << " fi;" << std::endl; + os_ << get_state_label(s, n) << ": "; + os_ << "/* " << automata_->format_state(s) << " */"; + os_ << std::endl; + os_ << " if" << std::endl; + os_ << " :: (0) -> goto " << get_state_label(s, n) << std::endl; + fi_needed_ = true; + } + else + { + state* current =it->current_state(); + if (state_is_accepting(s) + && it->current_condition() == bddtrue + && s->compare(init_) != 0 + && s->compare(current) == 0) + accept_all_ = n; + else + { + if (fi_needed_) + os_ << " fi;" << std::endl; + os_ << get_state_label(s, n) << ": "; + os_ << "/* " << automata_->format_state(s) << " */"; + os_ << std::endl; + os_ << " if" << std::endl; + fi_needed_ = true; + } + delete current; + } + delete it; + } - void - process_link(int in, int out, const tgba_succ_iterator* si) - { - if (in != accept_all_) - { - os_ << " :: ("; - const ltl::formula* f = bdd_to_formula(si->current_condition(), - automata_->get_dict()); - to_spin_string(f, os_); - destroy(f); - state* current = si->current_state(); - os_ << ") -> goto " << get_state_label(current, out) << std::endl; - delete current; - } - } + void + process_link(int in, int out, const tgba_succ_iterator* si) + { + if (in != accept_all_) + { + os_ << " :: ("; + const ltl::formula* f = bdd_to_formula(si->current_condition(), + automata_->get_dict()); + to_spin_string(f, os_); + destroy(f); + state* current = si->current_state(); + os_ << ") -> goto " << get_state_label(current, out) << std::endl; + delete current; + } + } - private: - std::ostream& os_; - const ltl::formula* f_; - int accept_all_; - bool fi_needed_; - state* init_; - }; + private: + std::ostream& os_; + const ltl::formula* f_; + int accept_all_; + bool fi_needed_; + state* init_; + }; + } // anonymous std::ostream& never_claim_reachable(std::ostream& os, const tgba_tba_proxy* g, diff --git a/src/tgbaalgos/save.cc b/src/tgbaalgos/save.cc index cd61c797a..4329c6eff 100644 --- a/src/tgbaalgos/save.cc +++ b/src/tgbaalgos/save.cc @@ -28,72 +28,73 @@ namespace spot { - - class save_bfs : public tgba_reachable_iterator_breadth_first + namespace { - public: - save_bfs(const tgba* a, std::ostream& os) - : tgba_reachable_iterator_breadth_first(a), os_(os) + class save_bfs: public tgba_reachable_iterator_breadth_first { - } + public: + save_bfs(const tgba* a, std::ostream& os) + : tgba_reachable_iterator_breadth_first(a), os_(os) + { + } - void - start() - { - os_ << "acc ="; - print_acc(automata_->all_acceptance_conditions()) << ";" << std::endl; - } + void + start() + { + os_ << "acc ="; + print_acc(automata_->all_acceptance_conditions()) << ";" << std::endl; + } - void - process_state(const state* s, int, tgba_succ_iterator* si) - { - const bdd_dict* d = automata_->get_dict(); - std::string cur = automata_->format_state(s); - for (si->first(); !si->done(); si->next()) - { - state* dest = si->current_state(); - os_ << "\"" << cur << "\", \"" - << automata_->format_state(dest) << "\", \""; - escape_str(os_, bdd_format_formula(d, si->current_condition())); - os_ << "\","; - print_acc(si->current_acceptance_conditions()) << ";" << std::endl; - delete dest; - } - } + void + process_state(const state* s, int, tgba_succ_iterator* si) + { + const bdd_dict* d = automata_->get_dict(); + std::string cur = automata_->format_state(s); + for (si->first(); !si->done(); si->next()) + { + state* dest = si->current_state(); + os_ << "\"" << cur << "\", \"" + << automata_->format_state(dest) << "\", \""; + escape_str(os_, bdd_format_formula(d, si->current_condition())); + os_ << "\","; + print_acc(si->current_acceptance_conditions()) << ";" << std::endl; + delete dest; + } + } - private: - std::ostream& os_; - - std::ostream& - print_acc(bdd acc) - { - const bdd_dict* d = automata_->get_dict(); - while (acc != bddfalse) - { - bdd cube = bdd_satone(acc); - acc -= cube; - while (cube != bddtrue) - { - assert(cube != bddfalse); - // Display the first variable that is positive. - // There should be only one per satisfaction. - if (bdd_high(cube) != bddfalse) - { - int v = bdd_var(cube); - bdd_dict::vf_map::const_iterator vi = - d->acc_formula_map.find(v); - assert(vi != d->acc_formula_map.end()); - os_ << " \""; - escape_str(os_, ltl::to_string(vi->second)) << "\""; - break; - } - cube = bdd_low(cube); - } - } - return os_; - } - }; + private: + std::ostream& os_; + std::ostream& + print_acc(bdd acc) + { + const bdd_dict* d = automata_->get_dict(); + while (acc != bddfalse) + { + bdd cube = bdd_satone(acc); + acc -= cube; + while (cube != bddtrue) + { + assert(cube != bddfalse); + // Display the first variable that is positive. + // There should be only one per satisfaction. + if (bdd_high(cube) != bddfalse) + { + int v = bdd_var(cube); + bdd_dict::vf_map::const_iterator vi = + d->acc_formula_map.find(v); + assert(vi != d->acc_formula_map.end()); + os_ << " \""; + escape_str(os_, ltl::to_string(vi->second)) << "\""; + break; + } + cube = bdd_low(cube); + } + } + return os_; + } + }; + } std::ostream& tgba_save_reachable(std::ostream& os, const tgba* g) diff --git a/src/tgbaalgos/stats.cc b/src/tgbaalgos/stats.cc index 3f59de79a..353b86108 100644 --- a/src/tgbaalgos/stats.cc +++ b/src/tgbaalgos/stats.cc @@ -25,30 +25,32 @@ namespace spot { - - class stats_bfs : public tgba_reachable_iterator_breadth_first + namespace { - public: - stats_bfs(const tgba* a, tgba_statistics& s) - : tgba_reachable_iterator_breadth_first(a), s_(s) + class stats_bfs: public tgba_reachable_iterator_breadth_first { - } + public: + stats_bfs(const tgba* a, tgba_statistics& s) + : tgba_reachable_iterator_breadth_first(a), s_(s) + { + } - void - process_state(const state*, int, tgba_succ_iterator*) - { - ++s_.states; - } + void + process_state(const state*, int, tgba_succ_iterator*) + { + ++s_.states; + } - void - process_link(int, int, const tgba_succ_iterator*) - { - ++s_.transitions; - } + void + process_link(int, int, const tgba_succ_iterator*) + { + ++s_.transitions; + } - private: - tgba_statistics& s_; - }; + private: + tgba_statistics& s_; + }; + } // anonymous tgba_statistics stats_reachable(const tgba* g)