From f486dab2418626db47565aef780da23a09fc4367 Mon Sep 17 00:00:00 2001 From: Etienne Renault Date: Fri, 29 Sep 2017 15:18:50 +0200 Subject: [PATCH] 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. --- spot/ltsmin/ltsmin.cc | 40 --------------------- spot/ltsmin/ltsmin.hh | 9 ----- spot/mc/Makefile.am | 2 +- spot/mc/mc.hh | 74 ++++++++++++++++++++++++++++++++++++++ tests/ltsmin/modelcheck.cc | 8 ++++- 5 files changed, 82 insertions(+), 51 deletions(-) create mode 100644 spot/mc/mc.hh diff --git a/spot/ltsmin/ltsmin.cc b/spot/ltsmin/ltsmin.cc index 4950a25d7..2f0d736fc 100644 --- a/spot/ltsmin/ltsmin.cc +++ b/spot/ltsmin/ltsmin.cc @@ -41,7 +41,6 @@ #include #include #include -#include using namespace std::string_literals; @@ -1122,45 +1121,6 @@ namespace spot { } - std::tuple> - 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> ecs; - for (unsigned i = 0; i < sys->get_threads(); ++i) - ecs.push_back({*sys, twa, i, stop}); - - std::vector threads; - for (unsigned i = 0; i < sys->get_threads(); ++i) - threads.push_back - (std::thread(&ec_renault13lpar::run, &ecs[i])); - - for (unsigned i = 0; i < sys->get_threads(); ++i) - threads[i].join(); - - bool has_ctrx = false; - std::string trace = ""; - std::vector 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(); diff --git a/spot/ltsmin/ltsmin.hh b/spot/ltsmin/ltsmin.hh index ca32bc95c..130188a62 100644 --- a/spot/ltsmin/ltsmin.hh +++ b/spot/ltsmin/ltsmin.hh @@ -25,7 +25,6 @@ #include #include #include -#include 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> - 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 diff --git a/spot/mc/Makefile.am b/spot/mc/Makefile.am index 35f90e11f..693d2527a 100644 --- a/spot/mc/Makefile.am +++ b/spot/mc/Makefile.am @@ -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 diff --git a/spot/mc/mc.hh b/spot/mc/mc.hh new file mode 100644 index 000000000..2a284ac94 --- /dev/null +++ b/spot/mc/mc.hh @@ -0,0 +1,74 @@ +// -*- 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 . + +#pragma once + +#include +#include +#include +#include +#include +#include +#include + +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 + static std::tuple> + 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> ecs; + for (unsigned i = 0; i < sys->get_threads(); ++i) + ecs.push_back({*sys, twa, i, stop}); + + std::vector threads; + for (unsigned i = 0; i < sys->get_threads(); ++i) + threads.push_back + (std::thread(&ec_renault13lpar::run, + &ecs[i])); + + for (unsigned i = 0; i < sys->get_threads(); ++i) + threads[i].join(); + + bool has_ctrx = false; + std::string trace = ""; + std::vector 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); + } +} diff --git a/tests/ltsmin/modelcheck.cc b/tests/ltsmin/modelcheck.cc index 08641be05..521d7340b 100644 --- a/tests/ltsmin/modelcheck.cc +++ b/tests/ltsmin/modelcheck.cc @@ -23,6 +23,8 @@ #include "bin/common_output.hh" #include +#include +#include #include #include #include @@ -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 (modelcube, propcube, mc_options.compute_counterexample); tm.stop("emptiness check"); memused = spot::memusage() - memused;