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

@@ -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 \
+ltsmin_modelcheck_LDADD =  \
-	$(LDADD) -lpthread
+  $(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
 

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 \
+  ../modelcheck --is-empty $opt --model $srcdir/beem-peterson.4.dve \
-    '!GF(P_0.CS|P_1.CS|P_2.CS|P_3.CS)' \
+		--formula '!GF(P_0.CS|P_1.CS|P_2.CS|P_3.CS)' \
-    | grep -v pages > stdout1
+      | grep -v pages > stdout1
   # same formula, different syntax.
-  ../modelcheck $opt -E $srcdir/beem-peterson.4.dve \
+  ../modelcheck --is-empty $opt --model $srcdir/beem-peterson.4.dve \
-    '!GF("P_0==CS"|"P_1 == CS"|"P_2 ==CS"|"P_3==  CS")' \
+		--formula '!GF("P_0==CS"|"P_1 == CS"|"P_2 ==CS"|"P_3==  CS")' \
-    | grep -v pages > stdout2
+      | grep -v pages > stdout2
   cmp stdout1 stdout2
-  run 0 ../modelcheck $opt -e $srcdir/beem-peterson.4.dve \
+  run 1 ../modelcheck --is-empty $opt --model $srcdir/beem-peterson.4.dve \
-    '!G(P_0.wait -> F P_0.CS)'
+      --formula '!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("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 \
+run 2 ../modelcheck --model beem-peterson.4.dve2C \
-        'Xfoo | P_0.f & X"P_0.k < 2xx" | G"pos[0]"' 2>stderr
+    --formula  'Xfoo | P_0.f & X"P_0.k < 2xx" | G"pos[0]"' 2>stderr
 cat stderr
-grep 'variable `foo' stderr
+grep 'Proposition "foo"' stderr
-grep "state \`f'.*P_0" stderr
+grep 'Proposition "P_0.f"' stderr
-grep "Unexpected.*\`xx'" stderr
+grep 'Proposition "P_0.k<2xx"' stderr
-grep 'Possible.*CS' stderr
-grep 'Possible.*NCS' stderr
-grep 'Possible.*q2' stderr
-grep 'Possible.*q3' stderr
-grep 'Possible.*wait' stderr

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 \
+run 0 ../modelcheck --is-empty --selfloopize dead --model $srcdir/finite.dve \
-  '!(G(dead -> ("P.a==3" | "P.b==3")))'
+    --formula '!(G(dead -> ("P.a==3" | "P.b==3")))'
 
-run 0 ../modelcheck -ddead -e $srcdir/finite.dve \
+run 1 ../modelcheck --is-empty --selfloopize dead --model $srcdir/finite.dve \
-  '!(G(dead -> ("P.a==2" | "P.b==3")))'
+    --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

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"' \
+run 0 ../modelcheck -compress --selfloopize false --dot model \
-> stdout
+    --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 \
+run 0 ../modelcheck --is-empty --selfloopize dead --model $srcdir/finite.pm \
-  '!(G(dead -> ("P_0.a==3" | "P_0.b==3")))'
+    --formula '!(G(dead -> ("P_0.a==3" | "P_0.b==3")))'
 
-run 0 ../modelcheck -ddead -e $srcdir/finite.pm \
+run 1 ../modelcheck --is-empty --selfloopize dead --model $srcdir/finite.pm \
-  '!(G(dead -> ("P_0.a==2" | "P_0.b==3")))'
+    --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

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")'

tests/ltsmin/modelcheck.cc

@@ -18,6 +18,10 @@
 // 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/twaalgos/dot.hh>
 #include <spot/tl/defaultenv.hh>
@@ -32,128 +36,139 @@
 #include <spot/kripke/kripkegraph.hh>
 #include <spot/twaalgos/hoa.hh>
 
-static void
+const char argp_program_doc[] =
-syntax(char* prog)
+"Process model and formula to check wether a "
-{
+"model meets a specification.\v\
-  // Display the supplied name unless it appears to be a libtool wrapper.
+Exit status:\n\
-  char* slash = strrchr(prog, '/');
+  0  No counterexample found\n\
-  if (slash && (strncmp(slash + 1, "lt-", 3) == 0))
+  1  A counterexample has been found\n\
-    prog = slash + 4;
+  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;
+  // This switch is alphabetically-ordered.
-
+  switch (key)
-  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)
     {
-      char* opt = argv[i];
+    case 'c':
-      if (*opt == '-')
+      mc_options.compute_counterexample = true;
-        {
+      break;
-          switch (*++opt)
+    case 'd':
-            {
+      if (strcmp(arg, "model") == 0)
-            case 'C':
+	mc_options.dot_output |= DOT_MODEL;
-              accepting_run = true;
+      else if (strcmp(arg, "product") == 0)
-              break;
+	mc_options.dot_output |= DOT_PRODUCT;
-            case 'd':
+      else if (strcmp(arg, "formula") == 0)
-              dead = opt + 1;
+	mc_options.dot_output |= DOT_FORMULA;
-              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;
-        }
       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)
+static const argp_option options[] =
-    syntax(argv[0]);
+  {
+    // 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();
+      if (mc_options.dead_ap == nullptr ||
-    }
+	  !strcasecmp(mc_options.dead_ap, "true"))
-  else if (!strcasecmp(dead, "false"))
+	deadf = spot::formula::tt();
-    {
+      else if (!strcasecmp(mc_options.dead_ap, "false"))
-      deadf = spot::formula::ff();
+	deadf = spot::formula::ff();
-    }
+      else
-  else
+	deadf = env.require(mc_options.dead_ap);
-    {
-      deadf = env.require(dead);
     }
 
-  if (output == EmptinessCheck)
+
+  if (mc_options.formula != nullptr)
     {
-      const char* err;
+      tm.start("parsing formula");
-      echeck_inst = spot::make_emptiness_check_instantiator(echeck_algo, &err);
+      {
-      if (!echeck_inst)
+	auto pf = spot::parse_infix_psl(mc_options.formula, env, false);
-        {
+	exit_code = pf.format_errors(std::cerr);
-          std::cerr << "Failed to parse argument of -e/-E near `"
+	f = pf.f;
-                    << err <<  "'\n";
+      }
-          exit_code = 1;
+      tm.stop("parsing formula");
-          goto safe_exit;
+
-        }
+      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");
+  if (mc_options.model != nullptr)
-  {
-    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)
     {
       tm.start("loading ltsmin model");
       try
-        {
+	{
-          model = spot::ltsmin_model::load(argv[1]).kripke(&ap, dict, deadf,
+	  model = spot::ltsmin_model::load(mc_options.model)
-                                                           compress_states);
+	    .kripke(&ap, dict, deadf, mc_options.compress);
-        }
+	}
-      catch (const std::runtime_error& e)
+      catch (std::runtime_error& e)
         {
           std::cerr << e.what() << '\n';
         }
       tm.stop("loading ltsmin model");
 
       if (!model)
-        {
+	{
-          exit_code = 1;
+	  exit_code = 2;
-          goto safe_exit;
+	  goto safe_exit;
-        }
+	}
 
-      if (output == DotModel)
+      if (mc_options.dot_output & DOT_MODEL)
-        {
+	{
-          tm.start("dot output");
+	  tm.start("dot output");
-          spot::print_dot(std::cout, model);
+	  spot::print_dot(std::cout, model);
-          tm.stop("dot output");
+	  tm.stop("dot output");
-          goto safe_exit;
+	}
-        }
+      if (mc_options.kripke_output)
-      if (output == Kripke)
+	{
-      {
+	  tm.start("kripke output");
-        tm.start("kripke output");
+	  spot::print_hoa(std::cout, model);
-        spot::print_hoa(std::cout, model);
+	  tm.stop("kripke output");
-        tm.stop("kripke output");
+	}
-        goto safe_exit;
-      }
     }
 
-  if (output == DotFormula)
+  if (mc_options.formula != nullptr &&
+      mc_options.model != nullptr)
     {
-      tm.start("dot output");
+      product = spot::otf_product(model, prop);
-      spot::print_dot(std::cout, prop);
+
-      tm.stop("dot output");
+      if (mc_options.is_empty)
-      goto safe_exit;
+	{
+	  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());