Commit fc17dd05 authored by Thibault Allançon's avatar Thibault Allançon

bench: bitstate: move benchmarking tools out of mc/

* bench/Makefile.am,
  configure.ac: add new bitstate sub-folder
* bench/bitstate/Makefile.am,
  bench/bitstate/bitstate.cc,
  bench/bitstate/bitstate.hh: implementation here
* spot/mc/Makefile.am,
  spot/mc/bitstate.hh,
  spot/mc/mc.hh,
  tests/ltsmin/modelcheck.cc: remove code from here
parent 8abe78a7
Pipeline #17034 failed with stage
in 84 minutes and 2 seconds
......@@ -19,4 +19,4 @@
## You should have received a copy of the GNU General Public License
## along with this program. If not, see <http://www.gnu.org/licenses/>.
SUBDIRS = emptchk ltl2tgba ltlcounter ltlclasses wdba spin13 dtgbasat stutter
SUBDIRS = bitstate emptchk ltl2tgba ltlcounter ltlclasses wdba spin13 dtgbasat stutter
## -*- coding: utf-8 -*-
## Copyright (C) 2020 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 <http://www.gnu.org/licenses/>.
AM_CPPFLAGS = -I$(top_builddir) -I$(top_srcdir) $(BUDDY_CPPFLAGS) \
-I$(top_builddir)/lib -I$(top_srcdir)/lib
AM_CXXFLAGS = $(CXXFLAGS)
LDADD = \
$(top_builddir)/bin/libcommon.a \
$(top_builddir)/lib/libgnu.la \
$(top_builddir)/spot/libspot.la \
$(top_builddir)/buddy/src/libbddx.la \
$(top_builddir)/spot/ltsmin/libspotltsmin.la
bin_PROGRAMS = bitstate
bitstate_SOURCES = bitstate.cc
// -*- coding: utf-8 -*-
// Copyright (C) 2020 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/>.
#include "config.h"
#include "bin/common_conv.hh"
#include "bin/common_setup.hh"
#include "bin/common_output.hh"
#include <spot/kripke/kripkegraph.hh>
#include <spot/ltsmin/ltsmin.hh>
#include <spot/ltsmin/spins_kripke.hh>
#include <ostream>
#include <string>
#include <thread>
#include <vector>
#include "bitstate.hh"
template<typename kripke_ptr, typename State,
typename Iterator, typename Hash, typename Equal>
void run(kripke_ptr sys, std::ofstream& csv, std::vector<size_t> mem_sizes)
{
std::string header("memory (bits), nb states reached");
csv << header << '\n';
// TODO: add timer and memory usage (misc/memusage and misc/timer)
for (auto mem_size : mem_sizes)
{
using algo_name = bitstate_hashing_stats<State, Iterator, Hash, Equal>;
auto bh = new algo_name(*sys, mem_size);
bh->run();
csv << mem_size << ',' << bh->get_nb_reached_states() << '\n';
delete bh;
}
}
int main(int argc, char** argv)
{
if (argc != 4)
{
std::cout << "Usage: ./bitstate [MODEL] [LOG_FILE] [MEM_SIZES]";
return 1;
}
const unsigned compression_level = 0;
const unsigned nb_threads = 1;
std::string model_path = argv[1];
std::ofstream log_file(argv[2]);
// Parse comma separated values
std::vector<size_t> mem_sizes;
std::istringstream iss(argv[3]);
std::string mem_size;
while (std::getline(iss, mem_size, ','))
mem_sizes.push_back(std::atoi(mem_size.c_str()));
// Load model
spot::ltsmin_kripkecube_ptr modelcube = nullptr;
try
{
modelcube = spot::ltsmin_model::load(model_path)
.kripkecube({}, spot::formula::ff(), compression_level, nb_threads);
}
catch (const std::runtime_error& e)
{
std::cerr << e.what() << '\n';
}
run<spot::ltsmin_kripkecube_ptr,
spot::cspins_state,
spot::cspins_iterator,
spot::cspins_state_hash,
spot::cspins_state_equal>
(modelcube, log_file, mem_sizes);
return 0;
}
......@@ -23,95 +23,71 @@
#include <spot/mc/bloom_filter.hh>
#include <spot/misc/hashfunc.hh>
namespace spot
using namespace spot;
template<typename State, typename SuccIterator,
typename StateHash, typename StateEqual>
class bitstate_hashing_stats
{
template<typename State, typename SuccIterator,
typename StateHash, typename StateEqual>
class bitstate
public:
bitstate_hashing_stats(kripkecube<State, SuccIterator>& sys, size_t mem_size):
sys_(sys)
{
public:
bitstate(kripkecube<State, SuccIterator>& sys, size_t mem_size):
sys_(sys)
{
static_assert(spot::is_a_kripkecube_ptr<decltype(&sys),
State, SuccIterator>::value,
"error: does not match the kripkecube requirements");
seen_.reserve(2000000);
todo_.reserve(100000);
bloom_filter::hash_functions_t hash_functions = {lookup3_hash};
bf_ = std::make_unique<bloom_filter>(mem_size, hash_functions);
}
static_assert(spot::is_a_kripkecube_ptr<decltype(&sys),
State, SuccIterator>::value,
"error: does not match the kripkecube requirements");
~bitstate()
{
// States will be destroyed by the system, so just clear map
seen_.clear();
}
seen_.reserve(2000000);
todo_.reserve(100000);
unsigned int dfs()
{
unsigned int state_number = 1;
State initial = sys_.initial(tid_);
todo_.push_back(initial);
while (!todo_.empty())
{
State current = todo_.back();
todo_.pop_back();
seen_.insert(current);
bloom_filter::hash_functions_t hash_functions = {lookup3_hash};
bf_ = std::make_unique<bloom_filter>(mem_size, hash_functions);
}
for (auto it = sys_.succ(current, tid_); !it->done(); it->next())
{
auto neighbor = it->state();
if (seen_.count(neighbor) == 0)
{
todo_.push_back(neighbor);
seen_.insert(neighbor);
++state_number;
}
}
}
~bitstate_hashing_stats()
{
// States will be destroyed by the system, so just clear map
seen_.clear();
}
return state_number;
}
void run()
{
state_number_ = 1;
State initial = sys_.initial(tid_);
StateHash state_hash;
todo_.push_back(initial);
unsigned int dfs_bitstate_hashing()
while (!todo_.empty())
{
unsigned int state_number = 1;
State initial = sys_.initial(tid_);
StateHash state_hash;
todo_.push_back(initial);
State current = todo_.back();
todo_.pop_back();
bf_->insert(state_hash(current));
while (!todo_.empty())
for (auto it = sys_.succ(current, tid_); !it->done(); it->next())
{
State current = todo_.back();
todo_.pop_back();
bf_->insert(state_hash(current));
for (auto it = sys_.succ(current, tid_); !it->done(); it->next())
auto neighbor = it->state();
if (bf_->contains(state_hash(neighbor)) == false)
{
auto neighbor = it->state();
if (bf_->contains(state_hash(neighbor)) == false)
{
todo_.push_back(neighbor);
bf_->insert(state_hash(neighbor));
++state_number;
}
todo_.push_back(neighbor);
bf_->insert(state_hash(neighbor));
++state_number_;
}
}
return state_number;
}
}
protected:
kripkecube<State, SuccIterator>& sys_;
unsigned int tid_;
std::unordered_set<State, StateHash, StateEqual> seen_;
std::vector<State> todo_;
// TODO: unique_ptr are not thread safe
std::unique_ptr<bloom_filter> bf_;
};
}
unsigned int get_nb_reached_states()
{
return state_number_;
}
protected:
kripkecube<State, SuccIterator>& sys_;
unsigned int tid_;
std::unordered_set<State, StateHash, StateEqual> seen_;
std::vector<State> todo_;
unsigned int state_number_;
// TODO: unique_ptr are not thread safe
std::unique_ptr<bloom_filter> bf_;
};
......@@ -212,6 +212,7 @@ AC_CONFIG_FILES([
bin/Makefile
bin/man/Makefile
bench/Makefile
bench/bitstate/Makefile
bench/dtgbasat/Makefile
bench/emptchk/Makefile
bench/emptchk/defs
......
......@@ -21,7 +21,7 @@ AM_CPPFLAGS = -I$(top_builddir) -I$(top_srcdir) $(BUDDY_CPPFLAGS)
AM_CXXFLAGS = $(WARNING_CXXFLAGS)
mcdir = $(pkgincludedir)/mc
mc_HEADERS = bitstate.hh bloom_filter.hh reachability.hh intersect.hh ec.hh unionfind.hh utils.hh\
mc_HEADERS = bloom_filter.hh reachability.hh intersect.hh ec.hh unionfind.hh utils.hh\
mc.hh deadlock.hh bloemen.hh cndfs.hh
noinst_LTLIBRARIES = libmc.la
......
......@@ -26,10 +26,8 @@
#include <vector>
#include <utility>
#include <spot/kripke/kripke.hh>
#include <spot/mc/bitstate.hh>
#include <spot/mc/bloemen.hh>
#include <spot/mc/bloemen_ec.hh>
#include <spot/mc/bloom_filter.hh>
#include <spot/mc/cndfs.hh>
#include <spot/mc/deadlock.hh>
#include <spot/mc/ec.hh>
......@@ -415,17 +413,4 @@ namespace spot
return std::make_tuple(is_empty, trace, stats, tm);
}
template<typename kripke_ptr, typename State,
typename Iterator, typename Hash, typename Equal>
void bitstate_hashing(kripke_ptr sys, size_t mem_size)
{
using algo_name = spot::bitstate<State, Iterator, Hash, Equal>;
auto s = new algo_name(*sys, mem_size);
std::cout << "\nBitstate hashing:\n";
std::cout << "DFS: " << s->dfs() << '\n';
std::cout << "DFS (with BH): " << s->dfs_bitstate_hashing() << '\n';
delete s;
}
}
......@@ -77,7 +77,6 @@ struct mc_options_
bool bloemen = false;
bool bloemen_ec = false;
bool cndfs = false;
size_t bitstate_mem_size = 0;
} mc_options;
......@@ -126,9 +125,6 @@ parse_opt_finput(int key, char* arg, struct argp_state*)
mc_options.has_deadlock = true;
mc_options.selfloopize = false;
break;
case 'H':
mc_options.bitstate_mem_size = to_unsigned(arg, "-H/--bitstate-hashing");
break;
case 'k':
mc_options.kripke_output = true;
break;
......@@ -200,10 +196,6 @@ static const argp_option options[] =
"2 : (faster) assume all values in [0 .. 2^28-1]", 0 },
// ------------------------------------------------------------
{ nullptr, 0, nullptr, 0, "General options:", 5 },
// ------------------------------------------------------------
{ nullptr, 0, nullptr, 0, "Bitstate hashing", 6 },
{ "bitstate_hashing", 'H', "INT", 0, "bitstate hashing memory size", 0 },
{ nullptr, 0, nullptr, 0, nullptr, 0 }
};
......@@ -315,42 +307,6 @@ static int checked_main()
}
}
if (mc_options.bitstate_mem_size != 0)
{
tm.start("load kripkecube");
spot::ltsmin_kripkecube_ptr modelcube = nullptr;
try
{
modelcube = spot::ltsmin_model::load(mc_options.model)
.kripkecube({}, spot::formula::ff(), mc_options.compress,
mc_options.nb_threads);
}
catch (const std::runtime_error& e)
{
std::cerr << e.what() << '\n';
}
tm.stop("load kripkecube");
int memused = spot::memusage();
tm.start("deadlock check");
spot::bitstate_hashing<spot::ltsmin_kripkecube_ptr,
spot::cspins_state,
spot::cspins_iterator,
spot::cspins_state_hash,
spot::cspins_state_equal>
(modelcube, mc_options.bitstate_mem_size);
tm.stop("deadlock check");
memused = spot::memusage() - memused;
if (!modelcube)
{
exit_code = 2;
goto safe_exit;
}
return 0;
}
if (mc_options.nb_threads == 1 &&
mc_options.formula != nullptr &&
mc_options.model != nullptr &&
......
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