5bb29d646b
* spot/mc/Makefile.am, spot/mc/bloemen.hh, spot/mc/bloemen_ec.hh, spot/mc/cndfs.hh, spot/mc/deadlock.hh, spot/mc/ec.hh, spot/mc/intersect.hh, spot/mc/mc.hh, spot/mc/mc_instanciator.hh, spot/mc/utils.hh, tests/ltsmin/modelcheck.cc: Here.
577 lines
19 KiB
C++
577 lines
19 KiB
C++
// -*- coding: utf-8 -*-
|
|
// Copyright (C) 2011-2020 Laboratoire de Recherche et Developpement
|
|
// 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/>.
|
|
|
|
#include "config.h"
|
|
#include "bin/common_conv.hh"
|
|
#include "bin/common_setup.hh"
|
|
#include "bin/common_output.hh"
|
|
|
|
#include <spot/ltsmin/ltsmin.hh>
|
|
#include <spot/ltsmin/spins_kripke.hh>
|
|
#include <spot/mc/mc_instanciator.hh>
|
|
#include <spot/twaalgos/dot.hh>
|
|
#include <spot/tl/defaultenv.hh>
|
|
#include <spot/tl/parse.hh>
|
|
#include <spot/twaalgos/translate.hh>
|
|
#include <spot/twaalgos/emptiness.hh>
|
|
#include <spot/twaalgos/postproc.hh>
|
|
#include <spot/twaalgos/degen.hh>
|
|
#include <spot/twaalgos/are_isomorphic.hh>
|
|
#include <spot/twa/twaproduct.hh>
|
|
#include <spot/misc/timer.hh>
|
|
#include <spot/misc/memusage.hh>
|
|
#include <cstring>
|
|
#include <spot/kripke/kripkegraph.hh>
|
|
#include <spot/twaalgos/hoa.hh>
|
|
|
|
#include <algorithm>
|
|
#include <thread>
|
|
#include <spot/twacube/twacube.hh>
|
|
#include <spot/twacube_algos/convert.hh>
|
|
#include <spot/mc/ec.hh>
|
|
|
|
const char argp_program_doc[] =
|
|
"Process model and formula to check wether a "
|
|
"model meets a specification.\v\
|
|
Exit status:\n\
|
|
0 No counterexample found\n\
|
|
1 A counterexample has been found\n\
|
|
2 Errors occurs during processing";
|
|
|
|
const unsigned DOT_MODEL = 1;
|
|
const unsigned DOT_PRODUCT = 2;
|
|
const unsigned DOT_FORMULA = 4;
|
|
const unsigned CSV = 8;
|
|
|
|
// Handle all options specified in the command line
|
|
struct mc_options_
|
|
{
|
|
bool compute_counterexample = false;
|
|
unsigned dot_output = 0;
|
|
bool is_empty = false;
|
|
char* formula = nullptr;
|
|
char* model = nullptr;
|
|
bool selfloopize = true;
|
|
char* dead_ap = nullptr;
|
|
bool use_timer = false;
|
|
unsigned compress = 0;
|
|
unsigned nb_threads = 1;
|
|
bool csv = false;
|
|
spot::mc_algorithm algorithm = spot::mc_algorithm::BLOEMEN_EC;
|
|
bool force_parallel = false;
|
|
} mc_options;
|
|
|
|
|
|
static int
|
|
parse_opt_finput(int key, char* arg, struct argp_state*)
|
|
{
|
|
// This switch is alphabetically-ordered.
|
|
switch (key)
|
|
{
|
|
case CSV:
|
|
mc_options.csv = true;
|
|
break;
|
|
case 'B':
|
|
mc_options.algorithm = spot::mc_algorithm::BLOEMEN_EC;
|
|
mc_options.force_parallel = true;
|
|
break;
|
|
case 'b':
|
|
// FIXME Differenciate bloemen and bloemen_ec: -b/-B is not enough
|
|
mc_options.algorithm = spot::mc_algorithm::BLOEMEN_SCC;
|
|
mc_options.force_parallel = true;
|
|
break;
|
|
case 'c':
|
|
mc_options.compute_counterexample = true;
|
|
break;
|
|
case 'C':
|
|
mc_options.algorithm = spot::mc_algorithm::CNDFS;
|
|
mc_options.force_parallel = true;
|
|
break;
|
|
case 'd':
|
|
if (strcmp(arg, "model") == 0)
|
|
mc_options.dot_output |= DOT_MODEL;
|
|
else if (strcmp(arg, "product") == 0)
|
|
mc_options.dot_output |= DOT_PRODUCT;
|
|
else if (strcmp(arg, "formula") == 0)
|
|
mc_options.dot_output |= DOT_FORMULA;
|
|
else
|
|
{
|
|
std::cerr << "Unknown argument: '" << arg
|
|
<< "' for option --dot\n";
|
|
return ARGP_ERR_UNKNOWN;
|
|
}
|
|
break;
|
|
case 'e':
|
|
mc_options.is_empty = true;
|
|
break;
|
|
case 'f':
|
|
mc_options.formula = arg;
|
|
break;
|
|
case 'h':
|
|
mc_options.algorithm = spot::mc_algorithm::DEADLOCK;
|
|
mc_options.force_parallel = true;
|
|
mc_options.selfloopize = false;
|
|
break;
|
|
case 'm':
|
|
mc_options.model = arg;
|
|
break;
|
|
case 'p':
|
|
mc_options.nb_threads = to_unsigned(arg, "-p/--parallel");
|
|
mc_options.force_parallel = true;
|
|
break;
|
|
case 's':
|
|
mc_options.dead_ap = arg;
|
|
break;
|
|
case 't':
|
|
mc_options.use_timer = true;
|
|
break;
|
|
case 'w':
|
|
mc_options.algorithm = spot::mc_algorithm::SWARMING;
|
|
mc_options.force_parallel = true;
|
|
break;
|
|
case 'z':
|
|
mc_options.compress = to_unsigned(arg, "-z/--compress");
|
|
break;
|
|
default:
|
|
return ARGP_ERR_UNKNOWN;
|
|
}
|
|
return 0;
|
|
}
|
|
|
|
static const argp_option options[] =
|
|
{
|
|
// Keep each section sorted
|
|
// ------------------------------------------------------------
|
|
{ nullptr, 0, nullptr, 0, "Input options:", 1 },
|
|
{ "formula", 'f', "STRING", 0, "use the formula STRING", 0 },
|
|
// FIXME do we want support for reading more than one formula?
|
|
{ "model", 'm', "STRING", 0, "use the model stored in file STRING", 0 },
|
|
// ------------------------------------------------------------
|
|
{ nullptr, 0, nullptr, 0, "Process options:", 2 },
|
|
{ "bloemen-ec", 'B', nullptr, 0,
|
|
"run the emptiness-check of Bloemen et al. (HVC'16). Return 1 "
|
|
"if a counterexample is found.", 0},
|
|
{ "bloemen", 'b', nullptr, 0,
|
|
"run the SCC computation of Bloemen et al. (PPOPP'16). Return 1 "
|
|
"if a counterexample is found.", 0 },
|
|
{ "cndfs", 'C', nullptr, 0,
|
|
"run the emptiness check of Evangelista et al. (ATVA'12). Return 1 "
|
|
"if a counterexample is found.", 0 },
|
|
{ "counterexample", 'c', nullptr, 0,
|
|
"compute an accepting counterexample (if it exists)", 0 },
|
|
{ "has-deadlock", 'h', nullptr, 0,
|
|
"check if the model has a deadlock. "
|
|
"Return 1 if the model contains a deadlock."
|
|
, 0 },
|
|
{ "is-empty", 'e', nullptr, 0,
|
|
"check if the model meets its specification. Uses Cou99 in sequential "
|
|
"and bloemen-ec in pallel (option -p). Return 1 if a counterexample "
|
|
"is found."
|
|
, 0 },
|
|
{ "parallel", 'p', "INT", 0, "use INT threads (when possible)", 0 },
|
|
{ "selfloopize", 's', "STRING", 0,
|
|
"use STRING as property for marking deadlock "
|
|
"states (by default selfloopize is activated with STRING='true')", 0 },
|
|
{ "swarming", 'w', nullptr, 0,
|
|
"run the technique of of Holzmann et al. (IEEE'11) with the emptiness-"
|
|
"check of Renault et al. (LPAR'13). Returns 1 if a counterexample "
|
|
"is found.", 0 },
|
|
{ "timer", 't', nullptr, 0,
|
|
"time the different phases of the execution", 0 },
|
|
// ------------------------------------------------------------
|
|
{ nullptr, 0, nullptr, 0, "Output options:", 3 },
|
|
{ "csv", CSV, nullptr, 0,
|
|
"output a CSV containing interesting values", 0 },
|
|
{ "dot", 'd', "[model|product|formula]", 0,
|
|
"output the associated automaton in dot format", 0 },
|
|
// ------------------------------------------------------------
|
|
{ nullptr, 0, nullptr, 0, "Optimization options:", 4 },
|
|
{ "compress", 'z', "INT", 0, "specify the level of compression\n"
|
|
"1 : handle large models\n"
|
|
"2 : (faster) assume all values in [0 .. 2^28-1]", 0 },
|
|
// ------------------------------------------------------------
|
|
{ nullptr, 0, nullptr, 0, "General options:", 5 },
|
|
{ nullptr, 0, nullptr, 0, nullptr, 0 }
|
|
};
|
|
|
|
const struct argp finput_argp = { options, parse_opt_finput,
|
|
nullptr, nullptr, nullptr,
|
|
nullptr, nullptr };
|
|
|
|
const struct argp_child children[] =
|
|
{
|
|
{ &finput_argp, 0, nullptr, 1 },
|
|
{ &misc_argp, 0, nullptr, -1 },
|
|
{ nullptr, 0, nullptr, 0 }
|
|
};
|
|
|
|
static std::string split_filename(const std::string& str) {
|
|
unsigned found = str.find_last_of("/");
|
|
return str.substr(found+1);
|
|
}
|
|
|
|
static int checked_main()
|
|
{
|
|
spot::default_environment& env = spot::default_environment::instance();
|
|
spot::atomic_prop_set ap;
|
|
auto dict = spot::make_bdd_dict();
|
|
spot::const_kripke_ptr model = nullptr;
|
|
spot::const_twa_graph_ptr prop = nullptr;
|
|
spot::const_twa_ptr product = nullptr;
|
|
spot::emptiness_check_instantiator_ptr echeck_inst = nullptr;
|
|
int exit_code = 0;
|
|
spot::postprocessor post;
|
|
spot::formula deadf = spot::formula::tt();
|
|
spot::formula f = nullptr;
|
|
spot::timer_map tm;
|
|
|
|
if (mc_options.selfloopize)
|
|
{
|
|
if (mc_options.dead_ap == nullptr ||
|
|
!strcasecmp(mc_options.dead_ap, "true"))
|
|
deadf = spot::formula::tt();
|
|
else if (!strcasecmp(mc_options.dead_ap, "false"))
|
|
deadf = spot::formula::ff();
|
|
else
|
|
deadf = env.require(mc_options.dead_ap);
|
|
}
|
|
|
|
if (mc_options.formula != nullptr)
|
|
{
|
|
tm.start("parsing formula");
|
|
{
|
|
auto pf = spot::parse_infix_psl(mc_options.formula, env, false);
|
|
exit_code = pf.format_errors(std::cerr);
|
|
f = pf.f;
|
|
}
|
|
tm.stop("parsing formula");
|
|
|
|
tm.start("translating formula");
|
|
{
|
|
spot::translator trans(dict);
|
|
// if (deterministic) FIXME
|
|
// trans.set_pref(spot::postprocessor::Deterministic);
|
|
prop = trans.run(&f);
|
|
}
|
|
tm.stop("translating formula");
|
|
|
|
atomic_prop_collect(f, &ap);
|
|
|
|
if (mc_options.dot_output & DOT_FORMULA)
|
|
{
|
|
tm.start("dot output");
|
|
spot::print_dot(std::cout, prop);
|
|
tm.stop("dot output");
|
|
}
|
|
}
|
|
|
|
if (mc_options.model != nullptr)
|
|
{
|
|
tm.start("loading ltsmin model");
|
|
try
|
|
{
|
|
model = spot::ltsmin_model::load(mc_options.model)
|
|
.kripke(&ap, dict, deadf, mc_options.compress);
|
|
}
|
|
catch (const std::runtime_error& e)
|
|
{
|
|
std::cerr << e.what() << '\n';
|
|
}
|
|
tm.stop("loading ltsmin model");
|
|
|
|
if (!model)
|
|
{
|
|
exit_code = 2;
|
|
goto safe_exit;
|
|
}
|
|
|
|
if (mc_options.dot_output & DOT_MODEL)
|
|
{
|
|
tm.start("dot output");
|
|
spot::print_dot(std::cout, model);
|
|
tm.stop("dot output");
|
|
}
|
|
}
|
|
|
|
if (mc_options.force_parallel == false &&
|
|
mc_options.formula != nullptr &&
|
|
mc_options.model != nullptr)
|
|
{
|
|
std::cout << "Warning : using sequential algorithms (BDD-based)\n\n";
|
|
|
|
product = spot::otf_product(model, prop);
|
|
|
|
if (mc_options.is_empty)
|
|
{
|
|
const char* err;
|
|
echeck_inst = spot::make_emptiness_check_instantiator("Cou99", &err);
|
|
if (!echeck_inst)
|
|
{
|
|
std::cerr << "Unknown emptiness check algorihm `"
|
|
<< err << "'\n";
|
|
exit_code = 1;
|
|
goto safe_exit;
|
|
}
|
|
|
|
auto ec = echeck_inst->instantiate(product);
|
|
assert(ec);
|
|
int memused = spot::memusage();
|
|
tm.start("running emptiness check");
|
|
spot::emptiness_check_result_ptr res;
|
|
try
|
|
{
|
|
res = ec->check();
|
|
}
|
|
catch (const std::bad_alloc&)
|
|
{
|
|
std::cerr << "Out of memory during emptiness check.\n";
|
|
if (!mc_options.compress)
|
|
std::cerr << "Try option -z for state compression.\n";
|
|
exit_code = 2;
|
|
exit(exit_code);
|
|
}
|
|
tm.stop("running emptiness check");
|
|
memused = spot::memusage() - memused;
|
|
|
|
ec->print_stats(std::cout);
|
|
std::cout << memused << " pages allocated for emptiness check"
|
|
<< std::endl;
|
|
|
|
if (!res)
|
|
{
|
|
std::cout << "no accepting run found" << std::endl;
|
|
}
|
|
else if (!mc_options.compute_counterexample)
|
|
{
|
|
std::cout << "an accepting run exists "
|
|
<< "(use -c to print it)" << std::endl;
|
|
exit_code = 1;
|
|
}
|
|
else
|
|
{
|
|
exit_code = 1;
|
|
spot::twa_run_ptr run;
|
|
tm.start("computing accepting run");
|
|
try
|
|
{
|
|
run = res->accepting_run();
|
|
}
|
|
catch (const std::bad_alloc&)
|
|
{
|
|
std::cerr
|
|
<< "Out of memory while looking for counterexample.\n";
|
|
exit_code = 2;
|
|
exit(exit_code);
|
|
}
|
|
tm.stop("computing accepting run");
|
|
|
|
if (!run)
|
|
{
|
|
std::cout << "an accepting run exists" << std::endl;
|
|
}
|
|
else
|
|
{
|
|
tm.start("reducing accepting run");
|
|
run = run->reduce();
|
|
tm.stop("reducing accepting run");
|
|
tm.start("printing accepting run");
|
|
std::cout << *run;
|
|
tm.stop("printing accepting run");
|
|
}
|
|
}
|
|
|
|
if (mc_options.csv)
|
|
{
|
|
std::cout << "\nFind following the csv: "
|
|
<< "model,formula,walltimems,memused,type,"
|
|
<< "states,transitions\n";
|
|
std::cout << '#'
|
|
<< split_filename(mc_options.model)
|
|
<< ','
|
|
<< mc_options.formula << ','
|
|
<< tm.timer("running emptiness check").walltime() << ','
|
|
<< memused << ','
|
|
<< (!res ? "EMPTY," : "NONEMPTY,")
|
|
<< ec->statistics()->get("states") << ','
|
|
<< ec->statistics()->get("transitions")
|
|
<< std::endl;
|
|
}
|
|
}
|
|
|
|
if (mc_options.dot_output & DOT_PRODUCT)
|
|
{
|
|
tm.start("dot output");
|
|
spot::print_dot(std::cout, product);
|
|
tm.stop("dot output");
|
|
}
|
|
}
|
|
// FIXME : handle here swarming
|
|
else if (mc_options.force_parallel && mc_options.model != nullptr)
|
|
{
|
|
std::cout << "Warning : using parallel algorithms (CUBE-based)\n\n";
|
|
|
|
if (mc_options.dot_output & DOT_PRODUCT)
|
|
{
|
|
std::cerr << "\nERROR: Parallel algorithm doesn't support DOT"
|
|
" output for the synchronous product.\n"
|
|
" Please consider removing '-p' option\n";
|
|
exit_code = 2;
|
|
goto safe_exit;
|
|
}
|
|
|
|
if (prop == nullptr &&
|
|
(mc_options.algorithm == spot::mc_algorithm::CNDFS ||
|
|
mc_options.algorithm == spot::mc_algorithm::BLOEMEN_EC ||
|
|
mc_options.algorithm == spot::mc_algorithm::SWARMING))
|
|
{
|
|
std::cerr << "\nERROR: Algorithm " << mc_options.algorithm
|
|
<< " requires to provide a formula (--formula)\n";
|
|
exit_code = 2;
|
|
goto safe_exit;
|
|
}
|
|
|
|
unsigned int hc = std::thread::hardware_concurrency();
|
|
if (mc_options.nb_threads > hc)
|
|
std::cerr << "Warning: you require " << mc_options.nb_threads
|
|
<< " threads, but your computer only support " << hc
|
|
<< ". This could slow down parallel algorithms.\n";
|
|
|
|
auto prop_degen = prop;
|
|
if (mc_options.algorithm == spot::mc_algorithm::CNDFS)
|
|
{
|
|
// Only support Single Acceptance Conditions
|
|
tm.start("degeneralize");
|
|
prop_degen = spot::degeneralize_tba(prop);
|
|
tm.stop("degeneralize");
|
|
}
|
|
|
|
tm.start("twa to twacube");
|
|
auto propcube = spot::twa_to_twacube(prop_degen);
|
|
tm.stop("twa to twacube");
|
|
|
|
tm.start("load kripkecube");
|
|
spot::ltsmin_kripkecube_ptr modelcube = nullptr;
|
|
try
|
|
{
|
|
std::vector<std::string> aps = {};
|
|
if (propcube != nullptr)
|
|
aps = propcube->get_ap();
|
|
|
|
modelcube = spot::ltsmin_model::load(mc_options.model)
|
|
.kripkecube(aps, deadf, 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("exploration");
|
|
|
|
auto result =
|
|
spot::ec_instanciator<spot::ltsmin_kripkecube_ptr, spot::cspins_state,
|
|
spot::cspins_iterator, spot::cspins_state_hash,
|
|
spot::cspins_state_equal>
|
|
(mc_options.algorithm, modelcube, propcube,
|
|
mc_options.compute_counterexample);
|
|
|
|
tm.stop("exploration");
|
|
memused = spot::memusage() - memused;
|
|
|
|
if (!modelcube)
|
|
{
|
|
exit_code = 2;
|
|
goto safe_exit;
|
|
}
|
|
|
|
// Display statistics
|
|
std::cout << result << '\n';
|
|
std::cout << memused << " pages allocated for "
|
|
<< mc_options.algorithm << '\n';
|
|
|
|
|
|
if (mc_options.csv)
|
|
{
|
|
std::cout << "\nSummary :\n";
|
|
auto rval = result.value[0];
|
|
std::for_each(result.value.rbegin(), result.value.rend(),
|
|
[&](spot::mc_rvalue n) { rval = rval | n; });
|
|
|
|
if (rval == spot::mc_rvalue::NO_DEADLOCK ||
|
|
rval == spot::mc_rvalue::EMPTY ||
|
|
rval == spot::mc_rvalue::SUCCESS)
|
|
std::cout << "no accepting run / counterexample found\n";
|
|
else if (!mc_options.compute_counterexample)
|
|
{
|
|
std::cout << "an accepting run exists "
|
|
<< "(use -c to print it)" << std::endl;
|
|
exit_code = 1;
|
|
}
|
|
else
|
|
std::cout << "an accepting run exists\n" << result.trace << '\n';
|
|
|
|
|
|
// Grab The informations to display into the CSV
|
|
// FIXME: The CSV can be inconsistent since it may return
|
|
// time of one thread and SCC of another.
|
|
auto walltime = std::min_element(result.walltime.rbegin(),
|
|
result.walltime.rend());
|
|
auto states = std::min_element(result.states.rbegin(),
|
|
result.states.rend());
|
|
auto trans = std::min_element(result.transitions.rbegin(),
|
|
result.transitions.rend());
|
|
auto sccs = std::max_element(result.sccs.rbegin(),
|
|
result.sccs.rend());
|
|
|
|
std::cout << "Find following the csv: "
|
|
<< "model,formula,walltimems,memused,type,"
|
|
<< "states,transitions,sccs\n";
|
|
std::cout << '#'
|
|
<< split_filename(mc_options.model) << ','
|
|
<< mc_options.formula << ','
|
|
<< *walltime << ',' << memused << ','
|
|
<< rval << ',' << *states << ',' << *trans << ','
|
|
<< *sccs << '\n';
|
|
}
|
|
}
|
|
|
|
safe_exit:
|
|
if (mc_options.use_timer)
|
|
tm.print(std::cout);
|
|
tm.reset_all(); // This helps valgrind.
|
|
return exit_code;
|
|
}
|
|
|
|
int
|
|
main(int argc, char** argv)
|
|
{
|
|
setup(argv);
|
|
const argp ap = { nullptr, nullptr, nullptr,
|
|
argp_program_doc, children, nullptr, nullptr };
|
|
|
|
if (int err = argp_parse(&ap, argc, argv, ARGP_NO_HELP, nullptr, nullptr))
|
|
exit(err);
|
|
|
|
auto exit_code = checked_main();
|
|
|
|
// Additional checks to debug reference counts in formulas.
|
|
assert(spot::fnode::instances_check());
|
|
exit(exit_code);
|
|
}
|