diff --git a/NEWS b/NEWS index 128f772f2..6fbf74d19 100644 --- a/NEWS +++ b/NEWS @@ -119,6 +119,9 @@ New in spot 1.99a (not yet released) has been removed too, because it was only used by the KV complementation. + - The unused implementation of state-based alternating Büchi automata + has been removed. + New in spot 1.2.5a (not yet released) * New features: diff --git a/README b/README index a14f3f698..e3abbbac7 100644 --- a/README +++ b/README @@ -166,9 +166,6 @@ src/ Sources for libspot. ta/ TA objects and cousins (TGTA). taalgos/ Algorithms on TA/TGTA. tgbatest/ Tests for tgba/, tgbaalgos/, tgbaparse/, ta/ and taalgos/. - saba/ SABA (State-labeled Alternating Büchi Automata) objects. - sabaalgos/ Algorithms on SABA. - sabatest/ Tests for saba/, sabaalgos/. sanity/ Sanity tests for the whole project. doc/ Documentation for libspot. org/ Source of userdoc/ as org-mode files. diff --git a/configure.ac b/configure.ac index 725428436..af3609d40 100644 --- a/configure.ac +++ b/configure.ac @@ -193,10 +193,6 @@ AC_CONFIG_FILES([ src/neverparse/Makefile src/priv/Makefile src/sanity/Makefile - src/saba/Makefile - src/sabaalgos/Makefile - src/sabatest/defs - src/sabatest/Makefile src/tgbaalgos/gtec/Makefile src/tgbaalgos/Makefile src/tgba/Makefile diff --git a/src/Makefile.am b/src/Makefile.am index 8b19c1a5d..25cc70fc9 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -26,9 +26,9 @@ AUTOMAKE_OPTIONS = subdir-objects # end, after building '.' (since the current directory contains # libspot.la needed by the tests) SUBDIRS = misc priv ltlenv ltlast ltlvisit ltlparse graph tgba \ - tgbaalgos tgbaparse ta taalgos kripke saba sabaalgos \ - neverparse kripkeparse dstarparse . bin ltltest graphtest \ - tgbatest sabatest kripketest sanity + tgbaalgos tgbaparse ta taalgos kripke neverparse \ + kripkeparse dstarparse . bin ltltest graphtest tgbatest \ + kripketest sanity lib_LTLIBRARIES = libspot.la libspot_la_SOURCES = @@ -44,8 +44,6 @@ libspot_la_LIBADD = \ misc/libmisc.la \ neverparse/libneverparse.la \ priv/libpriv.la \ - sabaalgos/libsabaalgos.la \ - saba/libsaba.la \ taalgos/libtaalgos.la \ ta/libta.la \ tgbaalgos/libtgbaalgos.la \ diff --git a/src/saba/Makefile.am b/src/saba/Makefile.am deleted file mode 100644 index f5fd0c665..000000000 --- a/src/saba/Makefile.am +++ /dev/null @@ -1,36 +0,0 @@ -## -*- coding: utf-8 -*- -## Copyright (C) 2009, 2011, 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 . - -AM_CPPFLAGS = -I$(srcdir)/.. -I.. $(BUDDY_CPPFLAGS) -AM_CXXFLAGS = $(WARNING_CXXFLAGS) - -sabadir = $(pkgincludedir)/saba - -saba_HEADERS = \ - explicitstateconjunction.hh \ - saba.hh \ - sabastate.hh \ - sabasucciter.hh \ - sabacomplementtgba.hh - -noinst_LTLIBRARIES = libsaba.la -libsaba_la_SOURCES = \ - explicitstateconjunction.cc \ - saba.cc \ - sabacomplementtgba.cc diff --git a/src/saba/explicitstateconjunction.cc b/src/saba/explicitstateconjunction.cc deleted file mode 100644 index 191ec4196..000000000 --- a/src/saba/explicitstateconjunction.cc +++ /dev/null @@ -1,89 +0,0 @@ -// -*- coding: utf-8 -*- -// Copyright (C) 2009, 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 "explicitstateconjunction.hh" - -namespace spot -{ - - /// explicit_state_conjunction - //////////////////////////////////////// - - explicit_state_conjunction::explicit_state_conjunction() - { - } - - explicit_state_conjunction:: - explicit_state_conjunction(const explicit_state_conjunction* other) - : set_(other->set_) - { - } - - explicit_state_conjunction& - explicit_state_conjunction::operator=(const explicit_state_conjunction& o) - { - if (this != &o) - { - this->~explicit_state_conjunction(); - new (this) explicit_state_conjunction(&o); - } - return *this; - } - - explicit_state_conjunction::~explicit_state_conjunction() - { - } - - void - explicit_state_conjunction::first() - { - it_ = set_.begin(); - } - - void - explicit_state_conjunction::next() - { - ++it_; - } - - bool - explicit_state_conjunction::done() const - { - return it_ == set_.end(); - } - - explicit_state_conjunction* - explicit_state_conjunction::clone() const - { - return new explicit_state_conjunction(this); - } - - saba_state* - explicit_state_conjunction::current_state() const - { - return (*it_)->clone(); - } - - void - explicit_state_conjunction::add(saba_state* state) - { - set_.insert(shared_saba_state(state)); - } - -} // end namespace spot. diff --git a/src/saba/explicitstateconjunction.hh b/src/saba/explicitstateconjunction.hh deleted file mode 100644 index ed0c36e79..000000000 --- a/src/saba/explicitstateconjunction.hh +++ /dev/null @@ -1,78 +0,0 @@ -// -*- coding: utf-8 -*- -// Copyright (C) 2009, 2012, 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 . - -#ifndef SPOT_SABA_EXPLICITSTATECONJUNCTION_HH -# define SPOT_SABA_EXPLICITSTATECONJUNCTION_HH - -#include "misc/common.hh" -#include "misc/hash.hh" -#include "sabasucciter.hh" - -namespace spot -{ - /// \ingroup saba_essentials - /// \brief Basic implementation of saba_state_conjunction. - /// - /// This class provides a basic implementation to - /// iterate over a conjunction of states of a saba. - class SPOT_API explicit_state_conjunction : public saba_state_conjunction - { - public: - - explicit_state_conjunction(); - explicit_state_conjunction(const explicit_state_conjunction* other); - virtual ~explicit_state_conjunction(); - - explicit_state_conjunction& operator=(const explicit_state_conjunction& o); - - /// \name Iteration - //@{ - - virtual void first(); - virtual void next(); - virtual bool done() const; - - //@} - - /// \name Inspection - //@{ - - /// Duplicate a this conjunction. - explicit_state_conjunction* clone() const; - - /// Return the a new instance on the current state. - /// This is the caller responsibility to delete the returned state. - virtual saba_state* current_state() const; - - //@} - - /// Add a new state in the conjunction. - /// The class becomes owner of \a state. - void add(saba_state* state); - private: - typedef std::unordered_set saba_state_set_t; - saba_state_set_t set_; - saba_state_set_t::iterator it_; - }; -} // end namespace spot. - - -#endif // SPOT_SABA_EXPLICITSTATECONJUNCTION_HH diff --git a/src/saba/saba.cc b/src/saba/saba.cc deleted file mode 100644 index 2b9a67f65..000000000 --- a/src/saba/saba.cc +++ /dev/null @@ -1,49 +0,0 @@ -// Copyright (C) 2009 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 "saba.hh" - -namespace spot -{ - saba::saba() - : num_acc_(-1) - { - } - - saba::~saba() - { - } - - unsigned int - saba::number_of_acceptance_conditions() const - { - if (num_acc_ < 0) - { - bdd all = all_acceptance_conditions(); - unsigned int n = 0; - while (all != bddfalse) - { - ++n; - all -= bdd_satone(all); - } - num_acc_ = n; - } - return num_acc_; - } - -} // end namespace spot. diff --git a/src/saba/saba.hh b/src/saba/saba.hh deleted file mode 100644 index 7a9f235e8..000000000 --- a/src/saba/saba.hh +++ /dev/null @@ -1,118 +0,0 @@ -// -*- coding: utf-8 -*- -// Copyright (C) 2009, 2010, 2013, 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 . - -#ifndef SPOT_SABA_SABA_HH -# define SPOT_SABA_SABA_HH - -#include "sabastate.hh" -#include "sabasucciter.hh" -#include - -namespace spot -{ - /// \defgroup saba SABA (State-based Alternating Büchi Automata) - /// - /// Spot was centered around non-deterministic \ref tgba. - /// Alternating automata are an extension to non-deterministic - /// automata, and are presented with spot::saba. - /// This type and its cousins are listed \ref saba_essentials "here". - /// This is an abstract interface. - - /// \addtogroup saba_essentials Essential SABA types - /// \ingroup saba - - /// \ingroup saba_essentials - /// \brief A State-based Alternating (Generalized) Büchi Automaton. - /// - /// Browsing such automaton can be achieved using two functions: - /// \c get_init_state, and \c succ_iter. The former returns - /// the initial state while the latter lists the - /// successor states of any state. - /// - /// Note that although this is a transition-based automata, - /// we never represent transitions! Transition informations are - /// obtained by querying the iterator over the successors of - /// a state. - class SPOT_API saba - { - protected: - saba(); - - public: - virtual ~saba(); - - /// \brief Get the initial state of the automaton. - /// - /// The state has been allocated with \c new. It is the - /// responsability of the caller to \c delete it when no - /// longer needed. - virtual saba_state* get_init_state() const = 0; - - /// \brief Get an iterator over the successors of \a local_state. - /// - /// The iterator has been allocated with \c new. It is the - /// responsability of the caller to \c delete it when no - /// longer needed. - /// - /// \param local_state The state whose successors are to be explored. - /// This pointer is not adopted in any way by \c succ_iter, and - /// it is still the caller's responsability to delete it when - /// appropriate (this can be done during the lifetime of - /// the iterator). - virtual saba_succ_iterator* - succ_iter(const saba_state* local_state) const = 0; - - /// \brief Get the dictionary associated to the automaton. - /// - /// State are represented as BDDs. The dictionary allows - /// to map BDD variables back to formulae, and vice versa. - /// This is useful when dealing with several automata (which - /// may use the same BDD variable for different formula), - /// or simply when printing. - virtual bdd_dict_ptr get_dict() const = 0; - - /// \brief Format the state as a string for printing. - /// - /// This formating is the responsability of the automata - /// that owns the state. - virtual std::string format_state(const saba_state* state) const = 0; - - /// \brief Return the set of all acceptance conditions used - /// by this automaton. - /// - /// The goal of the emptiness check is to ensure that - /// a strongly connected component walks through each - /// of these acceptiong conditions. I.e., the union - /// of the acceptiong conditions of all transition in - /// the SCC should be equal to the result of this function. - virtual bdd all_acceptance_conditions() const = 0; - - /// The number of acceptance conditions. - virtual unsigned int number_of_acceptance_conditions() const; - private: - mutable int num_acc_; - }; - - typedef std::shared_ptr saba_ptr; - typedef std::shared_ptr const_saba_ptr; - -} // end namespace spot. - - -#endif // SPOT_SABA_SABA_HH diff --git a/src/saba/sabacomplementtgba.cc b/src/saba/sabacomplementtgba.cc deleted file mode 100644 index 46e513079..000000000 --- a/src/saba/sabacomplementtgba.cc +++ /dev/null @@ -1,445 +0,0 @@ -// -*- coding: utf-8 -*- -// Copyright (C) 2009, 2010, 2011, 2012, 2013, 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 -#include "bdd.h" -#include "tgba/bddprint.hh" -#include "tgba/tgba.hh" -#include "misc/hash.hh" -#include "misc/bddlt.hh" -#include "tgbaalgos/degen.hh" -#include "tgbaalgos/bfssteps.hh" -#include "misc/hashfunc.hh" -#include "ltlast/formula.hh" -#include "ltlast/constant.hh" -#include "priv/countstates.hh" - -#include "sabacomplementtgba.hh" -#include "explicitstateconjunction.hh" - -namespace spot -{ - namespace - { - - // typedefs. - typedef int rank_t; - - //////////////////////////////////////// - // saba_state_complement_tgba - - /// States used by spot::saba_complement_tgba. - /// A state gather a spot::state* and a rank. - /// \ingroup saba_representation - class saba_state_complement_tgba : public saba_state - { - public: - saba_state_complement_tgba(); - saba_state_complement_tgba(const saba_state_complement_tgba* state_taa); - saba_state_complement_tgba(shared_state state, rank_t rank, - bdd condition); - virtual ~saba_state_complement_tgba() {} - - virtual int compare(const saba_state* other) const; - virtual size_t hash() const; - virtual saba_state_complement_tgba* clone() const; - - virtual bdd acceptance_conditions() const; - const state* get_state() const; - rank_t get_rank() const; - private: - shared_state state_; - rank_t rank_; - bdd condition_; - }; - - saba_state_complement_tgba::saba_state_complement_tgba(shared_state state, - rank_t rank, - bdd condition) - : state_(state), rank_(rank), condition_(condition) - { - } - - saba_state_complement_tgba:: - saba_state_complement_tgba(const saba_state_complement_tgba* state_taa) - : state_(state_taa->state_), rank_(state_taa->rank_), - condition_(state_taa->condition_) - { - } - - int - saba_state_complement_tgba::compare(const saba_state* o) const - { - const saba_state_complement_tgba* other = - dynamic_cast(o); - - int compare_value = get_state()->compare(other->get_state()); - if (compare_value != 0) - return compare_value; - - if (get_rank() != other->get_rank()) - return get_rank() - other->get_rank(); - - return acceptance_conditions().id() - - other->acceptance_conditions().id(); - } - - size_t - saba_state_complement_tgba::hash() const - { - size_t hash = get_state()->hash() ^ wang32_hash(get_rank()); - hash ^= wang32_hash(acceptance_conditions().id()); - return hash; - } - - saba_state_complement_tgba* - saba_state_complement_tgba::clone() const - { - return new saba_state_complement_tgba(*this); - } - - bdd - saba_state_complement_tgba::acceptance_conditions() const - { - if ((get_rank() & 1) == 1) - return condition_; - else - return bddfalse; - } - - const state* - saba_state_complement_tgba::get_state() const - { - return state_.get(); - } - - rank_t - saba_state_complement_tgba::get_rank() const - { - return rank_; - } - - - /// Successor iterators used by spot::saba_complement_tgba. - /// \ingroup saba_representation - /// - /// Since the algorithm works on-the-fly, the key components of the - /// algorithm are implemented in this class. - /// - class saba_complement_tgba_succ_iterator: public saba_succ_iterator - { - public: - typedef std::list state_conjunction_list_t; - typedef std::map - bdd_list_t; - - saba_complement_tgba_succ_iterator(const const_tgba_digraph_ptr& - automaton, - bdd the_acceptance_cond, - const saba_state_complement_tgba* - origin); - virtual ~saba_complement_tgba_succ_iterator(); - - virtual void first(); - virtual void next(); - virtual bool done() const; - virtual saba_state_conjunction* current_conjunction() const; - virtual bdd current_condition() const; - private: - void get_atomics(std::set& list, bdd c); - void get_conj_list(); - void state_conjunction(); - void delete_condition_list(); - - const_tgba_digraph_ptr automaton_; - bdd the_acceptance_cond_; - const saba_state_complement_tgba* origin_; - bdd_list_t condition_list_; - bdd_list_t::const_iterator current_condition_; - state_conjunction_list_t::const_iterator current_conjunction_; - state_conjunction_list_t::const_iterator current_end_conjunction_; - }; - - saba_complement_tgba_succ_iterator:: - saba_complement_tgba_succ_iterator(const const_tgba_digraph_ptr& automaton, - bdd the_acceptance_cond, - const saba_state_complement_tgba* origin) - : automaton_(automaton), the_acceptance_cond_(the_acceptance_cond), - origin_(origin) - { - assert(automaton->is_sba()); - // If state not accepting or rank is even - if (((origin_->get_rank() & 1) == 0) || - !automaton_->state_is_accepting(origin_->get_state())) - { - get_conj_list(); - state_conjunction(); - } - } - - saba_complement_tgba_succ_iterator:: - ~saba_complement_tgba_succ_iterator() - { - delete_condition_list(); - } - - void - saba_complement_tgba_succ_iterator::state_conjunction() - { - int max_rank = origin_->get_rank(); - - for (bdd_list_t::iterator it = condition_list_.begin(); - it != condition_list_.end(); - ++it) - { - // Get successors states. - bdd condition = it->first; - std::vector state_list; - for (auto iterator: automaton_->succ(origin_->get_state())) - { - bdd c = iterator->current_condition(); - if ((c & condition) != bddfalse) - state_list.push_back(shared_state(iterator->current_state(), - shared_state_deleter)); - } - - // Make the conjunction with ranks. - std::vector current_ranks(state_list.size(), max_rank); - - if (state_list.empty()) - return; - - do - { - explicit_state_conjunction* conj = new explicit_state_conjunction(); - for (unsigned i = 0; i < state_list.size(); ++i) - { - conj->add(new saba_state_complement_tgba(state_list[i], - current_ranks[i], - the_acceptance_cond_)); - } - it->second.push_back(conj); - - if (current_ranks[0] <= 0) - break; - - unsigned order = state_list.size() - 1; - while (current_ranks[order] == 0) - { - current_ranks[order] = max_rank; - --order; - } - --current_ranks[order]; - } - while (1); - } - } - - /// Insert in \a list atomic properties of the formula \a c. - void - saba_complement_tgba_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; - } - } - - /// Free the conjunctions in the condition map. - void - saba_complement_tgba_succ_iterator::delete_condition_list() - { - for (bdd_list_t::iterator i = condition_list_.begin(); - i != condition_list_.end(); - ++i) - { - for (state_conjunction_list_t::iterator j = i->second.begin(); - j != i->second.end(); - ++j) - delete *j; - } - condition_list_.clear(); - } - - /// Create the conjunction of all the atomic properties from - /// the successors of the current state. - void - saba_complement_tgba_succ_iterator::get_conj_list() - { - std::set atomics; - delete_condition_list(); - - for (auto iterator: automaton_->succ(origin_->get_state())) - { - bdd c = iterator->current_condition(); - get_atomics(atomics, c); - } - - // 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_[result] = state_conjunction_list_t(); - } - } - - void - saba_complement_tgba_succ_iterator::first() - { - current_condition_ = condition_list_.begin(); - if (current_condition_ != condition_list_.end()) - { - current_conjunction_ = current_condition_->second.begin(); - current_end_conjunction_ = current_condition_->second.end(); - } - } - - void - saba_complement_tgba_succ_iterator::next() - { - if (++current_conjunction_ == current_end_conjunction_) - { - ++current_condition_; - if (current_condition_ != condition_list_.end()) - { - current_conjunction_ = current_condition_->second.begin(); - current_end_conjunction_ = current_condition_->second.end(); - } - } - } - - bool - saba_complement_tgba_succ_iterator::done() const - { - return (current_condition_ == condition_list_.end()); - } - - saba_state_conjunction* - saba_complement_tgba_succ_iterator::current_conjunction() const - { - return (*current_conjunction_)->clone(); - } - - bdd - saba_complement_tgba_succ_iterator::current_condition() const - { - return current_condition_->first; - } - - } // end namespace anonymous. - - saba_complement_tgba::saba_complement_tgba(const const_tgba_ptr& a) - : automaton_(degeneralize(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); - nb_states_ = automaton_->num_states(); - } - - saba_complement_tgba::~saba_complement_tgba() - { - get_dict()->unregister_all_my_variables(this); - } - - saba_state* - saba_complement_tgba::get_init_state() const - { - state* original_init_state = automaton_->get_init_state(); - saba_state_complement_tgba* new_init; - if (automaton_->state_is_accepting(original_init_state)) - new_init = - new saba_state_complement_tgba(shared_state(original_init_state, - shared_state_deleter), - 2 * nb_states_, - the_acceptance_cond_); - else - new_init = - new saba_state_complement_tgba(shared_state(original_init_state, - shared_state_deleter), - 2 * nb_states_, - bddfalse); - - return new_init; - } - - saba_succ_iterator* - saba_complement_tgba::succ_iter(const saba_state* local_state) const - { - const saba_state_complement_tgba* state = - dynamic_cast(local_state); - assert(state); - - return new saba_complement_tgba_succ_iterator(automaton_, - the_acceptance_cond_, - state); - } - - bdd_dict_ptr - saba_complement_tgba::get_dict() const - { - return automaton_->get_dict(); - } - - std::string - saba_complement_tgba::format_state(const saba_state* state) const - { - const saba_state_complement_tgba* s = - dynamic_cast(state); - assert(s); - std::ostringstream ss; - ss << "{ original: " << automaton_->format_state(s->get_state()) - << "\n rank: " << s->get_rank() - << "\n acc: " << bdd_format_accset(get_dict(), - s->acceptance_conditions()) - << " }"; - return ss.str(); - } - - bdd - saba_complement_tgba::all_acceptance_conditions() const - { - return the_acceptance_cond_; - } - -} // end namespace spot. diff --git a/src/saba/sabacomplementtgba.hh b/src/saba/sabacomplementtgba.hh deleted file mode 100644 index 27c750cf4..000000000 --- a/src/saba/sabacomplementtgba.hh +++ /dev/null @@ -1,85 +0,0 @@ -// Copyright (C) 2009, 2010, 2013, 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 . - -#ifndef SPOT_SABA_SABACOMPLEMENTTGBA_HH -#define SPOT_SABA_SABACOMPLEMENTTGBA_HH - -#include "tgba/fwd.hh" -#include "saba.hh" - -namespace spot -{ - /// \ingroup saba - /// \brief Complement a TGBA and produce a SABA. - /// - /// The original TGBA is transformed into a States-based - /// Büchi Automaton. - /// - /// Several techniques are supposed to by applied on the resulting - /// automaton before its transformation into a TGBA. Those techniques - /// are expected to reduce the size of the automaton. - /// - /// This algorithm comes from: - /** \verbatim - @Article{ gurumurthy.03.lncs, - title = {On complementing nondeterministic {B\"uchi} automata}, - author = {Gurumurthy, S. and Kupferman, O. and Somenzi, F. and - Vardi, M.Y.}, - journal = {Lecture Notes in Computer Science}, - pages = {96--110}, - year = {2003}, - publisher = {Springer-Verlag} - } - \endverbatim */ - /// - /// The construction is done on-the-fly, by the - /// \c saba_complement_succ_iterator class. - /// \see saba_complement_succ_iterator - class SPOT_API saba_complement_tgba : public saba - { - public: - saba_complement_tgba(const const_tgba_ptr& a); - virtual ~saba_complement_tgba(); - - // tgba interface - virtual saba_state* get_init_state() const; - virtual saba_succ_iterator* - succ_iter(const saba_state* local_state) const; - - virtual bdd_dict_ptr get_dict() const; - virtual std::string format_state(const saba_state* state) const; - virtual bdd all_acceptance_conditions() const; - private: - const_tgba_digraph_ptr automaton_; - bdd the_acceptance_cond_; - unsigned nb_states_; - }; // end class tgba_saba_complement. - - typedef std::shared_ptr saba_complement_tgba_ptr; - typedef std::shared_ptr - const_saba_complement_tgba_ptr; - inline saba_complement_tgba_ptr make_saba_complement(const const_tgba_ptr& a) - { - return std::make_shared(a); - } - - -} // end namespace spot. - - -#endif // SPOT_SABA_SABACOMPLEMENTTGBA_HH diff --git a/src/saba/sabastate.hh b/src/saba/sabastate.hh deleted file mode 100644 index 83012bc6d..000000000 --- a/src/saba/sabastate.hh +++ /dev/null @@ -1,247 +0,0 @@ -// -*- coding: utf-8 -*- -// Copyright (C) 2009, 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 . - -#ifndef SPOT_SABA_SABASTATE_HH -# define SPOT_SABA_SABASTATE_HH - -#include "misc/common.hh" -#include -#include -#include -#include - -namespace spot -{ - - /// \ingroup saba_essentials - /// \brief Abstract class for saba states. - class SPOT_API saba_state - { - public: - /// \brief Compares two states (that come from the same automaton). - /// - /// This method returns an integer less than, equal to, or greater - /// than zero if \a this is found, respectively, to be less than, equal - /// to, or greater than \a other according to some implicit total order. - /// - /// This method should not be called to compare states from - /// different automata. - /// - /// \sa spot::saba_state_ptr_less_than - virtual int compare(const saba_state* other) const = 0; - - /// \brief Hash a state. - /// - /// This method returns an integer that can be used as a - /// hash value for this state. - /// - /// Note that the hash value is guaranteed to be unique for all - /// equal states (in compare()'s sense) for only has long has one - /// of these states exists. So it's OK to use a spot::saba_state - /// as a key in an \c unordered_map because the mere use of the - /// state as a key in the hash will ensure the state continues to - /// exist. - /// - /// However if you create the state, get its hash key, delete the - /// state, recreate the same state, and get its hash key, you may - /// obtain two different hash keys if the same state were not - /// already used elsewhere. In practice this weird situation can - /// occur only when the state is BDD-encoded, because BDD numbers - /// (used to build the hash value) can be reused for other - /// formulas. That probably doesn't matter, since the hash value - /// is meant to be used in an \c unordered_map, but it had to be noted. - virtual size_t hash() const = 0; - - /// Duplicate a state. - virtual saba_state* clone() const = 0; - - /// \brief Get the acceptance condition. - /// - /// saba are state-labeled automata, then their acceptance conditions - /// are labeled on states. - virtual bdd acceptance_conditions() const = 0; - - virtual ~saba_state() - { - } - }; - - /// \ingroup saba_essentials - /// \brief Strict Weak Ordering for \c saba_state*. - /// - /// This is meant to be used as a comparison functor for - /// STL \c map whose key are of type \c saba_state*. - /// - /// For instance here is how one could declare - /// a map of \c saba_state*. - /// \code - /// // Remember how many times each state has been visited. - /// std::map seen; - /// \endcode - struct saba_state_ptr_less_than: - public std::binary_function - { - bool - operator()(const saba_state* left, const saba_state* right) const - { - assert(left); - return left->compare(right) < 0; - } - }; - - /// \ingroup saba_essentials - /// \brief An Equivalence Relation for \c saba_state*. - /// - /// This is meant to be used as a comparison functor for - /// \c unordered_map whose keys are of type \c saba_state*. - /// - /// For instance here is how one could declare - /// a map of \c saba_state*. - /// \code - /// // Remember how many times each state has been visited. - /// std::unordered_map seen; - /// \endcode - struct saba_state_ptr_equal: - public std::binary_function - { - bool - operator()(const saba_state* left, const saba_state* right) const - { - assert(left); - return 0 == left->compare(right); - } - }; - - /// \ingroup saba_essentials - /// \ingroup hash_funcs - /// \brief Hash Function for \c saba_state*. - /// - /// This is meant to be used as a hash functor for - /// an \c unordered_map whose keys are of type \c saba_state*. - /// - /// For instance here is how one could declare - /// a map of \c saba_state*. - /// \code - /// // Remember how many times each state has been visited. - /// std::unordered_map seen; - /// \endcode - struct saba_state_ptr_hash: - public std::unary_function - { - size_t - operator()(const saba_state* that) const - { - assert(that); - return that->hash(); - } - }; - - // Functions related to shared_ptr. - ////////////////////////////////////////////////// - - typedef std::shared_ptr shared_saba_state; - - /// \ingroup saba_essentials - /// \brief Strict Weak Ordering for \c shared_saba_state - /// (shared_ptr). - /// - /// This is meant to be used as a comparison functor for - /// STL \c map whose keys are of type \c shared_saba_state. - /// - /// For instance here is how one could declare - /// a map of \c shared_saba_state. - /// \code - /// // Remember how many times each state has been visited. - /// std::map - /// seen; - /// \endcode - struct saba_state_shared_ptr_less_than: - public std::binary_function - { - bool - operator()(shared_saba_state left, - shared_saba_state right) const - { - assert(left); - return left->compare(right.get()) < 0; - } - }; - - /// \ingroup saba_essentials - /// \brief An Equivalence Relation for \c shared_saba_state - /// (shared_ptr). - /// - /// This is meant to be used as a comparison functor for - /// an \c unordred_map whose keys are of type \c shared_saba_state. - /// - /// For instance here is how one could declare - /// a map of \c shared_saba_state - /// \code - /// // Remember how many times each state has been visited. - /// std::unordered_map seen; - /// \endcode - struct saba_state_shared_ptr_equal: - public std::binary_function - { - bool - operator()(shared_saba_state left, - shared_saba_state right) const - { - assert(left); - return 0 == left->compare(right.get()); - } - }; - - /// \ingroup saba_essentials - /// \ingroup hash_funcs - /// \brief Hash Function for \c shared_saba_state - /// (shared_ptr). - /// - /// This is meant to be used as a hash functor for - /// \c unordered_map whose key are of type - /// \c shared_saba_state. - /// - /// For instance here is how one could declare - /// a map of \c shared_saba_state. - /// \code - /// // Remember how many times each state has been visited. - /// std::unordered_map seen; - /// \endcode - struct saba_state_shared_ptr_hash: - public std::unary_function - { - size_t - operator()(shared_saba_state that) const - { - assert(that); - return that->hash(); - } - }; - -} - -#endif // SPOT_SABA_SABASTATE_HH diff --git a/src/saba/sabasucciter.hh b/src/saba/sabasucciter.hh deleted file mode 100644 index 9d18d2798..000000000 --- a/src/saba/sabasucciter.hh +++ /dev/null @@ -1,158 +0,0 @@ -// -*- coding: utf-8 -*- -// Copyright (C) 2009, 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 . - -#ifndef SPOT_SABA_SABASUCCITER_HH -# define SPOT_SABA_SABASUCCITER_HH - -#include "sabastate.hh" - -namespace spot -{ - /// \ingroup saba_essentials - /// \brief Iterate over a conjunction of saba_state. - /// - /// This class provides the basic functionalities required to - /// iterate over a conjunction of states of a saba. - class SPOT_API saba_state_conjunction - { - public: - virtual - ~saba_state_conjunction() - { - } - - /// \name Iteration - //@{ - - /// \brief Position the iterator on the first successor of the conjunction - /// (if any). - /// - /// This method can be called several times to make multiple - /// passes over successors. - /// - /// \warning One should always call \c done() to - /// ensure there is a successor, even after \c first(). A - /// common trap is to assume that there is at least one - /// successor: this is wrong. - virtual void first() = 0; - - /// \brief Jump to the next successor (if any). - /// - /// \warning Again, one should always call \c done() to ensure - /// there is a successor. - virtual void next() = 0; - - /// \brief Check whether the iteration over a conjunction of states - /// is finished. - /// - /// This function should be called after any call to \c first() - /// or \c next() and before any enquiry about the current state. - virtual bool done() const = 0; - - //@} - - /// \name Inspection - //@{ - - /// \brief Get the state of the current successor. - /// - /// Note that the same state may occur at different points - /// in the iteration. These actually correspond to the same - /// destination. It just means there were several transitions, - /// with different conditions, leading to the same state. - /// - /// \warning the state is allocated with new, its deletion is - /// the responsibility of the caller. - virtual saba_state* current_state() const = 0; - - //@} - - /// Duplicate a saba_state conjunction. - virtual saba_state_conjunction* clone() const = 0; - }; - - - /// \ingroup saba_essentials - /// \brief Iterate over the successors of a saba_state. - /// - /// This class provides the basic functionalities required to - /// iterate over the successors of a state of a saba. Since - /// transitions of an alternating automaton are defined as a - /// boolean function with conjunctions (universal) and - /// disjunctions (non-deterministic), - class SPOT_API saba_succ_iterator - { - public: - virtual - ~saba_succ_iterator() - { - } - - /// \name Iteration - //@{ - - /// \brief Position the iterator on the first conjunction - /// of successors (if any). - /// - /// This method can be called several times to make multiple - /// passes over successors. - /// - /// \warning One should always call \c done() to - /// ensure there is a successor, even after \c first(). A - /// common trap is to assume that there is at least one - /// successor: this is wrong. - virtual void first() = 0; - - /// \brief Jump to the next conjunction of successors (if any). - /// - /// \warning Again, one should always call \c done() to ensure - /// there is a successor. - virtual void next() = 0; - - /// \brief Check whether the iteration is finished. - /// - /// This function should be called after any call to \c first() - /// or \c next() and before any enquiry about the current state. - /// - /// The usual way to do this is with a \c for loop. - /// \code - /// for (s->first(); !s->done(); s->next()) - /// ... - /// \endcode - virtual bool done() const = 0; - - //@} - - /// \name Inspection - //@{ - - /// \brief Get current conjunction of successor states. - virtual saba_state_conjunction* current_conjunction() const = 0; - - /// \brief Get the condition on the transition leading to this successor. - /// - /// This is a boolean function of atomic propositions. - virtual bdd current_condition() const = 0; - - //@} - }; -} - - -#endif // SPOT_TGBA_SUCCITER_HH diff --git a/src/sabaalgos/Makefile.am b/src/sabaalgos/Makefile.am deleted file mode 100644 index 44907efde..000000000 --- a/src/sabaalgos/Makefile.am +++ /dev/null @@ -1,28 +0,0 @@ -## -*- coding: utf-8 -*- -## Copyright (C) 2009, 2011, 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 . - -AM_CPPFLAGS = -I$(srcdir)/.. -I.. $(BUDDY_CPPFLAGS) -AM_CXXFLAGS = $(WARNING_CXXFLAGS) - -sabaalgosdir = $(pkgincludedir)/sabaalgos - -sabaalgos_HEADERS = sabadotty.hh sabareachiter.hh - -noinst_LTLIBRARIES = libsabaalgos.la -libsabaalgos_la_SOURCES = sabadotty.cc sabareachiter.cc diff --git a/src/sabaalgos/sabadotty.cc b/src/sabaalgos/sabadotty.cc deleted file mode 100644 index 1222c1825..000000000 --- a/src/sabaalgos/sabadotty.cc +++ /dev/null @@ -1,105 +0,0 @@ -// -*- coding: utf-8 -*- -// Copyright (C) 2009, 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 "sabadotty.hh" -#include "tgba/bddprint.hh" -#include "sabareachiter.hh" -#include "misc/escape.hh" - -namespace spot -{ - namespace - { - class saba_dotty_bfs : public saba_reachable_iterator_breadth_first - { - public: - saba_dotty_bfs(std::ostream& os, const const_saba_ptr& a) - : saba_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 - end() - { - os_ << '}' << std::endl; - } - - void - process_state(const saba_state* s, int n) - { - std::string label = - escape_str(automata_->format_state(s)) - + "\\n" - + bdd_format_accset(automata_->get_dict(), - s->acceptance_conditions()); - os_ << " " << n << ' ' - << "[label=\"" << label << "\"];\n"; - } - - void - process_state_conjunction(const saba_state*, int in, - const saba_state_conjunction*, - int sc_id, - const saba_succ_iterator* si) - { - os_ << " s" << in << "sc" << sc_id - << " [label=\"\", style=invis, height=0];" << std::endl; - - std::string label = - bdd_format_formula(automata_->get_dict(), - si->current_condition()); - - os_ << " " << in << " -> s" << in << "sc" << sc_id - << " [label=\"" << label << "\", arrowhead=\"none\"];\n"; - } - - void - process_link(const saba_state*, int in, - const saba_state*, int out, - const saba_state_conjunction*, - int sc_id, - const saba_succ_iterator*) - { - os_ << " s" << in << "sc" << sc_id << " -> " << out - << " [label=\"\"];\n"; - } - - private: - std::ostream& os_; - }; - } - - std::ostream& - saba_dotty_reachable(std::ostream& os, const const_saba_ptr& g) - { - saba_dotty_bfs d(os, g); - d.run(); - return os; - } - -} diff --git a/src/sabaalgos/sabadotty.hh b/src/sabaalgos/sabadotty.hh deleted file mode 100644 index 55180d866..000000000 --- a/src/sabaalgos/sabadotty.hh +++ /dev/null @@ -1,36 +0,0 @@ -// -*- coding: utf-8 -*- -// Copyright (C) 2009, 2013, 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 . - -#ifndef SPOT_SABAALGOS_SABADOTTY_HH -# define SPOT_SABAALGOS_SABADOTTY_HH - -#include "misc/common.hh" -#include -#include "saba/saba.hh" - -namespace spot -{ - /// \ingroup saba_io - /// \brief Print reachable states in dot format. - SPOT_API std::ostream& - saba_dotty_reachable(std::ostream& os, - const const_saba_ptr& g); -} - -#endif // SPOT_SABAALGOS_SABADOTTY_HH diff --git a/src/sabaalgos/sabareachiter.cc b/src/sabaalgos/sabareachiter.cc deleted file mode 100644 index 4682ce1ab..000000000 --- a/src/sabaalgos/sabareachiter.cc +++ /dev/null @@ -1,187 +0,0 @@ -// -*- coding: utf-8 -*- -// Copyright (C) 2009, 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 "sabareachiter.hh" - -namespace spot -{ - // saba_reachable_iterator - ////////////////////////////////////////////////////////////////////// - - saba_reachable_iterator::saba_reachable_iterator(const const_saba_ptr& a) - : automata_(a) - { - } - - saba_reachable_iterator::~saba_reachable_iterator() - { - seen_map::const_iterator s = seen.begin(); - while (s != seen.end()) - { - // Advance the iterator before deleting the "key" pointer. - const saba_state* ptr = s->first; - ++s; - delete ptr; - } - } - - void - saba_reachable_iterator::run() - { - int n = 0; - int conjn = 0; - - start(); - saba_state* i = automata_->get_init_state(); - if (want_state(i)) - add_state(i); - seen[i] = ++n; - const saba_state* t; - while ((t = next_state())) - { - assert(seen.find(t) != seen.end()); - int tn = seen[t]; - saba_succ_iterator* si = automata_->succ_iter(t); - process_state(t, tn); - for (si->first(); !si->done(); si->next()) - { - saba_state_conjunction* conj = si->current_conjunction(); - ++conjn; - process_state_conjunction(t, tn, conj, conjn, si); - - for (conj->first(); !conj->done(); conj->next()) - { - const saba_state* current = conj->current_state(); - seen_map::const_iterator s = seen.find(current); - bool ws = want_state(current); - - if (s == seen.end()) - { - seen[current] = ++n; - if (ws) - { - add_state(current); - process_link(t, tn, current, n, conj, conjn, si); - } - } - else - { - if (ws) - process_link(t, tn, s->first, s->second, conj, conjn, si); - delete current; - } - } - delete conj; - } - delete si; - } - end(); - } - - bool - saba_reachable_iterator::want_state(const saba_state*) const - { - return true; - } - - void - saba_reachable_iterator::start() - { - } - - void - saba_reachable_iterator::end() - { - } - - void - saba_reachable_iterator::process_state(const saba_state*, int) - { - } - - void - saba_reachable_iterator:: - process_state_conjunction(const saba_state*, int, - const saba_state_conjunction*, - int, - const saba_succ_iterator*) - { - } - - void - saba_reachable_iterator::process_link(const saba_state*, int, - const saba_state*, int, - const saba_state_conjunction*, - int, - const saba_succ_iterator*) - { - } - - // saba_reachable_iterator_depth_first - ////////////////////////////////////////////////////////////////////// - - saba_reachable_iterator_depth_first:: - saba_reachable_iterator_depth_first(const const_saba_ptr& a) - : saba_reachable_iterator(a) - { - } - - void - saba_reachable_iterator_depth_first::add_state(const saba_state* s) - { - todo.push(s); - } - - const saba_state* - saba_reachable_iterator_depth_first::next_state() - { - if (todo.empty()) - return 0; - const saba_state* s = todo.top(); - todo.pop(); - return s; - } - - // saba_reachable_iterator_breadth_first - ////////////////////////////////////////////////////////////////////// - - saba_reachable_iterator_breadth_first:: - saba_reachable_iterator_breadth_first(const const_saba_ptr& a) - : saba_reachable_iterator(a) - { - } - - void - saba_reachable_iterator_breadth_first::add_state(const saba_state* s) - { - todo.push_back(s); - } - - const saba_state* - saba_reachable_iterator_breadth_first::next_state() - { - if (todo.empty()) - return 0; - const saba_state* s = todo.front(); - todo.pop_front(); - return s; - } - -} diff --git a/src/sabaalgos/sabareachiter.hh b/src/sabaalgos/sabareachiter.hh deleted file mode 100644 index d80b79b93..000000000 --- a/src/sabaalgos/sabareachiter.hh +++ /dev/null @@ -1,153 +0,0 @@ -// -*- coding: utf-8 -*- -// Copyright (C) 2009, 2010, 2013, 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 . - -#ifndef SPOT_SABAALGOS_SABAREACHITER_HH -# define SPOT_SABAALGOS_SABAREACHITER_HH - -#include "misc/hash.hh" -#include "saba/saba.hh" -#include -#include - -namespace spot -{ - /// \ingroup saba_generic - /// \brief Iterate over all reachable states of a spot::saba. - class SPOT_API saba_reachable_iterator - { - public: - saba_reachable_iterator(const const_saba_ptr& a); - virtual ~saba_reachable_iterator(); - - /// \brief Iterate over all reachable states of a spot::saba. - /// - /// This is a template method that will call add_state(), next_state(), - /// start(), end(), process_state(), process_state_conjunction() and - /// process_link(), while it iterates over states. - void run(); - - /// \name Todo list management. - /// - /// spot::saba_reachable_iterator_depth_first and - /// spot::saba_reachable_iterator_breadth_first offer two precanned - /// implementations for these functions. - /// \{ - /// \brief Called by run() to register newly discovered states. - virtual void add_state(const saba_state* s) = 0; - /// \brief Called by run() to obtain the next state to process. - virtual const saba_state* next_state() = 0; - /// \} - - /// Called by add_state or next_states implementations to filter - /// states. Default implementation always return true. - virtual bool want_state(const saba_state* s) const; - - /// Called by run() before starting its iteration. - virtual void start(); - /// Called by run() once all states have been explored. - virtual void end(); - - /// Called by run() to process a state. - /// - /// \param s The current state. - /// \param n A unique number assigned to \a s. - virtual void process_state(const saba_state* s, int n); - - /// Called by run() to process a conjunction of states. - /// - /// \param in_s The current state. - /// \param in An unique number assigned to \a in_s. - /// \param sc The spot::saba_state_conjunction positionned on the current - /// conjunction. - /// \param sc_id An unique number for the this transition assigned to \a sc. - /// \param si The spot::saba_succ_iterator positionned on the current - /// transition. - virtual void - process_state_conjunction(const saba_state* in_s, int in, - const saba_state_conjunction* sc, - int sc_id, - const saba_succ_iterator* si); - /// Called by run() to process a transition. - /// - /// \param in_s The source state - /// \param in The source state number. - /// \param out_s The destination state - /// \param out The destination state number. - /// \param sc The spot::saba_state_conjunction positionned on the current - /// conjunction. - /// \param sc_id An unique number for the this transition assigned to \a sc. - /// \param si The spot::saba_succ_iterator positionned on the current - /// transition. - /// - /// The in_s and out_s states are owned by the - /// spot::saba_reachable_iterator instance and destroyed when the - /// instance is destroyed. - virtual void - process_link(const saba_state* in_s, int in, - const saba_state* out_s, int out, - const saba_state_conjunction* sc, - int sc_id, - const saba_succ_iterator* si); - - protected: - const_saba_ptr automata_; ///< The spot::saba to explore. - - typedef - std::unordered_map seen_map; - seen_map seen; ///< States already seen. - }; - - /// \ingroup saba_generic - /// \brief An implementation of spot::saba_reachable_iterator that browses - /// states depth first. - class SPOT_API saba_reachable_iterator_depth_first: - public saba_reachable_iterator - { - public: - saba_reachable_iterator_depth_first(const const_saba_ptr& a); - - virtual void add_state(const saba_state* s); - virtual const saba_state* next_state(); - - protected: - std::stack todo; ///< A stack of states yet to explore. - }; - - /// \ingroup saba_generic - /// \brief An implementation of spot::saba_reachable_iterator that browses - /// states breadth first. - class SPOT_API saba_reachable_iterator_breadth_first: - public saba_reachable_iterator - { - public: - saba_reachable_iterator_breadth_first(const const_saba_ptr& a); - - virtual void add_state(const saba_state* s); - virtual const saba_state* next_state(); - - protected: - std::deque todo; ///< A queue of states yet to explore. - }; - - -} - - -#endif // SPOT_SABAALGOS_SABAREACHITER_HH diff --git a/src/sabatest/.gitignore b/src/sabatest/.gitignore deleted file mode 100644 index 411970693..000000000 --- a/src/sabatest/.gitignore +++ /dev/null @@ -1,2 +0,0 @@ -defs -sabacomplementtgba diff --git a/src/sabatest/Makefile.am b/src/sabatest/Makefile.am deleted file mode 100644 index c880dd040..000000000 --- a/src/sabatest/Makefile.am +++ /dev/null @@ -1,37 +0,0 @@ -## Copyright (C) 2009, 2011 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 . - -AM_CPPFLAGS = -I$(srcdir)/.. -I.. $(BUDDY_CPPFLAGS) -AM_CXXFLAGS = $(WARNING_CXXFLAGS) -LDADD = ../libspot.la - -# These are the most used test programs, and they are also useful -# to run manually outside the test suite. Always build them. -# noinst_PROGRAMS = - -check_SCRIPTS = defs -# Keep this sorted alphabetically. -check_PROGRAMS = \ - sabacomplementtgba - -# Keep this sorted alphabetically. -sabacomplementtgba_SOURCES = sabacomplementtgba.cc - -# Keep this sorted by STRENGTH. Test basic things first, -# because such failures will be easier to diagnose and fix. -# TESTS = diff --git a/src/sabatest/defs.in b/src/sabatest/defs.in deleted file mode 100644 index dc39be955..000000000 --- a/src/sabatest/defs.in +++ /dev/null @@ -1,87 +0,0 @@ -# -*- shell-script -*- -# Copyright (C) 2009 Laboratoire de Recherche et Développement -# de l'Epita (LRDE). -# 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 . - -# Ensure we are running from the right directory. -test -f ./defs || { - echo "defs: not found in current directory" 1>&2 - exit 1 -} - -# If srcdir is not set, then we are not running from `make check'. -if test -z "$srcdir"; then - # compute $srcdir. - srcdir=`echo "$0" | sed -e 's,/[^\\/]*$,,'` - test $srcdir = $0 && srcdir=. -fi - -# Ensure $srcdir is set correctly. -test -f $srcdir/defs.in || { - echo "$srcdir/defs.in not found, check \$srcdir" 1>&2 - exit 1 -} - -echo "== Running test $0" - -me=`echo "$0" | sed -e 's,.*[\\/],,;s/\.test$//'` - -testSubDir=$me.dir -chmod -R a+rwx $testSubDir > /dev/null 2>&1 -rm -rf $testSubDir > /dev/null 2>&1 -mkdir $testSubDir -cd $testSubDir - -# Adjust srcdir now that we are in a subdirectory. We still want to -# source directory corresponding to the build directory that contains -# $testSubDir. -case $srcdir in - # I - [\\/$]* | ?:[\\/]* );; - *) srcdir=../$srcdir -esac - -DOT='@DOT@' -top_builddir='../@top_builddir@' -LBTT="@LBTT@" -LBTT_TRANSLATE="@LBTT_TRANSLATE@" -VALGRIND='@VALGRIND@' - -run() -{ - expected_exitcode=$1 - shift - exitcode=0 - if test -n "$VALGRIND"; then - exec 6>valgrind.err - GLIBCPP_FORCE_NEW=1 \ - ../../../libtool --mode=execute \ - $VALGRIND --tool=memcheck --leak-check=yes --log-fd=6 -q "$@" || - exitcode=$? - cat valgrind.err 1>&2 - test -z "`sed 1q valgrind.err`" || exit 50 - rm -f valgrind.err - else - "$@" || exitcode=$? - fi - test $exitcode = $expected_exitcode || exit 1 -} - -set -x diff --git a/src/sabatest/sabacomplementtgba.cc b/src/sabatest/sabacomplementtgba.cc deleted file mode 100644 index 423df8493..000000000 --- a/src/sabatest/sabacomplementtgba.cc +++ /dev/null @@ -1,76 +0,0 @@ -// -*- coding: utf-8 -*- -// Copyright (C) 2009, 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 -#include -#include -#include -#include -#include -#include - -void usage(const std::string& argv0) -{ - std::cerr - << "usage " << argv0 << " [options]" << std::endl - << "options:" << std::endl - << "-f formula display the saba of !forumula" - << std::endl; -} - -int main(int argc, char* argv[]) -{ - std::string formula; - for (int i = 1; i < argc; ++i) - { - if (!strcmp(argv[i], "-f")) - { - if (i + 1 >= argc) - { - usage(argv[0]); - return 1; - } - formula = argv[++i]; - } - else - { - usage(argv[0]); - return 1; - } - } - - if (formula.empty()) - { - usage(argv[0]); - return 1; - } - - spot::ltl::parse_error_list p1; - const spot::ltl::formula* f1 = spot::ltl::parse(formula, p1); - if (spot::ltl::format_parse_errors(std::cerr, formula, p1)) - return 2; - - auto a = spot::ltl_to_tgba_fm(f1, spot::make_bdd_dict()); - auto complement = spot::make_saba_complement(a); - spot::saba_dotty_reachable(std::cout, complement); - f1->destroy(); -}