diff --git a/src/tgbaalgos/gtec/Makefile.am b/src/tgbaalgos/gtec/Makefile.am index 0d2835da8..7daa01b58 100644 --- a/src/tgbaalgos/gtec/Makefile.am +++ b/src/tgbaalgos/gtec/Makefile.am @@ -27,7 +27,6 @@ gtecdir = $(pkgincludedir)/tgbaalgos/gtec gtec_HEADERS = \ ce.hh \ - explscc.hh \ gtec.hh \ sccstack.hh \ status.hh @@ -35,7 +34,6 @@ gtec_HEADERS = \ noinst_LTLIBRARIES = libgtec.la libgtec_la_SOURCES = \ ce.cc \ - explscc.cc \ gtec.cc \ sccstack.cc \ status.cc diff --git a/src/tgbaalgos/gtec/explscc.cc b/src/tgbaalgos/gtec/explscc.cc deleted file mode 100644 index c489d0034..000000000 --- a/src/tgbaalgos/gtec/explscc.cc +++ /dev/null @@ -1,65 +0,0 @@ -// Copyright (C) 2011 Laboratoire de Recherche et Developpement de -// l'Epita (LRDE). -// Copyright (C) 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 "explscc.hh" - -namespace spot -{ - const state* - connected_component_hash_set::has_state(const state* s) const - { - set_type::const_iterator it = states.find(s); - if (it != states.end()) - { - if (s != *it) - s->destroy(); - return *it; - } - else - return 0; - } - - void - connected_component_hash_set::insert(const state* s) - { - states.insert(s); - } - - ////////////////////////////////////////////////////////////////////// - - connected_component_hash_set_factory::connected_component_hash_set_factory() - : explicit_connected_component_factory() - { - } - - connected_component_hash_set* - connected_component_hash_set_factory::build() const - { - return new connected_component_hash_set(); - } - - const connected_component_hash_set_factory* - connected_component_hash_set_factory::instance() - { - static connected_component_hash_set_factory f; - return &f; - } -} diff --git a/src/tgbaalgos/gtec/explscc.hh b/src/tgbaalgos/gtec/explscc.hh deleted file mode 100644 index e1a6ff810..000000000 --- a/src/tgbaalgos/gtec/explscc.hh +++ /dev/null @@ -1,91 +0,0 @@ -// -*- coding: utf-8 -*- -// Copyright (C) 2011, 2013, 2014 Laboratoire de Recherche et Développement -// de l'Epita (LRDE). -// Copyright (C) 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 . - -#ifndef SPOT_TGBAALGOS_GTEC_EXPLSCC_HH -# define SPOT_TGBAALGOS_GTEC_EXPLSCC_HH - -#include "misc/hash.hh" -#include "sccstack.hh" - -namespace spot -{ - /// An SCC storing all its states explicitly. - class SPOT_API explicit_connected_component: - public scc_stack::connected_component - { - public: - virtual ~explicit_connected_component() {} - /// \brief Check if the SCC contains states \a s. - /// - /// Return the representative of \a s in the SCC, and destroy \a - /// s if it is different (acting like - /// numbered_state_heap::filter), or 0 otherwise. - virtual const state* has_state(const state* s) const = 0; - - /// Insert a new state in the SCC. - virtual void insert(const state* s) = 0; - }; - - /// A straightforward implementation of explicit_connected_component - /// using a hash. - class SPOT_API connected_component_hash_set: - public explicit_connected_component - { - public: - virtual ~connected_component_hash_set() {} - virtual const state* has_state(const state* s) const; - virtual void insert(const state* s); - protected: - typedef std::unordered_set set_type; - set_type states; - }; - - /// Abstract factory for explicit_connected_component. - class explicit_connected_component_factory - { - public: - virtual ~explicit_connected_component_factory() {} - /// Create an explicit_connected_component. - virtual explicit_connected_component* build() const = 0; - }; - - /// \brief Factory for connected_component_hash_set. - /// - /// This class is a singleton. Retrieve the instance using instance(). - class connected_component_hash_set_factory : - public explicit_connected_component_factory - { - public: - virtual connected_component_hash_set* build() const; - - /// Get the unique instance of this class. - static const connected_component_hash_set_factory* instance(); - - protected: - virtual ~connected_component_hash_set_factory() {} - /// Construction is forbiden. - connected_component_hash_set_factory(); - }; -} - -#endif // SPOT_TGBAALGOS_GTEC_EXPLSCC_HH