diff --git a/ChangeLog b/ChangeLog index 08ce8ec6c..69983a348 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,16 @@ +2009-09-29 Guillaume Sadegh + + A new complementation construction based on ranking. + + * src/tgba/tgbacomplement.cc, src/tgba/tgbacomplement.hh: The + construction. + * src/tgbatest/Makefile.am: Adjust. + * src/tgbatest/complementation.cc: Add options to support this + construction in addition to Safra construction. + * src/tgba/Makefile.am: Adjust. + * src/tgbatest/complementation.test: Adjust to test also this + complementation. + 2009-09-29 Guillaume Sadegh * src/ltltest/randltl.cc, src/ltltest/reduc.test, diff --git a/src/tgba/Makefile.am b/src/tgba/Makefile.am index 317d57f8a..9e3567e26 100644 --- a/src/tgba/Makefile.am +++ b/src/tgba/Makefile.am @@ -40,6 +40,7 @@ tgba_HEADERS = \ tgbabddconcreteproduct.hh \ tgbabddcoredata.hh \ tgbabddfactory.hh \ + tgbacomplement.hh \ tgbaexplicit.hh \ tgbafromfile.hh \ tgbascc.hh \ @@ -63,8 +64,9 @@ libtgba_la_SOURCES = \ tgbabddconcretefactory.cc \ tgbabddconcreteproduct.cc \ tgbabddcoredata.cc \ - tgbafromfile.cc \ + tgbacomplement.cc \ tgbaexplicit.cc \ + tgbafromfile.cc \ tgbaproduct.cc \ tgbareduc.cc \ tgbasafracomplement.cc \ diff --git a/src/tgba/tgbacomplement.cc b/src/tgba/tgbacomplement.cc new file mode 100644 index 000000000..394bb4ff0 --- /dev/null +++ b/src/tgba/tgbacomplement.cc @@ -0,0 +1,794 @@ +#include +#include +#include +#include +#include "bdd.h" +#include "state.hh" +#include "tgbacomplement.hh" +#include "misc/hash.hh" +#include "tgbaalgos/bfssteps.hh" +#include "misc/hashfunc.hh" +#include "ltlast/formula.hh" +#include "ltlast/constant.hh" + +namespace spot +{ + /// \brief An Equivalence Relation for \c boost::shared_ptr. + /// \ingroup tgba_essentials + /// + /// This is meant to be used as a comparison functor for + /// Sgi \c hash_map whose key are of type \c boost::shared_ptr. + /// + /// For instance here is how one could declare + /// a map of \c boost::shared_ptr + /// \code + /// // Remember how many times each state has been visited. + /// Sgi::hash_map, int, + /// spot::state_shared_ptr_hash, + /// spot::state_shared_ptr_equal> seen; + /// \endcode + struct state_shared_ptr_equal: + public std::binary_function, + boost::shared_ptr, bool> + { + bool + operator()(boost::shared_ptr left, + boost::shared_ptr right) const + { + assert(left); + return 0 == left->compare(right.get()); + } + }; + + + /// \brief Hash Function for \c boost::shared_ptr. + /// \ingroup tgba_essentials + /// \ingroup hash_funcs + /// + /// This is meant to be used as a hash functor for + /// Sgi's \c hash_map whose key are of type + /// \c boost::shared_ptr. + /// + /// For instance here is how one could declare + /// a map of \c boost::shared_ptr. + /// \code + /// // Remember how many times each state has been visited. + /// Sgi::hash_map, int, + /// spot::state_shared_ptr_hash, + /// spot::state_shared_ptr_equal> seen; + /// \endcode + struct state_shared_ptr_hash: + public std::unary_function, size_t> + { + size_t + operator()(boost::shared_ptr that) const + { + assert(that); + return that->hash(); + } + }; + + namespace + { + //////////////////////////////////////// + // rank + + /// \brief A rank structure, one of the main structure of the algorithm. + /// + /// A rank has a number (\a rank) that refers to the depth in the DAG of + /// the current word. When the rank is odd, a \a condition is associated + /// to this rank. + struct rank_t + { + mutable unsigned rank; + mutable bdd_ordered condition; + + bool operator<(const rank_t& other) const + { + return rank < other.rank || + condition.order() < other.condition.order(); + } + + unsigned get_rank() const + { + return rank; + } + + bdd_ordered get_condition() const + { + return condition; + } + + size_t hash() const + { + size_t hash = wang32_hash(rank); + if (rank & 1) + hash ^= wang32_hash(condition.order()); + return hash; + } + + std::string format() const + { + std::ostringstream ss; + ss << "{rank: " << rank; + if (rank & 1) + { + ss << ", bdd: {" << condition.order() << ", " << + bddset << condition.get_bdd() << "} "; + } + ss << "}"; + return ss.str(); + } + }; + + // typedefs. + typedef boost::shared_ptr shared_state; + typedef Sgi::hash_map state_rank_map; + typedef Sgi::hash_set state_set; + + //////////////////////////////////////// + // count_states + + /// \brief Count the number of states in a tgba. + class count_states : public bfs_steps + { + public: + count_states(const tgba* a) + : bfs_steps(a) + { + shared_state s(a->get_init_state()); + states_.insert(s); + + tgba_run::steps l; + search(s.get(), l); + } + + virtual const state* filter(const state* s) + { + shared_state _s(s); + if (states_.find(_s) == states_.end()) + { + states_.insert(_s); + return s; + } + return 0; + } + + virtual bool match(tgba_run::step&, const state*) + { + return false; + } + + size_t size() const + { + return states_.size(); + } + private: + state_set states_; + }; + + //////////////////////////////////////// + // state_complement + + /// States used by spot::tgba_complement. + /// A state has a map of states associated to ranks, and a set + /// of filtered states. + /// \ingroup tgba_representation + class state_complement : public state + { + public: + state_complement(); + state_complement(const state_complement& other); + state_complement(state_rank_map state_map, state_set state_filter); + virtual ~state_complement() {} + + virtual int compare(const state* other) const; + virtual size_t hash() const; + virtual state_complement* clone() const; + + void add(shared_state state, const rank_t& rank); + const state_rank_map& get_state_map() const; + const state_set& get_filter_set() const; + bool accepting() const; + private: + state_rank_map state_map_; + state_set state_filter_; + }; + + state_complement::state_complement() + { + } + + state_complement::state_complement(state_rank_map state_map, + state_set state_filter) + : state_map_(state_map), state_filter_(state_filter) + { + } + + state_complement::state_complement(const state_complement& other) + { + state_map_ = other.state_map_; + state_filter_ = other.state_filter_; + } + + int + state_complement::compare(const state* o) const + { + const state_complement* other = dynamic_cast(o); + + if (other == 0) + return 1; + + if (state_map_.size() < other->state_map_.size()) + return -1; + else if (state_map_.size() > other->state_map_.size()) + return 1; + + if (state_filter_.size() < other->state_filter_.size()) + return -1; + else if (state_filter_.size() > other->state_filter_.size()) + return 1; + + { + state_rank_map::const_iterator i = state_map_.begin(); + state_rank_map::const_iterator j = other->state_map_.begin(); + while (i != state_map_.end() && j != other->state_map_.end()) + { + int result = i->first->compare(j->first.get()); + if (result != 0) + return result; + if (i->second < j->second) + return -1; + if (j->second < i->second) + return 1; + ++i; + ++j; + } + } + + { + state_set::const_iterator i = state_filter_.begin(); + state_set::const_iterator j = other->state_filter_.begin(); + while (i != state_filter_.end() && j != other->state_filter_.end()) + { + int result = (*i)->compare(j->get()); + if (result != 0) + return result; + ++i; + ++j; + } + } + + return 0; + } + + size_t + state_complement::hash() const + { + size_t hash = 0; + + { + state_rank_map::const_iterator i = state_map_.begin(); + while (i != state_map_.end()) + { + hash ^= i->first->hash(); + hash ^= i->second.hash(); + ++i; + } + } + + { + state_set::const_iterator i = state_filter_.begin(); + while (i != state_filter_.end()) + { + hash ^= (*i)->hash(); + ++i; + } + } + + return hash; + } + + state_complement* + state_complement::clone() const + { + return new state_complement(*this); + } + + void + state_complement::add(shared_state state, + const rank_t& rank) + { + state_map_[state] = rank; + } + + const state_rank_map& + state_complement::get_state_map() const + { + return state_map_; + } + + const state_set& + state_complement::get_filter_set() const + { + return state_filter_; + } + + bool + state_complement::accepting() const + { + return state_filter_.empty(); + } + + /// Successor iterators used by spot::tgba_complement. + /// \ingroup tgba_representation + /// + /// Since the algorithm works on-the-fly, the key components of the + /// algorithm are implemented in this class. + /// + /// + class tgba_complement_succ_iterator: public tgba_succ_iterator + { + public: + typedef std::list bdd_list_t; + + tgba_complement_succ_iterator(const tgba_sgba_proxy* automaton, + bdd the_acceptance_cond, + const acc_list_t& acc_list, + const state_complement* origin); + virtual ~tgba_complement_succ_iterator() {}; + + virtual void first(); + virtual void next(); + virtual bool done() const; + virtual state_complement* current_state() const; + virtual bdd current_condition() const; + virtual bdd current_acceptance_conditions() const; + private: + /// \brief Create the highest rank of \a origin_ as origin and + /// \a condition as successor condition. + void successor_highest_rank(bdd condition); + void get_atomics(std::set& list, bdd c); + void get_conj_list(); + bool is_valid_rank() const; + bool next_valid_rank(); + + const tgba_sgba_proxy* automaton_; + bdd the_acceptance_cond_; + const acc_list_t& acc_list_; + const state_complement* origin_; + const state_complement* current_state_; + bdd_list_t condition_list_; + bdd_list_t::const_iterator current_condition_; + state_rank_map highest_current_ranks_; + state_rank_map current_ranks_; + state_set highest_state_set_; + }; + + tgba_complement_succ_iterator:: + tgba_complement_succ_iterator(const tgba_sgba_proxy* automaton, + bdd the_acceptance_cond, + const acc_list_t& acc_list, + const state_complement* origin) + : automaton_(automaton), the_acceptance_cond_(the_acceptance_cond), + acc_list_(acc_list), origin_(origin) + { + get_conj_list(); + } + + /// Insert in \a list atomic properties of the formula \a c. + void + tgba_complement_succ_iterator::get_atomics(std::set& list, bdd c) + { + bdd current = bdd_satone(c); + while (current != bddtrue && current != bddfalse) + { + list.insert(bdd_var(current)); + bdd high = bdd_high(current); + if (high == bddfalse) + current = bdd_low(current); + else + current = high; + } + } + + /// Create the conjunction of all the atomic properties from + /// the successors of the current state. + void + tgba_complement_succ_iterator::get_conj_list() + { + std::set atomics; + condition_list_.clear(); + state_rank_map sr_map = origin_->get_state_map(); + + // Retrieve all the atomics in acceptance conditions. + for (state_rank_map::const_iterator i = sr_map.begin(); + i != sr_map.end(); + ++i) + { + tgba_succ_iterator* iterator = automaton_->succ_iter(i->first.get()); + for (iterator->first(); !iterator->done(); iterator->next()) + { + bdd c = iterator->current_condition(); + get_atomics(atomics, c); + } + delete iterator; + } + + // Compute the conjunction of all those atomic properties. + unsigned atomics_size = atomics.size(); + + assert(atomics_size < 32); + for (unsigned i = 1; i <= static_cast(1 << atomics_size); ++i) + { + bdd result = bddtrue; + unsigned position = 1; + for (std::set::const_iterator a_it = atomics.begin(); + a_it != atomics.end(); + ++a_it, position <<= 1) + { + bdd this_atomic; + if (position & i) + this_atomic = bdd_ithvar(*a_it); + else + this_atomic = bdd_nithvar(*a_it); + result = bdd_apply(result, this_atomic, bddop_and); + } + condition_list_.push_back(result); + } + } + + /// Check whether \a current_ranks_ is a valid rank. + /// For each odd rank, its condition associated must not + /// be present in its tracked state. + bool + tgba_complement_succ_iterator::is_valid_rank() const + { + for (state_rank_map::const_iterator i = current_ranks_.begin(); + i != current_ranks_.end(); + ++i) + { + if (i->second.rank & 1) + { + if ((automaton_->state_acceptance_conditions(i->first.get()) & + i->second.condition.get_bdd()) != bddfalse) + return false; + } + } + return true; + } + + /// \brief Decrease \a current_ranks_ and produces a valid rank. + /// \a current_ranks_ is a map of states to a rank. + /// A rank for a state is valid if it is inferior than the rank of its + /// predecessor. + /// When the rank is odd, its has an acceptance condition associated that + /// must not be in its associated state. + /// \return false if there is not valid rank as successor. + bool tgba_complement_succ_iterator::next_valid_rank() + { + state_rank_map::const_iterator i; + do { + for (i = current_ranks_.begin(); + i != current_ranks_.end(); + ++i) + { + if (i->second.rank != 0) + { + if (i->second.rank & 1) + { + if (i->second.condition.order() == 0) + --i->second.rank; + else + i->second.condition = + acc_list_[i->second.condition.order() - 1]; + } + else + { + --i->second.rank; + i->second.condition = acc_list_[acc_list_.size() - 1]; + } + break; + } + else + { + current_ranks_[i->first] = highest_current_ranks_[i->first]; + } + } + } + while ((i != current_ranks_.end()) && !is_valid_rank()); + + return i != current_ranks_.end(); + } + + /// \brief Create the highest rank of \a origin_ as origin and + /// \a condition as successor condition. + void + tgba_complement_succ_iterator::successor_highest_rank(bdd condition) + { + // Highest rank for bdd. + state_rank_map sr_map = origin_->get_state_map(); + highest_current_ranks_.clear(); + + for (state_rank_map::const_iterator i = sr_map.begin(); + i != sr_map.end(); + ++i) + { + tgba_succ_iterator* iterator = automaton_->succ_iter(i->first.get()); + for (iterator->first(); !iterator->done(); iterator->next()) + { + bdd c = iterator->current_condition(); + if ((c & condition) != bddfalse) + { + shared_state s(iterator->current_state()); + if (highest_current_ranks_.find(s) != highest_current_ranks_.end()) + { + if (i->second < highest_current_ranks_[s]) + highest_current_ranks_[s] = i->second; + } + else + highest_current_ranks_[s] = i->second; + } + } + delete iterator; + } + + // Highest $O$ set of the algorithm. + state_set s_set = origin_->get_filter_set(); + highest_state_set_.clear(); + + for (state_set::const_iterator i = s_set.begin(); + i != s_set.end(); + ++i) + { + tgba_succ_iterator* iterator = automaton_->succ_iter(i->get()); + for (iterator->first(); !iterator->done(); iterator->next()) + { + bdd c = iterator->current_condition(); + if ((c & condition) != bddfalse) + { + shared_state s(iterator->current_state()); + highest_state_set_.insert(s); + } + } + delete iterator; + } + + current_ranks_ = highest_current_ranks_; + } + + void + tgba_complement_succ_iterator::first() + { + current_condition_ = condition_list_.begin(); + if (done()) + return; + + successor_highest_rank(*current_condition_); + + if (!is_valid_rank()) + next_valid_rank(); + } + + void + tgba_complement_succ_iterator::next() + { + if (done()) + return; + + if (!next_valid_rank()) + { + ++current_condition_; + if (!done()) + { + successor_highest_rank(*current_condition_); + if (!is_valid_rank()) + next_valid_rank(); + } + } + } + + bool + tgba_complement_succ_iterator::done() const + { + return (current_condition_ == condition_list_.end()); + } + + state_complement* + tgba_complement_succ_iterator::current_state() const + { + if (done()) + return 0; + + // If the filter set is empty, all the states of the map + // that are associated to an even rank create the new filter set. + state_set filter; + if (origin_->get_filter_set().empty()) + { + for (state_rank_map::const_iterator i = current_ranks_.begin(); + i != current_ranks_.end(); + ++i) + if (!(i->second.rank & 1)) + filter.insert(i->first); + } + else + { + // It the filter set is non-empty, we delete from this set states + // that are now associated to an odd rank. + for (state_set::const_iterator i = highest_state_set_.begin(); + i != highest_state_set_.end(); + ++i) + { + state_rank_map::const_iterator s(current_ranks_.find(*i)); + assert(s != current_ranks_.end()); + + if (!(s->second.get_rank() & 1)) + filter.insert(*i); + } + } + + return new state_complement(current_ranks_, filter); + } + + bdd + tgba_complement_succ_iterator::current_condition() const + { + if (done()) + return bddfalse; + return *current_condition_; + } + + bdd + tgba_complement_succ_iterator::current_acceptance_conditions() const + { + if (done()) + return bddfalse; + + // This algorithm doesn't generalized acceptance conditions. + if (origin_->accepting()) + return the_acceptance_cond_; + else + return bddfalse; + } + + } // end namespace anonymous. + + /// Retrieve all the atomic acceptance conditions of the automaton. + /// They are inserted into \a acc_list_. + void + tgba_complement::get_acc_list() + { + bdd c = automaton_->all_acceptance_conditions(); + bdd current = bdd_satone(c); + unsigned i = 0; + while (current != bddtrue && current != bddfalse) + { + acc_list_.push_back(bdd_ordered(bdd_var(current), i)); + ++i; + bdd high = bdd_high(current); + if (high == bddfalse) + current = bdd_low(current); + else + current = high; + } + } + + tgba_complement::tgba_complement(const tgba* a) + : automaton_(new tgba_sgba_proxy(a)) + { + get_dict()->register_all_variables_of(automaton_, this); + int v = get_dict() + ->register_acceptance_variable(ltl::constant::true_instance(), this); + the_acceptance_cond_ = bdd_ithvar(v); + { + count_states count(automaton_); + nb_states_ = count.size(); + } + get_acc_list(); + } + + tgba_complement::~tgba_complement() + { + get_dict()->unregister_all_my_variables(this); + delete automaton_; + } + + state* + tgba_complement::get_init_state() const + { + state_complement* init = new state_complement(); + rank_t r = {2 * nb_states_, bdd_ordered()}; + init->add(shared_state(automaton_->get_init_state()), r); + return init; + } + + tgba_succ_iterator* + tgba_complement::succ_iter(const state* local_state, + const state*, + const tgba*) const + { + const state_complement* state = + dynamic_cast(local_state); + assert(state); + + return new tgba_complement_succ_iterator(automaton_, + the_acceptance_cond_, + acc_list_, state); + } + + bdd_dict* + tgba_complement::get_dict() const + { + return automaton_->get_dict(); + } + + std::string + tgba_complement::format_state(const state* state) const + { + const state_complement* s = dynamic_cast(state); + assert(s); + std::ostringstream ss; + ss << "{ set: {" << std::endl; + + const state_rank_map& state_map = s->get_state_map(); + const state_set& state_filter = s->get_filter_set(); + + for (state_rank_map::const_iterator i = state_map.begin(); + i != state_map.end(); + ++i) + { + ss << " {" << automaton_->format_state(i->first.get()) + << ", " << i->second.format() << "}" << std::endl; + } + ss << "} odd-less: {"; + + for (state_set::const_iterator i = state_filter.begin(); + i != state_filter.end(); + ++i) + { + ss << " " << automaton_->format_state(i->get()) << std::endl; + } + + ss << "} }"; + return ss.str(); + } + + bdd + tgba_complement::all_acceptance_conditions() const + { + return the_acceptance_cond_; + } + + bdd + tgba_complement::neg_acceptance_conditions() const + { + return !the_acceptance_cond_; + } + + bdd + tgba_complement::compute_support_conditions(const state* state) const + { + tgba_succ_iterator* i = succ_iter(state); + bdd result = bddtrue; + for (i->first(); !i->done(); i->next()) + result |= i->current_condition(); + delete i; + return result; + } + + bdd + tgba_complement::compute_support_variables(const state* state) const + { + tgba_succ_iterator* i = succ_iter(state); + bdd result = bddtrue; + for (i->first(); !i->done(); i->next()) + result &= bdd_support(i->current_condition()); + delete i; + return result; + } + +} // end namespace spot. diff --git a/src/tgba/tgbacomplement.hh b/src/tgba/tgbacomplement.hh new file mode 100644 index 000000000..36dea136c --- /dev/null +++ b/src/tgba/tgbacomplement.hh @@ -0,0 +1,99 @@ +#ifndef SPOT_TGBA_TGBACOMPLEMENT_HH +#define SPOT_TGBA_TGBACOMPLEMENT_HH + +#include +#include "bdd.h" +#include "tgba.hh" +#include "tgba/tgbasgba.hh" + +namespace spot +{ + class bdd_ordered + { + public: + bdd_ordered() + : order_(0) + {}; + + bdd_ordered(int bdd_, unsigned order_) + : bdd_(bdd_), order_(order_) + { + } + + unsigned order() const + { + return order_; + } + + unsigned& order() + { + return order_; + } + + bdd get_bdd() const + { + return bdd_ithvar(bdd_); + } + private: + int bdd_; + unsigned order_; + }; + + typedef std::vector acc_list_t; + + /// \brief Build a complemented automaton. + /// \ingroup tgba + /// + /// The construction comes from: + /// @Article{ kupferman.05.tcs, + /// title = {{From complementation to certification}}, + /// author = {Kupferman, O. and Vardi, M.Y.}, + /// journal = {Theoretical Computer Science}, + /// volume = {345}, + /// number = {1}, + /// pages = {83--100}, + /// year = {2005}, + /// publisher = {Elsevier} + /// } + /// + /// The original automaton is used as a States-based Generalized + /// Büchi Automaton. + /// + /// The construction is done on-the-fly, by the + /// \c tgba_complement_succ_iterator class. + /// \see tgba_complement_succ_iteratora + class tgba_complement : public tgba + { + public: + tgba_complement(const tgba* a); + virtual ~tgba_complement(); + + // tgba interface + 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 state* state) const; + virtual bdd compute_support_variables(const state* state) const; + private: + /// Retrieve all the atomic acceptance conditions of the automaton. + /// They are inserted into \a acc_list_. + void get_acc_list(); + private: + const tgba_sgba_proxy* automaton_; + bdd the_acceptance_cond_; + unsigned nb_states_; + acc_list_t acc_list_; + }; // end class tgba_complement. + +} // end namespace spot. + + +#endif // !SPOT_TGBA_TGBACOMPLEMENT_HH diff --git a/src/tgbatest/Makefile.am b/src/tgbatest/Makefile.am index 8d09fb440..79e473f04 100644 --- a/src/tgbatest/Makefile.am +++ b/src/tgbatest/Makefile.am @@ -31,7 +31,7 @@ check_SCRIPTS = defs # Keep this sorted alphabetically. check_PROGRAMS = \ bddprod \ - safracomplement \ + complement \ explicit \ expldot \ explprod \ diff --git a/src/tgbatest/complementation.cc b/src/tgbatest/complementation.cc index 40c986b9b..ce227af42 100644 --- a/src/tgbatest/complementation.cc +++ b/src/tgbatest/complementation.cc @@ -16,18 +16,22 @@ #include "tgba/tgbatba.hh" #include "tgba/tgbasafracomplement.hh" +#include "tgba/tgbacomplement.hh" void usage(const char* prog) { std::cout << "usage: " << prog << " [options]" << std::endl; std::cout << "with options" << std::endl + << "-S Use safra complementation" + << std::endl << "-s buchi_automaton display the safra automaton" << std::endl << "-a buchi_automaton display the complemented automaton" << std::endl << "-astat buchi_automaton statistics for !a" << std::endl << "-fstat formula statistics for !A_f" << std::endl - << "-f formula test !A_f and !A_!f" << std::endl; + << "-f formula test !A_f and !A_!f" << std::endl + << "-p formula print the automaton for f" << std::endl; } int main(int argc, char* argv[]) @@ -40,6 +44,8 @@ int main(int argc, char* argv[]) bool stats = false; bool formula = false; bool automaton = false; + bool safra = false; + bool print_formula = false; if (argc < 3) { @@ -67,12 +73,16 @@ int main(int argc, char* argv[]) switch (argv[i][1]) { + case 'S': + safra = true; break; case 's': - print_safra = true; break; + safra = true; print_safra = true; break; case 'a': print_automaton = true; break; case 'f': check = true; break; + case 'p': + print_formula = true; break; default: std::cerr << "unrecognized option `-" << argv[i][1] << "'" << std::endl; @@ -98,14 +108,46 @@ int main(int argc, char* argv[]) if (spot::format_tgba_parse_errors(std::cerr, file, pel)) return 2; - spot::tgba_safra_complement* complement = - new spot::tgba_safra_complement(a); + spot::tgba* complement = 0; + + if (safra) + complement = new spot::tgba_safra_complement(a); + else + complement = new spot::tgba_complement(a); if (print_automaton) spot::dotty_reachable(std::cout, complement); if (print_safra) - spot::display_safra(complement); + { + spot::tgba_safra_complement* safra_complement = + dynamic_cast(complement); + spot::display_safra(safra_complement); + } + delete complement; + delete a; + } + else if (print_formula) + { + spot::tgba* a; + spot::ltl::formula* f1 = 0; + + spot::ltl::parse_error_list p1; + f1 = spot::ltl::parse(file, p1); + + if (spot::ltl::format_parse_errors(std::cerr, file, p1)) + return 2; + + a = spot::ltl_to_tgba_fm(f1, dict); + + spot::tgba* complement = 0; + if (safra) + complement = new spot::tgba_safra_complement(a); + else + complement = new spot::tgba_complement(a); + + spot::dotty_reachable(std::cout, complement); + spot::ltl::destroy(f1); delete complement; delete a; } @@ -133,7 +175,7 @@ int main(int argc, char* argv[]) return 2; } - spot::tgba_safra_complement* complement = + spot::tgba_safra_complement* safra_complement = new spot::tgba_safra_complement(a); spot::tgba_statistics a_size = spot::stats_reachable(a); @@ -152,8 +194,18 @@ int main(int argc, char* argv[]) << std::endl; delete buchi; - spot::tgba_statistics b_size = spot::stats_reachable(complement); - std::cout << "Complement: " + spot::tgba_statistics b_size = spot::stats_reachable(safra_complement); + std::cout << "Safra Complement: " + << b_size.states << ", " + << b_size.transitions << ", " + << safra_complement->number_of_acceptance_conditions() + << std::endl; + + spot::tgba_complement* complement = + new spot::tgba_complement(a); + + b_size = spot::stats_reachable(complement); + std::cout << "GBA Complement: " << b_size.states << ", " << b_size.transitions << ", " << complement->number_of_acceptance_conditions() @@ -191,8 +243,19 @@ int main(int argc, char* argv[]) spot::ltl::formula* nf1 = spot::ltl::unop::instance(spot::ltl::unop::Not, spot::ltl::clone(f1)); spot::tgba* Anf = spot::ltl_to_tgba_fm(nf1, dict); - spot::tgba_safra_complement* nAf = new spot::tgba_safra_complement(Af); - spot::tgba_safra_complement* nAnf = new spot::tgba_safra_complement(Anf); + + spot::tgba* nAf; + spot::tgba* nAnf; + if (safra) + { + nAf = new spot::tgba_safra_complement(Af); + nAnf = new spot::tgba_safra_complement(Anf); + } + else + { + nAf = new spot::tgba_complement(Af); + nAnf = new spot::tgba_complement(Anf); + } spot::tgba* prod = new spot::tgba_product(nAf, nAnf); spot::emptiness_check* ec = spot::couvreur99(prod); spot::emptiness_check_result* res = ec->check(); diff --git a/src/tgbatest/complementation.test b/src/tgbatest/complementation.test index 355448e13..aea8f12ca 100755 --- a/src/tgbatest/complementation.test +++ b/src/tgbatest/complementation.test @@ -26,6 +26,7 @@ set -e while read f; do run 0 ../complement -f "$f" + run 0 ../complement -S -f "$f" done <