alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

delete two unused files

Browse source 
* src/tgbaalgos/gtec/explscc.cc, src/tgbaalgos/gtec/explscc.hh: Delete.
* src/tgbaalgos/gtec/Makefile.am: Adjust.
This commit is contained in:
Alexandre Duret-Lutz 2014-12-06 23:41:50 +01:00
parent d2597854c8
commit 6dd2749c25
3 changed files with 0 additions and 158 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/tgbaalgos/gtec/Makefile.am
View file

@ -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

65
src/tgbaalgos/gtec/explscc.cc
View file

@ -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 <http://www.gnu.org/licenses/>.
#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;
}
}

91
src/tgbaalgos/gtec/explscc.hh
View file

@ -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 <http://www.gnu.org/licenses/>.
#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<const state*,
state_ptr_hash, state_ptr_equal> 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