Commit 231016b2 authored by Etienne Renault's avatar Etienne Renault

ltsmin: move modelchek in mc directory

* spot/ltsmin/ltsmin.cc, spot/ltsmin/ltsmin.hh,
spot/mc/Makefile.am, tests/ltsmin/modelcheck.cc,
spot/mc/mc.hh: here.
parent e9c274ec
......@@ -41,7 +41,6 @@
#include <spot/twaalgos/reachiter.hh>
#include <string.h>
#include <spot/mc/utils.hh>
#include <spot/mc/ec.hh>
using namespace std::string_literals;
......@@ -1122,45 +1121,6 @@ namespace spot
{
}
std::tuple<bool, std::string, std::vector<istats>>
ltsmin_model::modelcheck(ltsmin_kripkecube_ptr sys,
spot::twacube_ptr twa, bool compute_ctrx)
{
// Must ensure that the two automata are working on the same
// set of atomic propositions.
assert(sys->get_ap().size() == twa->get_ap().size());
for (unsigned int i = 0; i < sys->get_ap().size(); ++i)
assert(sys->get_ap()[i].compare(twa->get_ap()[i]) == 0);
bool stop = false;
std::vector<ec_renault13lpar<cspins_state, cspins_iterator,
cspins_state_hash, cspins_state_equal>> ecs;
for (unsigned i = 0; i < sys->get_threads(); ++i)
ecs.push_back({*sys, twa, i, stop});
std::vector<std::thread> threads;
for (unsigned i = 0; i < sys->get_threads(); ++i)
threads.push_back
(std::thread(&ec_renault13lpar<cspins_state, cspins_iterator,
cspins_state_hash, cspins_state_equal>::run, &ecs[i]));
for (unsigned i = 0; i < sys->get_threads(); ++i)
threads[i].join();
bool has_ctrx = false;
std::string trace = "";
std::vector<istats> stats;
for (unsigned i = 0; i < sys->get_threads(); ++i)
{
has_ctrx |= ecs[i].counterexample_found();
if (compute_ctrx && ecs[i].counterexample_found()
&& trace.compare("") == 0)
trace = ecs[i].trace(); // Pick randomly one !
stats.push_back(ecs[i].stats());
}
return std::make_tuple(has_ctrx, trace, stats);
}
int ltsmin_model::state_size() const
{
return iface->get_state_size();
......
......@@ -25,7 +25,6 @@
#include <spot/twacube/twacube.hh>
#include <spot/tl/apcollect.hh>
#include <tuple>
#include <spot/mc/intersect.hh>
namespace spot
{
......@@ -82,14 +81,6 @@ namespace spot
int compress = 0,
unsigned int nb_threads = 1) const;
/// \brief Check for the emptiness between a system and a twa.
/// Return a pair containing a boolean indicating wether a counterexample
/// has been found and a string representing the counterexample if the
/// computation have been required
static std::tuple<bool, std::string, std::vector<istats>>
modelcheck(ltsmin_kripkecube_ptr sys,
spot::twacube_ptr twa, bool compute_ctrx = false);
/// Number of variables in a state
int state_size() const;
/// Name of each variable
......
......@@ -21,7 +21,7 @@ AM_CPPFLAGS = -I$(top_builddir) -I$(top_srcdir) $(BUDDY_CPPFLAGS)
AM_CXXFLAGS = $(WARNING_CXXFLAGS)
mcdir = $(pkgincludedir)/mc
mc_HEADERS = reachability.hh intersect.hh ec.hh unionfind.hh utils.hh
mc_HEADERS = reachability.hh intersect.hh ec.hh unionfind.hh utils.hh mc.hh
noinst_LTLIBRARIES = libmc.la
......
// -*- coding: utf-8 -*-
// Copyright (C) 2015, 2016, 2017 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 <string>
#include <thread>
#include <tuple>
#include <vector>
#include <spot/kripke/kripke.hh>
#include <spot/mc/ec.hh>
#include <spot/misc/common.hh>
namespace spot
{
/// \brief Check for the emptiness between a system and a twa.
/// Return a pair containing a boolean indicating wether a counterexample
/// has been found and a string representing the counterexample if the
/// computation have been required
template<typename kripke_ptr, typename State,
typename Iterator, typename Hash, typename Equal>
static std::tuple<bool, std::string, std::vector<istats>>
modelcheck(kripke_ptr sys, spot::twacube_ptr twa, bool compute_ctrx = false)
{
// Must ensure that the two automata are working on the same
// set of atomic propositions.
SPOT_ASSERT(sys->get_ap().size() == twa->get_ap().size());
for (unsigned int i = 0; i < sys->get_ap().size(); ++i)
SPOT_ASSERT(sys->get_ap()[i].compare(twa->get_ap()[i]) == 0);
bool stop = false;
std::vector<ec_renault13lpar<State, Iterator, Hash, Equal>> ecs;
for (unsigned i = 0; i < sys->get_threads(); ++i)
ecs.push_back({*sys, twa, i, stop});
std::vector<std::thread> threads;
for (unsigned i = 0; i < sys->get_threads(); ++i)
threads.push_back
(std::thread(&ec_renault13lpar<State, Iterator, Hash, Equal>::run,
&ecs[i]));
for (unsigned i = 0; i < sys->get_threads(); ++i)
threads[i].join();
bool has_ctrx = false;
std::string trace = "";
std::vector<istats> stats;
for (unsigned i = 0; i < sys->get_threads(); ++i)
{
has_ctrx |= ecs[i].counterexample_found();
if (compute_ctrx && ecs[i].counterexample_found()
&& trace.compare("") == 0)
trace = ecs[i].trace(); // Pick randomly one !
stats.push_back(ecs[i].stats());
}
return std::make_tuple(has_ctrx, trace, stats);
}
}
......@@ -23,6 +23,8 @@
#include "bin/common_output.hh"
#include <spot/ltsmin/ltsmin.hh>
#include <spot/ltsmin/spins_kripke.hh>
#include <spot/mc/mc.hh>
#include <spot/twaalgos/dot.hh>
#include <spot/tl/defaultenv.hh>
#include <spot/tl/parse.hh>
......@@ -421,7 +423,11 @@ static int checked_main()
int memused = spot::memusage();
tm.start("emptiness check");
auto res = spot::ltsmin_model::modelcheck
auto res = spot::modelcheck<spot::ltsmin_kripkecube_ptr,
spot::cspins_state,
spot::cspins_iterator,
spot::cspins_state_hash,
spot::cspins_state_equal>
(modelcube, propcube, mc_options.compute_counterexample);
tm.stop("emptiness check");
memused = spot::memusage() - memused;
......
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