diff --git a/src/bin/ltl2tgba.cc b/src/bin/ltl2tgba.cc index bd13d062a..a2f8fca07 100644 --- a/src/bin/ltl2tgba.cc +++ b/src/bin/ltl2tgba.cc @@ -35,7 +35,6 @@ #include "ltlast/formula.hh" #include "ltlvisit/tostring.hh" -#include "tgba/tgbaexplicit.hh" #include "tgbaalgos/dotty.hh" #include "tgbaalgos/lbtt.hh" #include "tgbaalgos/neverclaim.hh" diff --git a/src/priv/countstates.cc b/src/priv/countstates.cc index 28fcac415..587800731 100644 --- a/src/priv/countstates.cc +++ b/src/priv/countstates.cc @@ -18,7 +18,6 @@ // along with this program. If not, see . #include "countstates.hh" -#include "tgba/tgbaexplicit.hh" #include "tgba/tgbagraph.hh" #include "tgbaalgos/stats.hh" @@ -28,10 +27,6 @@ namespace spot { if (auto b = dynamic_cast(a)) return b->num_states(); - if (auto b = dynamic_cast(a)) - return b->num_states(); - if (auto b = dynamic_cast(a)) - return b->num_states(); return stats_reachable(a).states; } } diff --git a/src/tgba/Makefile.am b/src/tgba/Makefile.am index 20a11daf8..15fbba016 100644 --- a/src/tgba/Makefile.am +++ b/src/tgba/Makefile.am @@ -35,7 +35,6 @@ tgba_HEADERS = \ succiter.hh \ taatgba.hh \ tgba.hh \ - tgbaexplicit.hh \ tgbagraph.hh \ tgbakvcomplement.hh \ tgbamask.hh \ @@ -56,7 +55,6 @@ libtgba_la_SOURCES = \ futurecondcol.cc \ taatgba.cc \ tgba.cc \ - tgbaexplicit.cc \ tgbakvcomplement.cc \ tgbaproduct.cc \ tgbamask.cc \ diff --git a/src/tgba/tgbaexplicit.cc b/src/tgba/tgbaexplicit.cc deleted file mode 100644 index 83109ae93..000000000 --- a/src/tgba/tgbaexplicit.cc +++ /dev/null @@ -1,28 +0,0 @@ -// Copyright (C) 2012 Laboratoire de Recherche et Développement -// de l'Epita (LRDE). -// -// This file is part of Spot, a model checking library. -// -// Spot is free software; you can redistribute it and/or modify it -// under the terms of the GNU General Public License as published by -// the Free Software Foundation; either version 3 of the License, or -// (at your option) any later version. -// -// Spot is distributed in the hope that it will be useful, but WITHOUT -// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY -// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public -// License for more details. -// -// You should have received a copy of the GNU General Public License -// along with this program. If not, see . - -#include "tgbaexplicit.hh" -#include "ltlast/constant.hh" - -namespace spot -{ - const std::string state_explicit_string::default_val("empty"); - const int state_explicit_number::default_val(0); - const ltl::formula* - state_explicit_formula::default_val(ltl::constant::true_instance()); -} diff --git a/src/tgba/tgbaexplicit.hh b/src/tgba/tgbaexplicit.hh deleted file mode 100644 index be7989a11..000000000 --- a/src/tgba/tgbaexplicit.hh +++ /dev/null @@ -1,831 +0,0 @@ -// -*- coding: utf-8 -*- -// Copyright (C) 2009, 2010, 2011, 2012, 2013, 2014 Laboratoire de -// Recherche et Développement de l'Epita. -// Copyright (C) 2003, 2004, 2006 Laboratoire d'Informatique de Paris -// 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), -// Université Pierre et Marie Curie. -// -// This file is part of Spot, a model checking library. -// -// Spot is free software; you can redistribute it and/or modify it -// under the terms of the GNU General Public License as published by -// the Free Software Foundation; either version 3 of the License, or -// (at your option) any later version. -// -// Spot is distributed in the hope that it will be useful, but WITHOUT -// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY -// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public -// License for more details. -// -// You should have received a copy of the GNU General Public License -// along with this program. If not, see . - -#ifndef SPOT_TGBA_TGBAEXPLICIT_HH -# define SPOT_TGBA_TGBAEXPLICIT_HH - -#include -#include - -#include "tgba.hh" -#include "sba.hh" -#include "tgba/formula2bdd.hh" -#include "misc/hash.hh" -#include "misc/bddop.hh" -#include "ltlast/formula.hh" -#include "ltlvisit/tostring.hh" - -namespace spot -{ - // How to destroy the label of a state. - template - struct SPOT_API destroy_key - { - void destroy(T t) - { - (void) t; - } - }; - - template<> - struct SPOT_API destroy_key - { - void destroy(const ltl::formula* t) - { - t->destroy(); - } - }; - - /// States used by spot::explicit_graph implementation - /// \ingroup tgba_representation - template - class SPOT_API state_explicit: public spot::state - { - public: - state_explicit() - { - } - - state_explicit(const Label& l): - label_(l) - { - } - - virtual ~state_explicit() - { - } - - virtual void destroy() const - { - } - - typedef Label label_t; - typedef label_hash label_hash_t; - - struct transition - { - bdd condition; - bdd acceptance_conditions; - const state_explicit* dest; - }; - - typedef std::list transitions_t; - transitions_t successors; - - const Label& label() const - { - return label_; - } - - bool empty() const - { - return successors.empty(); - } - - virtual int compare(const state* other) const - { - const state_explicit* s = - down_cast*>(other); - assert (s); - - // Do not simply return "o - this", it might not fit in an int. - if (s < this) - return -1; - if (s > this) - return 1; - return 0; - } - - virtual size_t hash() const - { - return - reinterpret_cast(this) - static_cast(0); - } - - virtual state_explicit* - clone() const - { - return const_cast*>(this); - } - - protected: - Label label_; - }; - - /// States labeled by an int - /// \ingroup tgba_representation - class SPOT_API state_explicit_number: - public state_explicit > - { - public: - state_explicit_number() - : state_explicit >() - { - } - - state_explicit_number(int label) - : state_explicit >(label) - { - } - - static const int default_val; - }; - - /// States labeled by a string - /// \ingroup tgba_representation - class SPOT_API state_explicit_string: - public state_explicit - { - public: - state_explicit_string(): - state_explicit() - { - } - - state_explicit_string(const std::string& label) - : state_explicit(label) - { - } - - static const std::string default_val; - }; - - /// States labeled by a formula - /// \ingroup tgba_representation - class SPOT_API state_explicit_formula: -#ifndef SWIG - public state_explicit -#else - public state -#endif - { - public: - state_explicit_formula(): - state_explicit() - { - } - - state_explicit_formula(const ltl::formula* label) - : state_explicit(label) - { - } - - static const ltl::formula* default_val; - }; - - /// Successor iterators used by spot::tgba_explicit. - /// \ingroup tgba_representation - template - class SPOT_API tgba_explicit_succ_iterator: - public tgba_succ_iterator - { - public: - tgba_explicit_succ_iterator(const State* start, - bdd all_acc) - : start_(start), - all_acceptance_conditions_(all_acc) - { - } - - void recycle(const State* start, bdd all_acc) - { - start_ = start; - all_acceptance_conditions_ = all_acc; - } - - virtual bool first() - { - it_ = start_->successors.begin(); - return it_ != start_->successors.end(); - } - - virtual bool next() - { - ++it_; - return it_ != start_->successors.end(); - } - - virtual bool done() const - { - return it_ == start_->successors.end(); - } - - virtual State* current_state() const - { - assert(!done()); - const State* res = down_cast(it_->dest); - assert(res); - return const_cast(res); - } - - virtual bdd current_condition() const - { - assert(!done()); - return it_->condition; - } - - virtual bdd current_acceptance_conditions() const - { - assert(!done()); - return it_->acceptance_conditions; - } - - typename State::transitions_t::const_iterator - get_iterator() const - { - return it_; - } - - private: - const State* start_; - typename State::transitions_t::const_iterator it_; - bdd all_acceptance_conditions_; - }; - - /// Graph implementation for explicit automaton - /// \ingroup tgba_representation - template - class SPOT_API explicit_graph: public Type - { - public: - typedef typename State::label_t label_t; - typedef typename State::label_hash_t label_hash_t; - typedef typename State::transitions_t transitions_t; - typedef typename State::transition transition; - typedef State state; - protected: - typedef std::unordered_map ls_map; - typedef std::unordered_map alias_map; - typedef std::unordered_map > sl_map; - - public: - - explicit_graph(bdd_dict* dict) - : ls_(), - sl_(), - init_(0), - dict_(dict), - all_acceptance_conditions_(bddfalse), - all_acceptance_conditions_computed_(false), - neg_acceptance_conditions_(bddtrue) - { - } - - State* add_default_init() - { - return add_state(State::default_val); - } - - size_t num_states() const - { - return sl_.size(); - } - - transition* - create_transition(State* source, const State* dest) - { - transition t; - - t.dest = dest; - t.condition = bddtrue; - t.acceptance_conditions = bddfalse; - - typename transitions_t::iterator i = - source->successors.insert(source->successors.end(), t); - - return &*i; - } - - transition* - create_transition(const label_t& source, const label_t& dest) - { - // It's important that the source be created before the - // destination, so the first source encountered becomes the - // default initial state. - State* s = add_state(source); - return create_transition(s, add_state(dest)); - } - - transition* - get_transition(const tgba_explicit_succ_iterator* si) - { - return const_cast(&(*(si->get_iterator()))); - } - - transition* - get_transition(const tgba_succ_iterator* si) - { - const tgba_explicit_succ_iterator* tmp - = down_cast*>(si); - assert(tmp); - return get_transition(tmp); - } - - void add_condition(transition* t, const ltl::formula* f) - { - t->condition &= formula_to_bdd(f, dict_, this); - f->destroy(); - } - - /// This assumes that all variables in \a f are known from dict. - void add_conditions(transition* t, bdd f) - { - dict_->register_propositions(f, this); - t->condition &= f; - } - - bool has_acceptance_condition(const ltl::formula* f) const - { - return dict_->is_registered_acceptance_variable(f, this); - } - - //old tgba explicit labeled interface - bool has_state(const label_t& name) - { - return ls_.find(name) != ls_.end(); - } - - /// \brief Return the state associated to a given label. - /// - /// This is similar to add_state(), except that it returns 0 if - /// the state does not exist. - const State* get_state(const label_t& name) - { - typename ls_map::const_iterator i = ls_.find(name); - if (i == ls_.end()) - return 0; - return &i->second; - } - - const label_t& get_label(const State* s) const - { - typename sl_map::const_iterator i = sl_.find(s); - assert(i != sl_.end()); - return i->second; - } - - const label_t& get_label(const spot::state* s) const - { - const State* se = down_cast(s); - assert(se); - return get_label(se); - } - - void - complement_all_acceptance_conditions() - { - bdd all = this->all_acceptance_conditions(); - typename ls_map::iterator i; - for (i = ls_.begin(); i != ls_.end(); ++i) - { - typename transitions_t::iterator i2; - for (i2 = i->second.successors.begin(); - i2 != i->second.successors.end(); ++i2) - i2->acceptance_conditions = all - i2->acceptance_conditions; - } - } - - void - merge_transitions() - { - typedef typename transitions_t::iterator trans_t; - typedef std::map acc_map; - typedef std::unordered_map > dest_map; - - typename ls_map::iterator i; - for (i = ls_.begin(); i != ls_.end(); ++i) - { - const spot::state* last_dest = 0; - dest_map dm; - typename dest_map::iterator dmi = dm.end(); - typename transitions_t::iterator t1 = i->second.successors.begin(); - - // Loop over all outgoing transitions (cond,acc,dest), and - // store them into dest_map[dest][acc] so that we can merge - // conditions. - while (t1 != i->second.successors.end()) - { - const spot::state* dest = t1->dest; - if (dest != last_dest) - { - last_dest = dest; - dmi = dm.find(dest); - if (dmi == dm.end()) - dmi = dm.emplace(dest, acc_map()).first; - } - int acc = t1->acceptance_conditions.id(); - typename acc_map::iterator it = dmi->second.find(acc); - if (it == dmi->second.end()) - { - dmi->second[acc] = t1; - ++t1; - } - else - { - it->second->condition |= t1->condition; - t1 = i->second.successors.erase(t1); - } - } - } - } - - /// Return the state_explicit for \a name, creating the state if - /// it does not exist. - State* add_state(const label_t& name) - { - typename ls_map::iterator i = ls_.find(name); - if (i == ls_.end()) - { - typename alias_map::iterator j = alias_.find(name); - if (j != alias_.end()) - return j->second; - - State* res = &(ls_.emplace(name, State(name)).first->second); - sl_[res] = name; - // The first state we add is the initial state. - // It can also be overridden with set_init_state(). - if (!init_) - init_ = res; - return res; - } - return &(i->second); - } - - State* - set_init_state(const label_t& state) - { - State* s = add_state(state); - init_ = s; - return s; - } - - // tgba interface - virtual ~explicit_graph() - { - typename ls_map::iterator i = ls_.begin(); - - while (i != ls_.end()) - { - label_t s = i->first; - i->second.destroy(); - ++i; - destroy_key dest; - dest.destroy(s); - } - - this->dict_->unregister_all_my_variables(this); - // Thus has already been destroyed by subclasses. - // Prevent destroying by tgba::~tgba. - this->last_support_conditions_input_ = 0; - } - - virtual State* get_init_state() const - { - if (!init_) - const_cast*>(this)->add_default_init(); - - return init_; - } - - virtual tgba_explicit_succ_iterator* - succ_iter(const spot::state* state) const - { - const State* s = down_cast(state); - assert(s); - - if (this->iter_cache_) - { - tgba_explicit_succ_iterator* it = - down_cast*>(this->iter_cache_); - it->recycle(s, this->all_acceptance_conditions()); - this->iter_cache_ = nullptr; - return it; - } - return - new tgba_explicit_succ_iterator(s, - this - ->all_acceptance_conditions()); - } - - - typedef std::string (*to_string_func_t)(const label_t& t); - - void set_to_string_func(to_string_func_t f) - { - to_string_func_ = f; - } - - to_string_func_t get_to_string_func() const - { - return to_string_func_; - } - - virtual std::string format_state(const spot::state* state) const - { - const State* se = down_cast(state); - assert(se); - typename sl_map::const_iterator i = sl_.find(se); - assert(i != sl_.end()); - assert(to_string_func_); - return to_string_func_(i->second); - } - - /// Create an alias for a state. Any reference to \a alias_name - /// will act as a reference to \a real_name. - void add_state_alias(const label_t& alias, const label_t& real) - { - alias_[alias] = add_state(real); - } - - - /// \brief Copy the acceptance conditions of a tgba. - /// - /// If used, this function should be called before creating any - /// transition. - void copy_acceptance_conditions_of(const tgba *a) - { - assert(neg_acceptance_conditions_ == bddtrue); - assert(all_acceptance_conditions_computed_ == false); - bdd f = a->neg_acceptance_conditions(); - this->dict_->register_acceptance_variables(f, this); - neg_acceptance_conditions_ = f; - } - - - /// Acceptance conditions handling - void set_acceptance_conditions(bdd acc) - { - assert(neg_acceptance_conditions_ == bddtrue); - assert(all_acceptance_conditions_computed_ == false); - - this->dict_->register_acceptance_variables(bdd_support(acc), this); - neg_acceptance_conditions_ = compute_neg_acceptance_conditions(acc); - all_acceptance_conditions_computed_ = true; - all_acceptance_conditions_ = acc; - } - - void add_acceptance_condition(transition* t, const ltl::formula* f) - { - bdd c = get_acceptance_condition(f); - t->acceptance_conditions |= c; - } - - /// This assumes that all acceptance conditions in \a f are known from - /// dict. - void add_acceptance_conditions(transition* t, bdd f) - { - bdd sup = bdd_support(f); - this->dict_->register_acceptance_variables(sup, this); - while (sup != bddtrue) - { - neg_acceptance_conditions_ &= bdd_nithvar(bdd_var(sup)); - sup = bdd_high(sup); - } - t->acceptance_conditions |= f; - } - - virtual bdd all_acceptance_conditions() const - { - if (!all_acceptance_conditions_computed_) - { - all_acceptance_conditions_ = - compute_all_acceptance_conditions(neg_acceptance_conditions_); - all_acceptance_conditions_computed_ = true; - } - return all_acceptance_conditions_; - } - - virtual bdd_dict* get_dict() const - { - return this->dict_; - } - - virtual bdd neg_acceptance_conditions() const - { - return neg_acceptance_conditions_; - } - - void - declare_acceptance_condition(const ltl::formula* f) - { - int v = this->dict_->register_acceptance_variable(f, this); - f->destroy(); - bdd neg = bdd_nithvar(v); - neg_acceptance_conditions_ &= neg; - - // Append neg to all acceptance conditions. - - // FIXME: Declaring acceptance conditions after the automaton - // has been constructed is very slow because we traverse the - // entire automaton for each new acceptance condition. It would - // be better to fix the automaton in a single pass after all - // acceptance conditions have been declared. - typename ls_map::iterator i; - for (i = this->ls_.begin(); i != this->ls_.end(); ++i) - { - typename transitions_t::iterator i2; - for (i2 = i->second.successors.begin(); - i2 != i->second.successors.end(); ++i2) - i2->acceptance_conditions &= neg; - } - - all_acceptance_conditions_computed_ = false; - } - - bdd get_acceptance_condition(const ltl::formula* f) - { - bdd_dict::fv_map::iterator i = this->dict_->acc_map.find(f); - assert(this->has_acceptance_condition(f)); - f->destroy(); - bdd v = bdd_ithvar(i->second); - v &= bdd_exist(neg_acceptance_conditions_, v); - return v; - } - - protected: - - virtual bdd compute_support_conditions(const spot::state* in) const - { - const State* s = down_cast(in); - assert(s); - const transitions_t& st = s->successors; - - bdd res = bddfalse; - - typename transitions_t::const_iterator i; - for (i = st.begin(); i != st.end(); ++i) - res |= i->condition; - - return res; - } - - ls_map ls_; - alias_map alias_; - sl_map sl_; - State* init_; - - bdd_dict* dict_; - - mutable bdd all_acceptance_conditions_; - mutable bool all_acceptance_conditions_computed_; - bdd neg_acceptance_conditions_; - to_string_func_t to_string_func_; - }; - - template - class SPOT_API tgba_explicit: - public explicit_graph - { - public: - tgba_explicit(bdd_dict* dict): explicit_graph(dict) - { - } - - virtual ~tgba_explicit() - { - } - - private: - // Disallow copy. - tgba_explicit(const tgba_explicit& other) SPOT_DELETED; - tgba_explicit& operator=(const tgba_explicit& other) SPOT_DELETED; - }; - - template - class SPOT_API sba_explicit: - public explicit_graph - { - public: - sba_explicit(bdd_dict* dict): explicit_graph(dict) - { - } - - virtual ~sba_explicit() - { - } - - virtual bool state_is_accepting(const spot::state* s) const - { - const State* st = down_cast(s); - // Assume that an accepting state has only accepting output transitions - // So we need only to check one to decide - if (st->successors.empty()) - return false; - return (st->successors.front().acceptance_conditions - == this->all_acceptance_conditions()); - } - - private: - // Disallow copy. - sba_explicit(const sba_explicit& other) SPOT_DELETED; - sba_explicit& operator=(const sba_explicit& other) SPOT_DELETED; - }; - - - // It is tempting to write - // - // templateclass graph, typename Type> - // class explicit_conf: public graph - // - // to simplify the typedefs at the end of the file, however swig - // cannot parse this syntax. - - /// Configuration of graph automata - /// \ingroup tgba_representation - template - class SPOT_API explicit_conf: public graph - { - public: - explicit_conf(bdd_dict* d): graph(d) - { - this->set_to_string_func(to_string); - }; - - static std::string to_string(const typename Type::label_t& l) - { - std::stringstream ss; - ss << l; - return ss.str(); - } - }; - - template - class SPOT_API explicit_conf: public graph - { - public: - explicit_conf(bdd_dict* d): graph(d) - { - this->set_to_string_func(to_string); - }; - - static std::string to_string(const std::string& l) - { - return l; - } - }; - - template - class SPOT_API explicit_conf: public graph - { - public: - explicit_conf(bdd_dict* d): graph(d) - { - this->set_to_string_func(to_string); - }; - - // Enable UTF8 output for the formulae that label states. - void enable_utf8() - { - this->set_to_string_func(to_utf8_string); - } - - static std::string to_string(const ltl::formula* const& l) - { - return ltl::to_string(l); - } - - static std::string to_utf8_string(const ltl::formula* const& l) - { - return ltl::to_utf8_string(l); - } - }; - - - // Typedefs for tgba - typedef explicit_conf, - state_explicit_string> tgba_explicit_string; - typedef explicit_conf, - state_explicit_formula> tgba_explicit_formula; - typedef explicit_conf, - state_explicit_number> tgba_explicit_number; - - // Typedefs for sba - typedef explicit_conf, - state_explicit_string> sba_explicit_string; - typedef explicit_conf, - state_explicit_formula> sba_explicit_formula; - typedef explicit_conf, - state_explicit_number> sba_explicit_number; -} - -#endif // SPOT_TGBA_TGBAEXPLICIT_HH diff --git a/src/tgbaalgos/Makefile.am b/src/tgbaalgos/Makefile.am index cc2816999..b482660f2 100644 --- a/src/tgbaalgos/Makefile.am +++ b/src/tgbaalgos/Makefile.am @@ -56,7 +56,6 @@ tgbaalgos_HEADERS = \ randomgraph.hh \ reachiter.hh \ reducerun.hh \ - reductgba_sim.hh \ replayrun.hh \ rundotdec.hh \ safety.hh \ @@ -103,7 +102,6 @@ libtgbaalgos_la_SOURCES = \ randomgraph.cc \ reachiter.cc \ reducerun.cc \ - reductgba_sim.cc \ replayrun.cc \ rundotdec.cc \ safety.cc \ diff --git a/src/tgbaalgos/isweakscc.cc b/src/tgbaalgos/isweakscc.cc index 185a62600..b8471274b 100644 --- a/src/tgbaalgos/isweakscc.cc +++ b/src/tgbaalgos/isweakscc.cc @@ -18,7 +18,6 @@ // along with this program. If not, see . #include "cycles.hh" -#include "tgba/tgbaexplicit.hh" #include "ltlast/formula.hh" #include "isweakscc.hh" diff --git a/src/tgbaalgos/lbtt.cc b/src/tgbaalgos/lbtt.cc index b4a7c4cad..607ad2ce0 100644 --- a/src/tgbaalgos/lbtt.cc +++ b/src/tgbaalgos/lbtt.cc @@ -25,7 +25,6 @@ #include #include #include -#include "tgba/tgbaexplicit.hh" #include "tgba/formula2bdd.hh" #include "reachiter.hh" #include "misc/bddlt.hh" @@ -81,11 +80,13 @@ namespace spot all_acc_conds_(a->all_acceptance_conditions()), acs_(all_acc_conds_), sba_format_(sba_format), - // If outputting with state-based acceptance, check if the - // automaton can be converted into an sba. This makes the - // state_is_accepting() function more efficient. - sba_(sba_format ? dynamic_cast(a) : 0) + // Check if the automaton can be converted into a + // tgba_digraph. This makes the state_is_accepting() + // function more efficient. + sba_(dynamic_cast(a)) { + if (sba_ && !sba_->get_bprop(tgba_digraph::SBA)) + sba_ = nullptr; } bool @@ -165,7 +166,7 @@ namespace spot bdd all_acc_conds_; acceptance_cond_splitter acs_; bool sba_format_; - const sba* sba_; + const tgba_digraph* sba_; }; static diff --git a/src/tgbaalgos/ltl2tgba_fm.cc b/src/tgbaalgos/ltl2tgba_fm.cc index 1e91eb376..de60ca8e2 100644 --- a/src/tgbaalgos/ltl2tgba_fm.cc +++ b/src/tgbaalgos/ltl2tgba_fm.cc @@ -37,7 +37,6 @@ #include "ltl2tgba_fm.hh" #include "tgba/bddprint.hh" #include "tgbaalgos/sccinfo.hh" -#include "tgba/tgbaexplicit.hh" //#include "tgbaalgos/dotty.hh" #include "priv/acccompl.hh" diff --git a/src/tgbaalgos/minimize.cc b/src/tgbaalgos/minimize.cc index f29a57cb3..1b4836b14 100644 --- a/src/tgbaalgos/minimize.cc +++ b/src/tgbaalgos/minimize.cc @@ -615,7 +615,7 @@ namespace spot tgba_digraph* minimize_obligation(const tgba_digraph* aut_f, - const ltl::formula* f, const tgba* aut_neg_f, + const ltl::formula* f, const tgba_digraph* aut_neg_f, bool reject_bigger) { auto min_aut_f = minimize_wdba(aut_f); @@ -656,7 +656,7 @@ namespace spot neg_f->destroy(); // Remove useless SCCs. - const tgba* tmp = scc_filter(aut_neg_f, true); + auto tmp = scc_filter(aut_neg_f, true); delete aut_neg_f; to_free = aut_neg_f = tmp; } diff --git a/src/tgbaalgos/minimize.hh b/src/tgbaalgos/minimize.hh index f8f9c23d5..57edcac8a 100644 --- a/src/tgbaalgos/minimize.hh +++ b/src/tgbaalgos/minimize.hh @@ -152,7 +152,7 @@ namespace spot /// that the minimized WDBA is correct. SPOT_API tgba_digraph* minimize_obligation(const tgba_digraph* aut_f, const ltl::formula* f = 0, - const tgba* aut_neg_f = 0, + const tgba_digraph* aut_neg_f = 0, bool reject_bigger = false); /// @} diff --git a/src/tgbaalgos/powerset.cc b/src/tgbaalgos/powerset.cc index 5ce9d1d82..9254b4af1 100644 --- a/src/tgbaalgos/powerset.cc +++ b/src/tgbaalgos/powerset.cc @@ -328,7 +328,7 @@ namespace spot unsigned threshold_states, unsigned threshold_cycles, const ltl::formula* f, - const tgba* neg_aut) + const tgba_digraph* neg_aut) { const tgba* built = 0; if (f == 0 && neg_aut == 0) @@ -349,7 +349,7 @@ namespace spot neg_f->destroy(); // Remove useless SCCs. - const tgba* tmp = scc_filter(neg_aut, true); + auto tmp = scc_filter(neg_aut, true); delete neg_aut; built = neg_aut = tmp; } diff --git a/src/tgbaalgos/powerset.hh b/src/tgbaalgos/powerset.hh index 2c9dc9a7b..fdbdc378b 100644 --- a/src/tgbaalgos/powerset.hh +++ b/src/tgbaalgos/powerset.hh @@ -143,7 +143,7 @@ namespace spot unsigned threshold_states = 0, unsigned threshold_cycles = 0, const ltl::formula* f = 0, - const tgba* neg_aut = 0); + const tgba_digraph* neg_aut = 0); } diff --git a/src/tgbaalgos/reductgba_sim.cc b/src/tgbaalgos/reductgba_sim.cc deleted file mode 100644 index 4a3af77c6..000000000 --- a/src/tgbaalgos/reductgba_sim.cc +++ /dev/null @@ -1,57 +0,0 @@ -// -*- coding: utf-8 -*- -// Copyright (C) 2009, 2011, 2012, 2013 Laboratoire de Recherche et -// Développement de l'Epita (LRDE). -// Copyright (C) 2004, 2005, 2007 Laboratoire d'Informatique de -// Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), -// Université Pierre et Marie Curie. -// -// This file is part of Spot, a model checking library. -// -// Spot is free software; you can redistribute it and/or modify it -// under the terms of the GNU General Public License as published by -// the Free Software Foundation; either version 3 of the License, or -// (at your option) any later version. -// -// Spot is distributed in the hope that it will be useful, but WITHOUT -// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY -// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public -// License for more details. -// -// You should have received a copy of the GNU General Public License -// along with this program. If not, see . - -#define SKIP_DEPRECATED_WARNING -#include "reductgba_sim.hh" -#include "sccfilter.hh" -#include "simulation.hh" -#include "dupexp.hh" - -namespace spot -{ - const tgba* - reduc_tgba_sim(const tgba* f, int opt) - { - if (opt & Reduce_Scc) - { - f = scc_filter(f); - - // No more reduction requested? Return the automaton as-is. - if (opt == Reduce_Scc) - return f; - } - - if (opt & (Reduce_quotient_Dir_Sim | Reduce_transition_Dir_Sim - | Reduce_quotient_Del_Sim | Reduce_transition_Del_Sim)) - { - tgba* res = simulation(f); - - if (opt & Reduce_Scc) - delete f; - - return res; - } - - return tgba_dupexp_dfs(f); - } - -} diff --git a/src/tgbaalgos/reductgba_sim.hh b/src/tgbaalgos/reductgba_sim.hh deleted file mode 100644 index dff51bef8..000000000 --- a/src/tgbaalgos/reductgba_sim.hh +++ /dev/null @@ -1,85 +0,0 @@ -// -*- coding: utf-8 -*- -// Copyright (C) 2009, 2010, 2011, 2012, 2013 Laboratoire de Recherche et -// Développement de l'Epita (LRDE). -// Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6), -// département Systèmes Répartis Coopératifs (SRC), Université Pierre -// et Marie Curie. -// -// This file is part of Spot, a model checking library. -// -// Spot is free software; you can redistribute it and/or modify it -// under the terms of the GNU General Public License as published by -// the Free Software Foundation; either version 3 of the License, or -// (at your option) any later version. -// -// Spot is distributed in the hope that it will be useful, but WITHOUT -// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY -// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public -// License for more details. -// -// You should have received a copy of the GNU General Public License -// along with this program. If not, see . - - -#ifndef SPOT_TGBAALGOS_REDUCTGBA_SIM_HH -#define SPOT_TGBAALGOS_REDUCTGBA_SIM_HH - -#if __GNUC__ -#ifndef SKIP_DEPRECATED_WARNING -#warning This file is deprecated. Use postproc.hh instead. -#endif -#endif - -#include "misc/common.hh" - -namespace spot -{ - class tgba; - - /// \addtogroup tgba_reduction - /// @{ - - /// Options for reduce. - enum reduce_tgba_options - { - // Reduce_None and Reduce_All clash with the definitions in ltl::reduce - // for Swig because Swig does not handle namespaces. -#ifndef SWIG - /// No reduction. - Reduce_None = 0, -#endif - /// Reduction of state using direct simulation relation. - Reduce_quotient_Dir_Sim = 1, - /// Reduction of transitions using direct simulation relation. - Reduce_transition_Dir_Sim = 2, - /// Reduction of state using delayed simulation relation. - Reduce_quotient_Del_Sim = 4, - /// Reduction of transition using delayed simulation relation. - Reduce_transition_Del_Sim = 8, - /// Reduction using SCC. - Reduce_Scc = 16, -#ifndef SWIG - /// All reductions. - Reduce_All = -1U -#endif - }; - - /// \brief Simplify the automaton using a simulation relation. - /// - /// Do not use this obsolete function. - /// - /// \param a the automata to reduce - /// \param opt a conjonction of spot::reduce_tgba_options specifying - /// which optimizations to apply. Actually any - /// simulation-related flag will cause direct simulation - /// to be applied. - /// \return the reduced automaton - /// \deprecated Use scc_filter(), minimize_wdba(), simulation(), - /// or postprocessor. - SPOT_API SPOT_DEPRECATED - const tgba* reduc_tgba_sim(const tgba* a, int opt = Reduce_All); - - /// @} -} - -#endif // SPOT_TGBAALGOS_REDUCTGBA_SIM_HH diff --git a/src/tgbaalgos/sccfilter.cc b/src/tgbaalgos/sccfilter.cc index 1c7b74ace..4c9c63f99 100644 --- a/src/tgbaalgos/sccfilter.cc +++ b/src/tgbaalgos/sccfilter.cc @@ -17,7 +17,6 @@ // You should have received a copy of the GNU General Public License // along with this program. If not, see . -#include "tgba/tgbaexplicit.hh" #include "sccfilter.hh" #include "reachiter.hh" #include "scc.hh" @@ -31,492 +30,6 @@ namespace spot typedef std::map accremap_t; typedef std::vector remap_table_t; - static - state_explicit_number::transition* - create_transition(const tgba*, tgba_explicit_number* out_aut, - const state*, int in, const state*, int out) - { - return out_aut->create_transition(in, out); - } - - static - state_explicit_string::transition* - create_transition(const tgba* aut, tgba_explicit_string* out_aut, - const state* in_s, int, const state* out_s, int) - { - const tgba_explicit_string* a = - static_cast(aut); - return out_aut->create_transition(a->get_label(in_s), - a->get_label(out_s)); - } - - static - state_explicit_formula::transition* - create_transition(const tgba* aut, tgba_explicit_formula* out_aut, - const state* in_s, int, const state* out_s, int) - { - const tgba_explicit_formula* a = - static_cast(aut); - const ltl::formula* in_f = a->get_label(in_s); - const ltl::formula* out_f = a->get_label(out_s); - if (!out_aut->has_state(in_f)) - in_f->clone(); - if ((in_f != out_f) && !out_aut->has_state(out_f)) - out_f->clone(); - return out_aut->create_transition(in_f, out_f); - } - - template - class filter_iter_states: public tgba_reachable_iterator_depth_first - { - public: - typedef T output_t; - - filter_iter_states(const tgba* a, - const scc_map& sm, - const std::vector& useless) - : tgba_reachable_iterator_depth_first(a), - out_(new T(a->get_dict())), - sm_(sm), - useless_(useless) - { - a->get_dict()->register_all_variables_of(a, out_); - out_->set_acceptance_conditions(a->all_acceptance_conditions()); - } - - T* - result() - { - return out_; - } - - bool - want_state(const state* s) const - { - return !useless_[sm_.scc_of_state(s)]; - } - - void - process_link(const state* in_s, int in, - const state* out_s, int out, - const tgba_succ_iterator* si) - { - typename output_t::state::transition* t = - create_transition(this->aut_, out_, in_s, in, out_s, out); - t->condition = si->current_condition(); - t->acceptance_conditions = si->current_acceptance_conditions(); - } - - protected: - T* out_; - const scc_map& sm_; - const std::vector& useless_; - }; - - template - class filter_iter: public tgba_reachable_iterator_depth_first - { - public: - typedef T output_t; - typedef std::map map_t; - typedef std::vector remap_t; - - filter_iter(const tgba* a, - const scc_map& sm, - const std::vector& useless, - remap_table_t& remap_table, - unsigned max_num, - bool remove_all_useless) - : tgba_reachable_iterator_depth_first(a), - out_(new T(a->get_dict())), - sm_(sm), - useless_(useless), - all_(remove_all_useless), - acc_(max_num) - { - acc_[0] = bddfalse; - bdd tmp = a->all_acceptance_conditions(); - bdd_dict* d = a->get_dict(); - assert(a->number_of_acceptance_conditions() >= max_num - 1); - if (tmp != bddfalse) - { - for (unsigned n = max_num - 1; n > 0; --n) - { - assert(tmp != bddfalse); - const ltl::formula* a = d->oneacc_to_formula(bdd_var(tmp)); - out_->declare_acceptance_condition(a->clone()); - tmp = bdd_low(tmp); - } - tmp = a->all_acceptance_conditions(); - for (unsigned n = max_num - 1; n > 0; --n) - { - const ltl::formula* a = d->oneacc_to_formula(bdd_var(tmp)); - acc_[n] = out_->get_acceptance_condition(a->clone()); - tmp = bdd_low(tmp); - } - } - else - { - assert(max_num == 1); - } - - unsigned c = sm.scc_count(); - remap_.resize(c); - bdd all_orig_neg = aut_->neg_acceptance_conditions(); - bdd all_sup = bdd_support(all_orig_neg); - - for (unsigned n = 0; n < c; ++n) - { - //std::cerr << "SCC #" << n << '\n'; - if (!sm.accepting(n)) - continue; - - bdd all = sm.useful_acc_of(n); - while (all != bddfalse) - { - bdd one = bdd_satoneset(all, all_sup, bddtrue); - all -= one; - bdd res = bddfalse; - bdd resacc = bddfalse; - while (one != bddtrue) - { - if (bdd_high(one) == bddfalse) - { - one = bdd_low(one); - continue; - } - int vn = bdd_var(one); - bdd v = bdd_ithvar(vn); - resacc |= bdd_exist(all_orig_neg, v) & v; - res |= acc_[remap_table[n][vn]]; - one = bdd_high(one); - } - int id = resacc.id(); - //std::cerr << resacc << " -> " << res << '\n'; - remap_[n][id] = res; - } - } - } - - T* - result() - { - return out_; - } - - bool - want_state(const state* s) const - { - return !useless_[sm_.scc_of_state(s)]; - } - - void - process_link(const state* in_s, int in, - const state* out_s, int out, - const tgba_succ_iterator* si) - { - typename output_t::state::transition* t = - create_transition(this->aut_, out_, in_s, in, out_s, out); - out_->add_conditions(t, si->current_condition()); - - // Regardless of all_, do not output any acceptance condition - // if the destination is not in an accepting SCC. - // - // If all_ is set, do not output any acceptance condition if the - // source is not in the same SCC as dest. - // - // (See the documentation of scc_filter() for a rational.) - unsigned u = sm_.scc_of_state(out_s); - unsigned v = sm_.scc_of_state(in_s); - if (sm_.accepting(u) && (!all_ || u == v)) - { - bdd acc = si->current_acceptance_conditions(); - if (acc == bddfalse) - return; - map_t::const_iterator i = this->remap_[u].find(acc.id()); - if (i != this->remap_[u].end()) - { - t->acceptance_conditions = i->second; - } - else - { - //t->acceptance_conditions = this->remap_[v][acc.id()]; - } - } - } - - protected: - T* out_; - const scc_map& sm_; - const std::vector& useless_; - bool all_; - std::vector acc_; - remap_t remap_; - }; - - } // anonymous - - - tgba* scc_filter(const tgba* aut, bool remove_all_useless, - scc_map* given_sm) - { - scc_map* sm = given_sm; - if (!sm) - { - sm = new scc_map(aut); - sm->build_map(); - } - scc_stats ss = build_scc_stats(*sm); - - remap_table_t remap_table(ss.scc_total); - std::vector max_table(ss.scc_total); - std::vector useful_table(ss.scc_total); - std::vector useless_table(ss.scc_total); - unsigned max_num = 1; - - for (unsigned n = 0; n < ss.scc_total; ++n) - { - if (!sm->accepting(n)) - continue; - bdd all = sm->useful_acc_of(n); - bdd negall = aut->neg_acceptance_conditions(); - - //std::cerr << "SCC #" << n << "; used = " << all << std::endl; - - // Compute a set of useless acceptance sets. - // If the acceptance combinations occurring in - // the automata are { a, ab, abc, bd }, then - // ALL contains (a&!b&!c&!d)|(a&b&!c&!d)|(a&b&c&!d)|(!a&b&!c&d) - // and we want to find that 'a' and 'b' are useless because - // they always occur with 'c'. - // The way we check if 'a' is useless is to look whether ALL - // implies (x -> a) for some other acceptance set x. - // - // The two while() loops in the code perform the equivalent of - // for all a in allconds_a: - // for all x in allconds_x: - // check whether x -> a - // ... - // - // Initially allconds_a = allconds_x contains all acceptance - // sets. However when an acceptance set 'a' is determined to - // be useless, it can be removed from allconds_x from future - // iterations. - bdd allconds_a = bdd_support(negall); - bdd allconds_x = allconds_a; - bdd useless = bddtrue; - while (allconds_a != bddtrue) - { - // Speed-up the computation of implied acceptance sets by - // removing those that are always present. We detect - // those that appear as conjunction of positive variables - // at the start of ALL. - bdd prefix = bdd_satprefix(all); - if (prefix != bddtrue) - { - assert(prefix == bdd_support(prefix)); - allconds_a = bdd_exist(allconds_a, prefix); - if (allconds_a != bddtrue) - { - useless &= prefix; - } - else - { - // Never erase all conditions: at least keep one. - useless &= bdd_high(prefix); - break; - } - allconds_x = bdd_exist(allconds_x, prefix); - } - - // Pick an acceptance set 'a'. - bdd a = bdd_ithvar(bdd_var(allconds_a)); - // For all acceptance sets 'x' that are not already - // useless... - bdd others = allconds_x; - while (others != bddtrue) - { - bdd x = bdd_ithvar(bdd_var(others)); - // ... check whether 'x' always implies 'a'. - if (x != a && bdd_implies(all, x >> a)) - { - // If so, 'a' is useless. - all = bdd_exist(all, a); - useless &= a; - allconds_x = bdd_exist(allconds_x, a); - break; - } - others = bdd_high(others); - } - allconds_a = bdd_high(allconds_a); - } - - // We never remove ALL acceptance marks. - assert(negall == bddtrue || useless != bdd_support(negall)); - - useless_table[n] = useless; - bdd useful = bdd_exist(negall, useless); - - //std::cerr << "SCC #" << n << "; useful = " << useful << std::endl; - - // Go over all useful sets of acceptance marks, and give them - // a number. - unsigned num = 1; - // First compute the number of acceptance conditions used. - for (BDD c = useful.id(); c != 1; c = bdd_low(c)) - ++num; - max_table[n] = num; - if (num > max_num) - max_num = num; - - useful_table[n] = useful; - } - - // Now that we know about the max number of acceptance conditions, - // use add extra acceptance conditions to those SCC that do not - // have enough. - for (unsigned n = 0; n < ss.scc_total; ++n) - { - if (!sm->accepting(n)) - continue; - //std::cerr << "SCC " << n << '\n'; - bdd useful = useful_table[n]; - - int missing = max_num - max_table[n]; - bdd useless = useless_table[n]; - while (missing--) - { - //std::cerr << useful << " : " << useless << std::endl; - useful &= bdd_nithvar(bdd_var(useless)); - useless = bdd_high(useless); - } - int num = max_num; - // Then number all of these acceptance conditions in the - // reverse order. This makes sure that the associated number - // varies in the same direction as the bdd variables, which in - // turn makes sure we preserve the acceptance condition - // ordering (which matters for degeneralization). - for (BDD c = useful.id(); c != 1; c = bdd_low(c)) - remap_table[n].emplace(bdd_var(c), --num); - - max_table[n] = max_num; - } - - tgba* ret; - // In most cases we will create a tgba_explicit_string copy of the - // initial tgba, but this is not very space efficient as the - // labels are built using the "format_state()" string output of - // the original automaton. In the case where the source automaton is - // a tgba_explicit_formula (typically after calling ltl2tgba_fm()) - // we can create another tgba_explicit_formula instead. - const tgba_explicit_formula* af = - dynamic_cast(aut); - if (af) - { - filter_iter fi(af, *sm, - ss.useless_scc_map, - remap_table, max_num, - remove_all_useless); - fi.run(); - tgba_explicit_formula* res = fi.result(); - res->merge_transitions(); - ret = res; - } - else - { - const tgba_explicit_string* as = - dynamic_cast(aut); - if (as) - { - filter_iter fi(aut, *sm, ss.useless_scc_map, - remap_table, max_num, - remove_all_useless); - fi.run(); - tgba_explicit_string* res = fi.result(); - res->merge_transitions(); - ret = res; - } - else - { - filter_iter fi(aut, *sm, - ss.useless_scc_map, - remap_table, max_num, - remove_all_useless); - fi.run(); - tgba_explicit_number* res = fi.result(); - res->merge_transitions(); - ret = res; - } - } - if (!given_sm) - delete sm; - return ret; - } - - tgba* scc_filter_states(const tgba* aut, scc_map* given_sm) - { - const tgba_digraph* autg = dynamic_cast(aut); - if (autg && !given_sm) - return scc_filter_states(autg, nullptr); - - scc_map* sm = given_sm; - if (!sm) - { - sm = new scc_map(aut); - sm->build_map(); - } - scc_stats ss = build_scc_stats(*sm); - - tgba* ret; - - const tgba_explicit_formula* af = - dynamic_cast(aut); - if (af) - { - filter_iter_states fi(af, *sm, - ss.useless_scc_map); - fi.run(); - tgba_explicit_formula* res = fi.result(); - res->merge_transitions(); - ret = res; - } - else - { - const tgba_explicit_string* as = - dynamic_cast(aut); - if (as) - { - filter_iter_states fi(aut, *sm, - ss.useless_scc_map); - fi.run(); - tgba_explicit_string* res = fi.result(); - res->merge_transitions(); - ret = res; - } - else - { - filter_iter_states fi(aut, *sm, - ss.useless_scc_map); - fi.run(); - tgba_explicit_number* res = fi.result(); - res->merge_transitions(); - ret = res; - } - } - if (!given_sm) - delete sm; - return ret; - } - - - ////////////////////////////////////////////////////////////////////// - // The goal is to remove all the code above this line eventually, so - // do not waste your time code common to both sides of this note. - ////////////////////////////////////////////////////////////////////// - - namespace - { - typedef std::tuple filtered_trans; typedef std::pair acc_pair; diff --git a/src/tgbaalgos/sccfilter.hh b/src/tgbaalgos/sccfilter.hh index 08bc6730a..b4bfb5858 100644 --- a/src/tgbaalgos/sccfilter.hh +++ b/src/tgbaalgos/sccfilter.hh @@ -60,15 +60,9 @@ namespace spot /// (i.e., transitions leaving accepting states are all marked as /// accepting) may destroy this property. Use scc_filter_states() /// instead. - /// @{ - SPOT_API tgba* - scc_filter(const tgba* aut, bool remove_all_useless = false, - scc_map* given_sm = 0); - SPOT_API tgba_digraph* scc_filter(const tgba_digraph* aut, bool remove_all_useless = false, scc_info* given_si = 0); - /// @} /// \brief Prune unaccepting SCCs. /// @@ -78,10 +72,6 @@ namespace spot /// Especially, if the input TGBA has the SBA property, (i.e., /// transitions leaving accepting states are all marked as /// accepting), then the output TGBA will also have that property. - /// @{ - SPOT_API tgba* - scc_filter_states(const tgba* aut, scc_map* given_sm = 0); - SPOT_API tgba_digraph* scc_filter_states(const tgba_digraph* aut, scc_info* given_si = 0); @@ -99,7 +89,6 @@ namespace spot scc_filter_susp(const tgba_digraph* aut, bool remove_all_useless, bdd suspvars, bdd ignoredvars, bool early_susp, scc_info* given_si = 0); - /// @} } #endif // SPOT_TGBAALGOS_SCC_HH diff --git a/src/tgbaalgos/simulation.cc b/src/tgbaalgos/simulation.cc index 3f1d775bf..d8053c496 100644 --- a/src/tgbaalgos/simulation.cc +++ b/src/tgbaalgos/simulation.cc @@ -22,7 +22,6 @@ #include #include #include -#include "tgba/tgbaexplicit.hh" #include "simulation.hh" #include "priv/acccompl.hh" #include "misc/minato.hh" diff --git a/src/tgbatest/Makefile.am b/src/tgbatest/Makefile.am index ceb195e8b..dd375089a 100644 --- a/src/tgbatest/Makefile.am +++ b/src/tgbatest/Makefile.am @@ -33,9 +33,6 @@ check_SCRIPTS = defs check_PROGRAMS = \ bitvect \ complement \ - explicit \ - explicit2 \ - explicit3 \ expldot \ explprod \ intvcomp \ @@ -51,9 +48,6 @@ check_PROGRAMS = \ # Keep this sorted alphabetically. bitvect_SOURCES = bitvect.cc complement_SOURCES = complementation.cc -explicit_SOURCES = explicit.cc -explicit2_SOURCES = explicit2.cc -explicit3_SOURCES = explicit3.cc expldot_SOURCES = powerset.cc expldot_CXXFLAGS = -DDOTTY explprod_SOURCES = explprod.cc @@ -74,8 +68,6 @@ tripprod_SOURCES = tripprod.cc TESTS = \ intvcomp.test \ bitvect.test \ - explicit.test \ - explicit2.test \ ltlcross3.test \ taatgba.test \ tgbaread.test \ diff --git a/src/tgbatest/explicit.cc b/src/tgbatest/explicit.cc deleted file mode 100644 index b9a49d527..000000000 --- a/src/tgbatest/explicit.cc +++ /dev/null @@ -1,61 +0,0 @@ -// Copyright (C) 2009 Laboratoire de Recherche et Développement -// de l'Epita (LRDE). -// 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. -// -// This file is part of Spot, a model checking library. -// -// Spot is free software; you can redistribute it and/or modify it -// under the terms of the GNU General Public License as published by -// the Free Software Foundation; either version 3 of the License, or -// (at your option) any later version. -// -// Spot is distributed in the hope that it will be useful, but WITHOUT -// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY -// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public -// License for more details. -// -// You should have received a copy of the GNU General Public License -// along with this program. If not, see . - -#include -#include -#include "ltlenv/defaultenv.hh" -#include "tgba/tgbaexplicit.hh" -#include "tgbaalgos/dotty.hh" -#include "ltlast/allnodes.hh" - -int -main() -{ - spot::bdd_dict* dict = new spot::bdd_dict(); - - spot::ltl::default_environment& e = - spot::ltl::default_environment::instance(); - spot::tgba_explicit_string* a = new spot::tgba_explicit_string(dict); - - typedef spot::state_explicit_string::transition trans; - - trans* t1 = a->create_transition("state 0", "state 1"); - trans* t2 = a->create_transition("state 1", "state 2"); - trans* t3 = a->create_transition("state 2", "state 0"); - a->add_condition(t2, e.require("a")); - a->add_condition(t3, e.require("b")); - a->add_condition(t3, e.require("c")); - a->declare_acceptance_condition(e.require("p")); - a->declare_acceptance_condition(e.require("q")); - a->declare_acceptance_condition(e.require("r")); - a->add_acceptance_condition(t1, e.require("p")); - a->add_acceptance_condition(t1, e.require("q")); - a->add_acceptance_condition(t2, e.require("r")); - - spot::dotty_reachable(std::cout, a); - - delete a; - delete dict; - assert(spot::ltl::atomic_prop::instance_count() == 0); - assert(spot::ltl::unop::instance_count() == 0); - assert(spot::ltl::binop::instance_count() == 0); - assert(spot::ltl::multop::instance_count() == 0); -} diff --git a/src/tgbatest/explicit.test b/src/tgbatest/explicit.test deleted file mode 100755 index 2626c1bf8..000000000 --- a/src/tgbatest/explicit.test +++ /dev/null @@ -1,45 +0,0 @@ -#!/bin/sh -# Copyright (C) 2008, 2009, 2013 Laboratoire de Recherche et Développement -# de l'Epita (LRDE). -# Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de -# Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), -# Université Pierre et Marie Curie. -# -# This file is part of Spot, a model checking library. -# -# Spot is free software; you can redistribute it and/or modify it -# under the terms of the GNU General Public License as published by -# the Free Software Foundation; either version 3 of the License, or -# (at your option) any later version. -# -# Spot is distributed in the hope that it will be useful, but WITHOUT -# ANY WARRANTY; without even the implied warranty of MERCHANTABILITY -# or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public -# License for more details. -# -# You should have received a copy of the GNU General Public License -# along with this program. If not, see . - - -. ./defs - -set -e - -run 0 ../explicit > stdout - -cat >expected < 1 - 1 [label="state 0"] - 1 -> 2 [label="1\n{Acc[q], Acc[p]}"] - 2 [label="state 1"] - 2 -> 3 [label="a\n{Acc[r]}"] - 3 [label="state 2"] - 3 -> 1 [label="b & c\n"] -} -EOF - -diff stdout expected - -rm stdout expected diff --git a/src/tgbatest/explicit2.cc b/src/tgbatest/explicit2.cc deleted file mode 100644 index 17b882f5c..000000000 --- a/src/tgbatest/explicit2.cc +++ /dev/null @@ -1,200 +0,0 @@ -// -*- coding: utf-8 -*- -// Copyright (C) 2012, 2014 Laboratoire de Recherche et Développement -// de l'Epita (LRDE). -// -// This file is part of Spot, a model checking library. -// -// Spot is free software; you can redistribute it and/or modify it -// under the terms of the GNU General Public License as published by -// the Free Software Foundation; either version 3 of the License, or -// (at your option) any later version. -// -// Spot is distributed in the hope that it will be useful, but WITHOUT -// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY -// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public -// License for more details. -// -// You should have received a copy of the GNU General Public License -// along with this program. If not, see . - -#include -#include - -#include "ltlenv/defaultenv.hh" -#include "ltlast/allnodes.hh" -#include "ltlvisit/tostring.hh" - -#include "tgba/tgbaexplicit.hh" - -using namespace spot; - -void -create_tgba_explicit_string(bdd_dict* d) -{ - tgba_explicit* tgba = - new tgba_explicit(d); - state_explicit_string* s1 = tgba->add_state("toto"); - state_explicit_string* s2 = tgba->add_state("tata"); - state_explicit_string::transition* t = - tgba->create_transition(s1, s2); - (void) t; - - for (auto it: tgba->succ(tgba->get_init_state())) - { - state_explicit_string* se = - down_cast(it->current_state()); - std::cout << se->label() << std::endl; - se->destroy(); - } - delete tgba; -} - -void -create_tgba_explicit_number(bdd_dict* d) -{ - tgba_explicit* tgba = - new tgba_explicit(d); - - state_explicit_number* s1 = tgba->add_state(51); - state_explicit_number* s2 = tgba->add_state(69); - state_explicit_number::transition* t = - tgba->create_transition(s1, s2); - (void) t; - - for (auto it: tgba->succ(tgba->get_init_state())) - { - state_explicit_number* s = - down_cast(it->current_state()); - std::cout << s->label() << std::endl; - s->destroy(); - } - delete tgba; -} - -void -create_tgba_explicit_formula(bdd_dict* d, spot::ltl::default_environment& e) -{ - tgba_explicit* tgba = - new tgba_explicit(d); - - state_explicit_formula* s1 = tgba->add_state(e.require("a")); - state_explicit_formula* s2 = tgba->add_state(e.require("b")); - - state_explicit_formula::transition* t = - tgba->create_transition(s1, s2); - (void) t; - - for (auto it: tgba->succ(tgba->get_init_state())) - { - state_explicit_formula* s = - down_cast(it->current_state()); - to_string(s->label(), std::cout) << std::endl; - s->destroy(); - } - delete tgba; -} - -void create_sba_explicit_string(bdd_dict* d) -{ - sba_explicit* sba = - new sba_explicit(d); - - ltl::formula* acc = ltl::constant::true_instance(); - sba->declare_acceptance_condition(acc); - - state_explicit_string* s1 = sba->add_state("STATE1"); - state_explicit_string* s2 = sba->add_state("STATE2"); - state_explicit_string* s3 = sba->add_state("STATE3"); - - state_explicit_string::transition* t = - sba->create_transition(s1, s2); - sba->add_acceptance_condition(t, acc); - - t = sba->create_transition(s1, s3); - sba->add_acceptance_condition(t, acc); - - std::cout << "S1 ACCEPTING? " << sba->state_is_accepting(s1) << std::endl; - std::cout << "S2 ACCEPTING? " << sba->state_is_accepting(s2) << std::endl; - std::cout << "S3 ACCEPTING? " << sba->state_is_accepting(s3) << std::endl; - - delete sba; -} - -void create_sba_explicit_number(bdd_dict* d) -{ - sba_explicit* sba = - new sba_explicit(d); - - ltl::formula* acc = ltl::constant::true_instance(); - sba->declare_acceptance_condition(acc); - - state_explicit_number* s1 = sba->add_state(1); - state_explicit_number* s2 = sba->add_state(2); - - state_explicit_number::transition* t = sba->create_transition(s1, s2); - sba->add_acceptance_condition(t, acc); - - std::cout << "S1 ACCEPTING? " << sba->state_is_accepting(s1) << std::endl; - std::cout << "S2 ACCEPTING? " << sba->state_is_accepting(s2) << std::endl; - - delete sba; -} - -void -create_sba_explicit_formula(bdd_dict* d, spot::ltl::default_environment& e) -{ - sba_explicit* sba = - new sba_explicit(d); - - ltl::formula* acc = ltl::constant::true_instance(); - sba->declare_acceptance_condition(acc); - - state_explicit_formula* s1 = sba->add_state(e.require("a")); - state_explicit_formula* s2 = sba->add_state(e.require("b")); - state_explicit_formula* s3 = sba->add_state(e.require("c")); - - state_explicit_formula::transition* t = sba->create_transition(s1, s2); - sba->add_acceptance_condition(t, acc); - - t = sba->create_transition(s1, s3); - sba->add_acceptance_condition(t, acc); - - std::cout << "S1 ACCEPTING? " << sba->state_is_accepting(s1) << std::endl; - std::cout << "S2 ACCEPTING? " << sba->state_is_accepting(s2) << std::endl; - std::cout << "S3 ACCEPTING? " << sba->state_is_accepting(s3) << std::endl; - - delete sba; -} - -int -main(int argc, char** argv) -{ - (void) argc; - (void) argv; - - bdd_dict* d = new spot::bdd_dict(); - spot::ltl::default_environment& e = - spot::ltl::default_environment::instance(); - - //check tgba creation - std::cout << "* TGBA explicit string" << std::endl; - create_tgba_explicit_string(d); - std::cout << "* TGBA explicit number" << std::endl; - create_tgba_explicit_number(d); - std::cout << "* TGBA explicit formula" << std::endl; - create_tgba_explicit_formula(d, e); - - //check sba creation - std::cout << "* SBA explicit string, 1 accepting state" << std::endl; - create_sba_explicit_string(d); - std::cout << "* SBA explicit number, 1 accepting state" << std::endl; - create_sba_explicit_number(d); - std::cout << "* SBA explicit formula, 1 accepting state" << std::endl; - create_sba_explicit_formula(d, e); - - delete d; - assert(spot::ltl::atomic_prop::instance_count() == 0); - assert(spot::ltl::unop::instance_count() == 0); - assert(spot::ltl::binop::instance_count() == 0); - assert(spot::ltl::multop::instance_count() == 0); -} diff --git a/src/tgbatest/explicit2.test b/src/tgbatest/explicit2.test deleted file mode 100755 index 6025a84f9..000000000 --- a/src/tgbatest/explicit2.test +++ /dev/null @@ -1,46 +0,0 @@ -#!/bin/sh -# Copyright (C) 2012 Laboratoire de Recherche et Développement -# de l'Epita (LRDE). -# -# This file is part of Spot, a model checking library. -# -# Spot is free software; you can redistribute it and/or modify it -# under the terms of the GNU General Public License as published by -# the Free Software Foundation; either version 3 of the License, or -# (at your option) any later version. -# -# Spot is distributed in the hope that it will be useful, but WITHOUT -# ANY WARRANTY; without even the implied warranty of MERCHANTABILITY -# or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public -# License for more details. -# -# You should have received a copy of the GNU General Public License -# along with this program. If not, see . - -. ./defs - -set -e - -run 0 ../explicit2 >stdout -cat stdout -cat >expected <. - -#include -#include -#include "ltlenv/defaultenv.hh" -#include "tgba/tgbaexplicit.hh" -#include "tgbaalgos/dotty.hh" -#include "ltlast/allnodes.hh" -#include "tgba/tgbamask.hh" - -int -main() -{ - spot::ltl::default_environment& e = - spot::ltl::default_environment::instance(); - - const spot::ltl::formula* a = e.require("a"); - const spot::ltl::formula* b = e.require("b"); - const spot::ltl::formula* c = e.require("c"); - - spot::bdd_dict* dict = new spot::bdd_dict(); - spot::tgba_explicit_number* aut = new spot::tgba_explicit_number(dict); - - typedef spot::state_explicit_number::transition trans; - - { - trans* t = aut->create_transition(0, 1); - aut->add_condition(t, a->clone()); - } - { - trans* t = aut->create_transition(1, 2); - aut->add_condition(t, a->clone()); - } - { - trans* t = aut->create_transition(2, 0); - aut->add_condition(t, a->clone()); - } - { - trans* t = aut->create_transition(1, 3); - aut->add_condition(t, b->clone()); - } - { - trans* t = aut->create_transition(3, 4); - aut->add_condition(t, c->clone()); - } - { - trans* t = aut->create_transition(4, 3); - aut->add_condition(t, c->clone()); - aut->declare_acceptance_condition(b->clone()); - aut->add_acceptance_condition(t, b->clone()); - } - - a->destroy(); - b->destroy(); - c->destroy(); - - spot::dotty_reachable(std::cout, aut); - - spot::state_set s; - s.insert(aut->get_state(0)); - s.insert(aut->get_state(1)); - s.insert(aut->get_state(2)); - - const spot::tgba* mk = build_tgba_mask_keep(aut, s); - spot::dotty_reachable(std::cout, mk); - delete mk; - - const spot::tgba* mi = build_tgba_mask_ignore(aut, s); - spot::dotty_reachable(std::cout, mi); - delete mi; - - const spot::tgba* mi2 = build_tgba_mask_ignore(aut, s, aut->get_state(1)); - spot::dotty_reachable(std::cout, mi2); - delete mi2; - - delete aut; - delete dict; - assert(spot::ltl::atomic_prop::instance_count() == 0); - assert(spot::ltl::unop::instance_count() == 0); - assert(spot::ltl::binop::instance_count() == 0); - assert(spot::ltl::multop::instance_count() == 0); -} diff --git a/src/tgbatest/explicit3.test b/src/tgbatest/explicit3.test deleted file mode 100755 index 8d92a7792..000000000 --- a/src/tgbatest/explicit3.test +++ /dev/null @@ -1,68 +0,0 @@ -#!/bin/sh -# Copyright (C) 2013 Laboratoire de Recherche et Développement -# de l'Epita (LRDE). -# -# This file is part of Spot, a model checking library. -# -# Spot is free software; you can redistribute it and/or modify it -# under the terms of the GNU General Public License as published by -# the Free Software Foundation; either version 3 of the License, or -# (at your option) any later version. -# -# Spot is distributed in the hope that it will be useful, but WITHOUT -# ANY WARRANTY; without even the implied warranty of MERCHANTABILITY -# or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public -# License for more details. -# -# You should have received a copy of the GNU General Public License -# along with this program. If not, see . - -. ./defs - -set -e - -run 0 ../explicit3 | tee stdout -cat >expected < 1 - 1 [label="0"] - 1 -> 2 [label="a\n"] - 2 [label="1"] - 2 -> 3 [label="a\n"] - 2 -> 4 [label="b\n"] - 3 [label="2"] - 3 -> 1 [label="a\n"] - 4 [label="3"] - 4 -> 5 [label="c\n"] - 5 [label="4"] - 5 -> 4 [label="c\n{Acc[b]}"] -} -digraph G { - 0 [label="", style=invis, height=0] - 0 -> 1 - 1 [label="0"] - 1 -> 2 [label="a\n"] - 2 [label="1"] - 2 -> 3 [label="a\n"] - 3 [label="2"] - 3 -> 1 [label="a\n"] -} -digraph G { - 0 [label="", style=invis, height=0] - 0 -> 1 - 1 [label="0"] -} -digraph G { - 0 [label="", style=invis, height=0] - 0 -> 1 - 1 [label="1"] - 1 -> 2 [label="b\n"] - 2 [label="3"] - 2 -> 3 [label="c\n"] - 3 [label="4"] - 3 -> 2 [label="c\n{Acc[b]}"] -} -EOF - -cmp expected stdout diff --git a/src/tgbatest/explprod.cc b/src/tgbatest/explprod.cc index 560a69bbc..0215bfcbc 100644 --- a/src/tgbatest/explprod.cc +++ b/src/tgbatest/explprod.cc @@ -23,7 +23,6 @@ #include #include #include -#include "tgba/tgbaexplicit.hh" #include "tgba/tgbaproduct.hh" #include "tgbaparse/public.hh" #include "tgbaalgos/save.hh" diff --git a/src/tgbatest/ltl2tgba.cc b/src/tgbatest/ltl2tgba.cc index d70ac48ca..815473602 100644 --- a/src/tgbatest/ltl2tgba.cc +++ b/src/tgbatest/ltl2tgba.cc @@ -1301,10 +1301,19 @@ main(int argc, char** argv) if (scc_filter && (reduction_dir_sim || reduction_rev_sim)) { + auto aa = dynamic_cast(a); + bool freeit = false; + if (!aa) + { + freeit = true; + aa = spot::tgba_dupexp_dfs(a); + } tm.start("SCC-filter post-sim"); delete aut_scc; - aut_scc = a = spot::scc_filter(a, scc_filter_all); + aut_scc = a = spot::scc_filter(aa, scc_filter_all); tm.stop("SCC-filter post-sim"); + if (freeit) + delete aa; } if (reduction_dont_care_sim) diff --git a/src/tgbatest/powerset.cc b/src/tgbatest/powerset.cc index 5f9bcb931..667c4f6f5 100644 --- a/src/tgbatest/powerset.cc +++ b/src/tgbatest/powerset.cc @@ -23,7 +23,6 @@ #include #include #include -#include "tgba/tgbaexplicit.hh" #include "tgbaalgos/powerset.hh" #include "tgbaparse/public.hh" #include "tgbaalgos/save.hh" diff --git a/src/tgbatest/tgbaread.cc b/src/tgbatest/tgbaread.cc index ab9194c71..6706d0a7d 100644 --- a/src/tgbatest/tgbaread.cc +++ b/src/tgbatest/tgbaread.cc @@ -25,7 +25,6 @@ #include #include #include "tgbaparse/public.hh" -#include "tgba/tgbaexplicit.hh" #include "tgbaalgos/dotty.hh" #include "ltlast/allnodes.hh" diff --git a/src/tgbatest/tripprod.cc b/src/tgbatest/tripprod.cc index ca419997d..a712078f2 100644 --- a/src/tgbatest/tripprod.cc +++ b/src/tgbatest/tripprod.cc @@ -23,7 +23,6 @@ #include #include #include -#include "tgba/tgbaexplicit.hh" #include "tgba/tgbaproduct.hh" #include "tgbaparse/public.hh" #include "tgbaalgos/save.hh" diff --git a/wrap/python/ajax/spot.in b/wrap/python/ajax/spot.in index 588634c03..4c784c0d3 100755 --- a/wrap/python/ajax/spot.in +++ b/wrap/python/ajax/spot.in @@ -700,9 +700,6 @@ if degen or neverclaim: else: degen = automaton -if utf8: - spot.tgba_enable_utf8(degen) - # Buchi Automaton Output if output_type == 'a': if buchi_type == 'i': diff --git a/wrap/python/spot.i b/wrap/python/spot.i index 296945255..6750052e3 100644 --- a/wrap/python/spot.i +++ b/wrap/python/spot.i @@ -79,7 +79,6 @@ namespace std { #include "tgba/tgba.hh" #include "tgba/sba.hh" #include "tgba/taatgba.hh" -#include "tgba/tgbaexplicit.hh" #include "tgba/tgbaproduct.hh" #include "tgba/tgbatba.hh" @@ -221,7 +220,6 @@ using namespace spot; %include "tgba/tgba.hh" %include "tgba/sba.hh" %include "tgba/taatgba.hh" -%include "tgba/tgbaexplicit.hh" %include "tgba/tgbaproduct.hh" %include "tgba/tgbatba.hh" @@ -233,61 +231,6 @@ namespace spot { }; } -%template(tgba_explicit_succ_iterator__string) - spot::tgba_explicit_succ_iterator; -%template(tgba_explicit_succ_iterator__number) - spot::tgba_explicit_succ_iterator; -%template(tgba_explicit_succ_iterator__formula) - spot::tgba_explicit_succ_iterator; - -%template(explicit_graph__string_tgba) - spot::explicit_graph; -%template(explicit_graph__number_tgba) - spot::explicit_graph; -%template(explicit_graph__formula_tgba) - spot::explicit_graph; - -%template(explicit_string_tgba) - spot::tgba_explicit; -%template(explicit_number_tgba) - spot::tgba_explicit; -%template(explicit_formula_tgba) - spot::tgba_explicit; - -%template(explicit_string__tgba) - spot::explicit_conf, - state_explicit_string>; -%template(explicit_number__tgba) - spot::explicit_conf, - state_explicit_number>; -%template(explicit_formula__tgba) - spot::explicit_conf, - state_explicit_formula>; - -%template(explicit_graph__string_sba) - spot::explicit_graph; -%template(explicit_graph__number_sba) - spot::explicit_graph; -%template(explicit_graph__formula_sba) - spot::explicit_graph; - -%template(explicit_string_sba) - spot::sba_explicit; -%template(explicit_number_sba) - spot::sba_explicit; -%template(explicit_formula_sba) - spot::sba_explicit; - -%template(explicit_string__sba) - spot::explicit_conf, - state_explicit_string>; -%template(explicit_number__sba) - spot::explicit_conf, - state_explicit_number>; -%template(explicit_formula__sba) - spot::explicit_conf, - state_explicit_formula>; - %include "tgbaalgos/degen.hh" %include "tgbaalgos/dottydec.hh" %include "tgbaalgos/dotty.hh" @@ -399,17 +342,6 @@ minimize_obligation_new(const spot::tgba* a, const spot::ltl::formula* f) return res; } -void -tgba_enable_utf8(spot::tgba* a) -{ - if (spot::tgba_explicit_formula* tef = - dynamic_cast(a)) - tef->enable_utf8(); - else if (spot::sba_explicit_formula* sef = - dynamic_cast(a)) - sef->enable_utf8(); -} - spot::ltl::parse_error_list empty_parse_error_list() {