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());