From 4337abc5a6c99e632625507a75f83b9761b192ea Mon Sep 17 00:00:00 2001 From: Etienne Renault Date: Thu, 10 Mar 2016 13:27:42 +0100 Subject: [PATCH] modelcheck: rewrite and use argp * tests/Makefile.am, tests/ltsmin/check.test, tests/ltsmin/finite.test, tests/ltsmin/finite2.test, tests/ltsmin/kripke.test, tests/ltsmin/modelcheck.cc: here. --- tests/Makefile.am | 10 +- tests/ltsmin/check.test | 50 ++-- tests/ltsmin/finite.test | 23 +- tests/ltsmin/finite2.test | 25 +- tests/ltsmin/kripke.test | 10 +- tests/ltsmin/modelcheck.cc | 572 ++++++++++++++++++------------------- 6 files changed, 355 insertions(+), 335 deletions(-) diff --git a/tests/Makefile.am b/tests/Makefile.am index 8a07b91fc..4c305f393 100644 --- a/tests/Makefile.am +++ b/tests/Makefile.am @@ -454,10 +454,14 @@ EXTRA_DIST = \ if USE_LTSMIN check_PROGRAMS += ltsmin/modelcheck - +ltsmin_modelcheck_CPPFLAGS = -I$(top_builddir) -I$(top_srcdir) \ + $(BUDDY_CPPFLAGS) \-I$(top_builddir)/lib -I$(top_srcdir)/lib ltsmin_modelcheck_SOURCES = ltsmin/modelcheck.cc -ltsmin_modelcheck_LDADD = $(top_builddir)/spot/ltsmin/libspotltsmin.la \ - $(LDADD) -lpthread +ltsmin_modelcheck_LDADD = \ + $(top_builddir)/bin/libcommon.a \ + $(top_builddir)/lib/libgnu.la \ + $(top_builddir)/spot/libspot.la \ + $(top_builddir)/spot/ltsmin/libspotltsmin.la check_SCRIPTS += ltsmin/defs diff --git a/tests/ltsmin/check.test b/tests/ltsmin/check.test index dddbf4a78..a5de6efbb 100755 --- a/tests/ltsmin/check.test +++ b/tests/ltsmin/check.test @@ -1,6 +1,6 @@ #!/bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2011, 2012, 2014, 2015, 2016 Laboratoire de Recherche +# Copyright (C) 2011, 2012, 2014, 2015, 2016, 2017 Laboratoire de Recherche # et Développement de l'Epita (LRDE). # # This file is part of Spot, a model checking library. @@ -32,37 +32,43 @@ fi set -e -for opt in '' '-z'; do +# Promela +for opt in '' '--compress 1'; do + + run 0 ../modelcheck --is-emtpy $opt --model $srcdir/elevator2.1.pm \ + --formula '!G("req[1]==1" -> (F("p==1" && "cabin_0._pc==2")))' + run 1 ../modelcheck --is-empty $opt --model $srcdir/elevator2.1.pm \ + --formula 'F("p==2")' +done + +# dve2 +for opt in '' '--compress 1'; do # The three examples from the README. # (Don't run the first one using "run 0" because it would take too much # time with valgrind.). - ../modelcheck $opt -E $srcdir/beem-peterson.4.dve \ - '!GF(P_0.CS|P_1.CS|P_2.CS|P_3.CS)' \ - | grep -v pages > stdout1 + ../modelcheck --is-empty $opt --model $srcdir/beem-peterson.4.dve \ + --formula '!GF(P_0.CS|P_1.CS|P_2.CS|P_3.CS)' \ + | grep -v pages > stdout1 # same formula, different syntax. - ../modelcheck $opt -E $srcdir/beem-peterson.4.dve \ - '!GF("P_0==CS"|"P_1 == CS"|"P_2 ==CS"|"P_3== CS")' \ - | grep -v pages > stdout2 + ../modelcheck --is-empty $opt --model $srcdir/beem-peterson.4.dve \ + --formula '!GF("P_0==CS"|"P_1 == CS"|"P_2 ==CS"|"P_3== CS")' \ + | grep -v pages > stdout2 cmp stdout1 stdout2 - run 0 ../modelcheck $opt -e $srcdir/beem-peterson.4.dve \ - '!G(P_0.wait -> F P_0.CS)' - run 0 ../modelcheck $opt -e $srcdir/beem-peterson.4.dve '!G("pos[1] < 3")' + run 1 ../modelcheck --is-empty $opt --model $srcdir/beem-peterson.4.dve \ + --formula '!G(P_0.wait -> F P_0.CS)' + run 1 ../modelcheck --is-empty $opt --model $srcdir/beem-peterson.4.dve\ + --formula '!G("pos[1] < 3")' done # Now check some error messages. -run 1 ../modelcheck foo.dve "F(P_0.CS)" 2>stderr +run 2 ../modelcheck --model foo.dve --formula "F(P_0.CS)" 2>stderr cat stderr grep 'Cannot open' stderr # the dve2C file was generated in the current directory -run 1 ../modelcheck beem-peterson.4.dve2C \ - 'Xfoo | P_0.f & X"P_0.k < 2xx" | G"pos[0]"' 2>stderr +run 2 ../modelcheck --model beem-peterson.4.dve2C \ + --formula 'Xfoo | P_0.f & X"P_0.k < 2xx" | G"pos[0]"' 2>stderr cat stderr -grep 'variable `foo' stderr -grep "state \`f'.*P_0" stderr -grep "Unexpected.*\`xx'" stderr -grep 'Possible.*CS' stderr -grep 'Possible.*NCS' stderr -grep 'Possible.*q2' stderr -grep 'Possible.*q3' stderr -grep 'Possible.*wait' stderr +grep 'Proposition "foo"' stderr +grep 'Proposition "P_0.f"' stderr +grep 'Proposition "P_0.k<2xx"' stderr diff --git a/tests/ltsmin/finite.test b/tests/ltsmin/finite.test index d9d1aee3e..042f428c6 100755 --- a/tests/ltsmin/finite.test +++ b/tests/ltsmin/finite.test @@ -31,28 +31,33 @@ else fi set -e -run 0 ../modelcheck -gm $srcdir/finite.dve '"P.a < 10"' > stdout +run 0 ../modelcheck --dot=model --model $srcdir/finite.dve \ + --formula '"P.a < 10"' > stdout test `grep ' -> ' stdout | wc -l` = 25 test `grep 'P.a=' stdout | wc -l` = 15 -run 0 ../modelcheck -dtrue -gm $srcdir/finite.dve '"P.a < 10"' > stdout2 +run 0 ../modelcheck --selfloopize true --dot=model --model $srcdir/finite.dve \ + --formula '"P.a < 10"' > stdout2 cmp stdout stdout2 -run 0 ../modelcheck -dfalse -gm $srcdir/finite.dve '"P.a < 10"' > stdout +run 0 ../modelcheck --selfloopize false --dot model --model $srcdir/finite.dve \ + --formula '"P.a < 10"' > stdout test `grep ' -> ' stdout | wc -l` = 19 test `grep 'P.a=' stdout | wc -l` = 15 # the same with compressed states -run 0 ../modelcheck -z -dfalse -gm $srcdir/finite.dve '"P.a < 10"' > stdout +run 0 ../modelcheck --compress 1 --selfloopize false \ + --dot model --model $srcdir/finite.dve --formula '"P.a < 10"' > stdout test `grep ' -> ' stdout | wc -l` = 19 test `grep 'P.a=' stdout | wc -l` = 15 -run 0 ../modelcheck -ddead -E $srcdir/finite.dve \ - '!(G(dead -> ("P.a==3" | "P.b==3")))' +run 0 ../modelcheck --is-empty --selfloopize dead --model $srcdir/finite.dve \ + --formula '!(G(dead -> ("P.a==3" | "P.b==3")))' -run 0 ../modelcheck -ddead -e $srcdir/finite.dve \ - '!(G(dead -> ("P.a==2" | "P.b==3")))' +run 1 ../modelcheck --is-empty --selfloopize dead --model $srcdir/finite.dve \ + --formula '!(G(dead -> ("P.a==2" | "P.b==3")))' # This used to segfault because of a bug in a # function that do not exist anymore. -run 0 ../modelcheck -gp $srcdir/finite.dve true +run 0 ../modelcheck --dot product --model $srcdir/finite.dve \ + --formula true diff --git a/tests/ltsmin/finite2.test b/tests/ltsmin/finite2.test index d4fc731f1..509fc5a0e 100755 --- a/tests/ltsmin/finite2.test +++ b/tests/ltsmin/finite2.test @@ -1,6 +1,6 @@ #!/bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2011, 2013, 2014 Laboratoire de Recherche et Développement +# Copyright (C) 2011, 2013, 2014, 2016 Laboratoire de Recherche et Développement # de l'Epita (LRDE). # # This file is part of Spot, a model checking library. @@ -28,27 +28,30 @@ if ! spins $srcdir/finite.pm; then exit 77 fi -run 0 ../modelcheck -gm $srcdir/finite.pm '"P_0.a < 10"' > stdout +run 0 ../modelcheck --dot model --model $srcdir/finite.pm \ + --formula '"P_0.a < 10"' > stdout test `grep ' -> ' stdout | wc -l` = 25 test `grep 'P_0.a=' stdout | wc -l` = 15 -run 0 ../modelcheck -dtrue -gm $srcdir/finite.pm '"P_0.a < 10"' > stdout2 +run 0 ../modelcheck --selfloopize true --dot model --model $srcdir/finite.pm \ + --formula '"P_0.a < 10"' > stdout2 diff stdout stdout2 -run 0 ../modelcheck -dfalse -gm $srcdir/finite.pm '"P_0.a < 10"' > stdout +run 0 ../modelcheck --selfloopize dfalse --dot model --model $srcdir/finite.pm \ + --formula '"P_0.a < 10"' > stdout test `grep ' -> ' stdout | wc -l` = 19 test `grep 'P_0.a=' stdout | wc -l` = 15 # the same with compressed states -run 0 ../modelcheck -z -dfalse -gm $srcdir/finite.pm '"P_0.a < 10"' \ -> stdout +run 0 ../modelcheck -compress --selfloopize false --dot model \ + --model $srcdir/finite.pm --formula '"P_0.a < 10"' > stdout test `grep ' -> ' stdout | wc -l` = 19 test `grep 'P_0.a=' stdout | wc -l` = 15 -run 0 ../modelcheck -ddead -E $srcdir/finite.pm \ - '!(G(dead -> ("P_0.a==3" | "P_0.b==3")))' +run 0 ../modelcheck --is-empty --selfloopize dead --model $srcdir/finite.pm \ + --formula '!(G(dead -> ("P_0.a==3" | "P_0.b==3")))' -run 0 ../modelcheck -ddead -e $srcdir/finite.pm \ - '!(G(dead -> ("P_0.a==2" | "P_0.b==3")))' +run 1 ../modelcheck --is-empty --selfloopize dead --model $srcdir/finite.pm \ + --formula '!(G(dead -> ("P_0.a==2" | "P_0.b==3")))' -run 0 ../modelcheck -gp $srcdir/finite.pm true +run 0 ../modelcheck --dot product --model $srcdir/finite.pm --formula true diff --git a/tests/ltsmin/kripke.test b/tests/ltsmin/kripke.test index 7fffd403c..113c5e304 100755 --- a/tests/ltsmin/kripke.test +++ b/tests/ltsmin/kripke.test @@ -1,6 +1,6 @@ -#! /bin/sh + #! /bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2011, 2014, 2015 Laboratoire de Recherche et Developpement +# Copyright (C) 2011, 2014, 2015, 2016 Laboratoire de Recherche et Developpement # de l'Epita (LRDE) # # This file is part of Spot, a model checking library. @@ -33,10 +33,12 @@ fi set -e -run 0 ../modelcheck -gK $srcdir/finite.dve 'F("P.a > 5")' > output +run 0 ../modelcheck --kripke --model $srcdir/finite.dve \ + --formula 'F("P.a > 5")' > output run 0 ../../core/kripkecat output | tr -d '"' > output2 tr -d '"' < output >outputF cmp outputF output2 -../modelcheck -gK $srcdir/beem-peterson.4.dve '!G("pos[1] < 3")' > outputP +../modelcheck --kripke --model $srcdir/beem-peterson.4.dve \ + --formula '!G("pos[1] < 3")' > outputP ../../core/ikwiad -e -KPoutputP '!G("pos[1] < 3")' diff --git a/tests/ltsmin/modelcheck.cc b/tests/ltsmin/modelcheck.cc index c6f9bbdf6..63ca36cea 100644 --- a/tests/ltsmin/modelcheck.cc +++ b/tests/ltsmin/modelcheck.cc @@ -18,6 +18,10 @@ // along with this program. If not, see . #include "config.h" +#include "bin/common_conv.hh" +#include "bin/common_setup.hh" +#include "bin/common_output.hh" + #include #include #include @@ -32,128 +36,139 @@ #include #include -static void -syntax(char* prog) -{ - // Display the supplied name unless it appears to be a libtool wrapper. - char* slash = strrchr(prog, '/'); - if (slash && (strncmp(slash + 1, "lt-", 3) == 0)) - prog = slash + 4; +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"; + +unsigned DOT_MODEL = 1; +unsigned DOT_PRODUCT = 2; +unsigned DOT_FORMULA = 4; + +// 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; + bool kripke_output = false; +} mc_options; - std::cerr << "usage: " << prog << " [options] model formula\n\ -\n\ -Options:\n\ - -dDEAD use DEAD as property for marking DEAD states\n\ - (by default DEAD = true)\n\ - -e[ALGO] run emptiness check, expect an accepting run\n\ - -E[ALGO] run emptiness check, expect no accepting run\n\ - -C compute an accepting run (Counterexample) if it exists\n\ - -D favor a deterministic translation over a small transition\n\ - -gf output the automaton of the formula in dot format\n\ - -gm output the model state-space in dot format\n\ - -gK output the model state-space in Kripke format\n\ - -gp output the product state-space in dot format\n\ - -T time the different phases of the execution\n\ - -z compress states to handle larger models\n\ - -Z compress states (faster) assuming all values in [0 .. 2^28-1]\n\ -"; - exit(1); -} static int -checked_main(int argc, char **argv) +parse_opt_finput(int key, char* arg, struct argp_state*) { - spot::timer_map tm; - - bool use_timer = false; - - enum { DotFormula, DotModel, DotProduct, EmptinessCheck, Kripke } - output = EmptinessCheck; - bool accepting_run = false; - bool expect_counter_example = false; - bool deterministic = false; - char *dead = nullptr; - int compress_states = 0; - - const char* echeck_algo = "Cou99"; - - int dest = 1; - int n = argc; - for (int i = 1; i < n; ++i) + // This switch is alphabetically-ordered. + switch (key) { - char* opt = argv[i]; - if (*opt == '-') - { - switch (*++opt) - { - case 'C': - accepting_run = true; - break; - case 'd': - dead = opt + 1; - break; - case 'D': - deterministic = true; - break; - case 'e': - case 'E': - { - echeck_algo = opt + 1; - if (!*echeck_algo) - echeck_algo = "Cou99"; - - expect_counter_example = (*opt == 'e'); - output = EmptinessCheck; - break; - } - case 'g': - switch (opt[1]) - { - case 'm': - output = DotModel; - break; - case 'p': - output = DotProduct; - break; - case 'f': - output = DotFormula; - break; - case 'K': - output = Kripke; - break; - default: - goto error; - } - break; - case 'T': - use_timer = true; - break; - case 'z': - compress_states = 1; - break; - case 'Z': - compress_states = 2; - break; - default: - error: - std::cerr << "Unknown option `" << argv[i] << "'.\n"; - exit(1); - } - --argc; - } + case 'c': + mc_options.compute_counterexample = 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 - { - argv[dest++] = argv[i]; - } + { + 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 'k': + mc_options.kripke_output = true; + break; + case 'm': + mc_options.model = arg; + break; + case 's': + mc_options.dead_ap = arg; + break; + case 't': + mc_options.use_timer = true; + break; + case 'z': + mc_options.compress = to_unsigned(arg); + break; + default: + return ARGP_ERR_UNKNOWN; } + return 0; +} - if (argc != 3) - syntax(argv[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 }, + { "counterexample", 'c', nullptr, 0, + "compute an accepting counterexample (if it exists)", 0 }, + { "is-empty", 'e', nullptr, 0, + "check if the model meets its specification using " + "the (sequential) algorithm as described " + "in [Renault et al, LPAR'13]. Return 1 if a counterexample " + "is found." + , 0 }, + { "selfloopize", 's', "STRING", 0, + "use STRING as property for marking deadlock " + "states (by default selfloopize is activated with STRING='true')", 0 }, + { "timer", 't', nullptr, 0, + "time the different phases of the execution", 0 }, + // ------------------------------------------------------------ + { nullptr, 0, nullptr, 0, "Output options:", 3 }, + { "dot", 'd', "[model|product|formula]", 0, + "output the associated automaton in dot format", 0 }, + { "kripke", 'k', nullptr, 0, + "output the associated automaton in (internal) kripke 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 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; @@ -162,213 +177,198 @@ checked_main(int argc, char **argv) spot::emptiness_check_instantiator_ptr echeck_inst = nullptr; int exit_code = 0; spot::postprocessor post; - spot::formula deadf = nullptr; + spot::formula deadf = spot::formula::tt(); spot::formula f = nullptr; + spot::timer_map tm; - if (!dead || !strcasecmp(dead, "true")) + if (mc_options.selfloopize) { - deadf = spot::formula::tt(); - } - else if (!strcasecmp(dead, "false")) - { - deadf = spot::formula::ff(); - } - else - { - deadf = env.require(dead); + 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 (output == EmptinessCheck) + + if (mc_options.formula != nullptr) { - const char* err; - echeck_inst = spot::make_emptiness_check_instantiator(echeck_algo, &err); - if (!echeck_inst) - { - std::cerr << "Failed to parse argument of -e/-E near `" - << err << "'\n"; - exit_code = 1; - goto safe_exit; - } + 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"); + } } - tm.start("parsing formula"); - { - auto pf = spot::parse_infix_psl(argv[2], env, false); - exit_code = pf.format_errors(std::cerr); - f = pf.f; - } - tm.stop("parsing formula"); - - if (exit_code) - goto safe_exit; - - tm.start("translating formula"); - { - spot::translator trans(dict); - if (deterministic) - trans.set_pref(spot::postprocessor::Deterministic); - - prop = trans.run(&f); - } - tm.stop("translating formula"); - - atomic_prop_collect(f, &ap); - - if (output != DotFormula) + if (mc_options.model != nullptr) { tm.start("loading ltsmin model"); try - { - model = spot::ltsmin_model::load(argv[1]).kripke(&ap, dict, deadf, - compress_states); - } - catch (const std::runtime_error& e) + { + model = spot::ltsmin_model::load(mc_options.model) + .kripke(&ap, dict, deadf, mc_options.compress); + } + catch (std::runtime_error& e) { std::cerr << e.what() << '\n'; } tm.stop("loading ltsmin model"); if (!model) - { - exit_code = 1; - goto safe_exit; - } + { + exit_code = 2; + goto safe_exit; + } - if (output == DotModel) - { - tm.start("dot output"); - spot::print_dot(std::cout, model); - tm.stop("dot output"); - goto safe_exit; - } - if (output == Kripke) - { - tm.start("kripke output"); - spot::print_hoa(std::cout, model); - tm.stop("kripke output"); - 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.kripke_output) + { + tm.start("kripke output"); + spot::print_hoa(std::cout, model); + tm.stop("kripke output"); + } } - if (output == DotFormula) + if (mc_options.formula != nullptr && + mc_options.model != nullptr) { - tm.start("dot output"); - spot::print_dot(std::cout, prop); - tm.stop("dot output"); - goto safe_exit; + 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 (std::bad_alloc) + { + std::cerr << "Out of memory during emptiness check." + << std::endl; + if (!mc_options.compress) + std::cerr << "Try option -z for state compression." << std::endl; + 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"; + } + 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 (std::bad_alloc) + { + std::cerr << "Out of memory while looking for counterexample." + << std::endl; + 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.dot_output & DOT_PRODUCT) + { + tm.start("dot output"); + spot::print_dot(std::cout, product); + tm.stop("dot output"); + } } - product = spot::otf_product(model, prop); - - if (output == DotProduct) - { - tm.start("dot output"); - spot::print_dot(std::cout, product); - tm.stop("dot output"); - goto safe_exit; - } - - assert(echeck_inst); - - { - auto ec = echeck_inst->instantiate(product); - bool search_many = echeck_inst->options().get("repeated"); - assert(ec); - do - { - 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 (!compress_states) - 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 (expect_counter_example == !res && - (!expect_counter_example || ec->safe())) - exit_code = 1; - - if (!res) - { - std::cout << "no accepting run found"; - if (!ec->safe() && expect_counter_example) - { - std::cout << " even if expected" << std::endl; - std::cout << "this may be due to the use of the bit" - << " state hashing technique" << std::endl; - std::cout << "you can try to increase the heap size " - << "or use an explicit storage" - << std::endl; - } - std::cout << std::endl; - break; - } - else if (accepting_run) - { - - 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"); - } - } - else - { - std::cout << "an accepting run exists " - << "(use -C to print it)" << std::endl; - } - } - while (search_many); - } - safe_exit: - if (use_timer) + if (mc_options.use_timer) tm.print(std::cout); tm.reset_all(); // This helps valgrind. return exit_code; } + int -main(int argc, char **argv) +main(int argc, char** argv) { - auto exit_code = checked_main(argc, 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());