Commit 22c4c4a1 authored by Etienne Renault's avatar Etienne Renault

reachability: sequential reachability for kripkecube

* README, configure.ac, spot/mc/Makefile.am,
spot/mc/reachability.hh: here.
parent 5df48a5a
......@@ -284,6 +284,7 @@ spot/ Sources for libspot.
kripke/ Kripke Structure interface.
tl/ Temporal Logic formulas and algorithms.
misc/ Miscellaneous support files.
mc/ All algorithms useful for model checking
parseaut/ Parser for automata in multiple formats.
parsetl/ Parser for LTL/PSL formulas.
priv/ Private algorithms, used internally but not exported.
......
......@@ -234,6 +234,7 @@ AC_CONFIG_FILES([
spot/ltsmin/Makefile
spot/Makefile
spot/misc/Makefile
spot/mc/Makefile
spot/parseaut/Makefile
spot/parsetl/Makefile
spot/priv/Makefile
......
## -*- coding: utf-8 -*-
## Copyright (C) 2009, 2010, 2011, 2012, 2013, 2014, 2015, 2016 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 <http://www.gnu.org/licenses/>.
AM_CPPFLAGS = -I$(top_builddir) -I$(top_srcdir) $(BUDDY_CPPFLAGS)
AM_CXXFLAGS = $(WARNING_CXXFLAGS)
mcdir = $(pkgincludedir)/mc
mc_HEADERS = reachability.hh
noinst_LTLIBRARIES = libmc.la
// -*- coding: utf-8 -*-
// Copyright (C) 2015, 2016 Laboratoire de Recherche et
// Developpement de l'Epita
//
// 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/>.
#pragma once
#include <spot/kripke/kripke.hh>
namespace spot
{
/// \brief This template class provide a sequential reachability
/// of a kripkecube. The algorithm uses a single DFS since it
/// is the most efficient in a sequential setting
template<typename State, typename SuccIterator,
typename StateHash, typename StateEqual,
typename Visitor>
class SPOT_API seq_reach_kripke
{
public:
seq_reach_kripke(kripkecube<State, SuccIterator>& sys):
sys_(sys)
{
assert(is_a_kripkecube(sys));
visited.reserve(2000000);
todo.reserve(100000);
}
~seq_reach_kripke()
{
// States will be destroyed by the system, so just clear map
visited.clear();
}
Visitor& self()
{
return static_cast<Visitor&>(*this);
}
void run()
{
self().setup();
State initial = sys_.initial();
todo.push_back({initial, sys_.succ(initial)});
visited[initial] = ++dfs_number;
self().push(initial, dfs_number);
while (!todo.empty())
{
if (todo.back().it->done())
{
sys_.recycle(todo.back().it);
todo.pop_back();
}
else
{
++transitions;
State dst = todo.back().it->state();
auto it = visited.insert({dst, dfs_number+1});
if (it.second)
{
++dfs_number;
self().push(dst, dfs_number);
self().edge(visited[todo.back().s], dfs_number);
todo.back().it->next();
todo.push_back({dst, sys_.succ(dst)});
}
else
{
self().edge(visited[todo.back().s], visited[dst]);
todo.back().it->next();
}
}
}
self().finalize();
}
unsigned int states()
{
return dfs_number;
}
unsigned int trans()
{
return transitions;
}
protected:
struct todo_element
{
State s;
SuccIterator* it;
};
kripkecube<State, SuccIterator>& sys_;
std::vector<todo_element> todo;
// FIXME: The system already handle a set of visited states so
// this map is redundant: an we avoid this new map?
typedef std::unordered_map<const State, int,
StateHash, StateEqual> visited_map;
visited_map visited;
unsigned int dfs_number = 0;
unsigned int transitions = 0;
};
}
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment