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

@@ -41,7 +41,6 @@
 #include <spot/twaalgos/reachiter.hh>
 #include <string.h>
 #include <spot/mc/utils.hh>
-#include <spot/mc/ec.hh>
 
 using namespace std::string_literals;
 
@@ -1122,45 +1121,6 @@ namespace spot
   {
   }
 
-  std::tuple<bool, std::string, std::vector<istats>>
-  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<ec_renault13lpar<cspins_state, cspins_iterator,
-                                 cspins_state_hash, cspins_state_equal>> ecs;
-    for (unsigned i = 0; i < sys->get_threads(); ++i)
-      ecs.push_back({*sys, twa, i, stop});
-
-    std::vector<std::thread> threads;
-    for (unsigned i = 0; i < sys->get_threads(); ++i)
-      threads.push_back
-        (std::thread(&ec_renault13lpar<cspins_state, cspins_iterator,
-                     cspins_state_hash, cspins_state_equal>::run, &ecs[i]));
-
-    for (unsigned i = 0; i < sys->get_threads(); ++i)
-      threads[i].join();
-
-    bool has_ctrx = false;
-    std::string trace = "";
-    std::vector<istats> 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();

spot/ltsmin/ltsmin.hh

@@ -25,7 +25,6 @@
 #include <spot/twacube/twacube.hh>
 #include <spot/tl/apcollect.hh>
 #include <tuple>
-#include <spot/mc/intersect.hh>
 
 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<bool, std::string, std::vector<istats>>
-    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

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
 

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 <http://www.gnu.org/licenses/>.
+
+#pragma once
+
+#include <string>
+#include <thread>
+#include <tuple>
+#include <vector>
+#include <spot/kripke/kripke.hh>
+#include <spot/mc/ec.hh>
+#include <spot/misc/common.hh>
+
+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<typename kripke_ptr, typename State,
+           typename Iterator, typename Hash, typename Equal>
+  static std::tuple<bool, std::string, std::vector<istats>>
+  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<ec_renault13lpar<State, Iterator, Hash, Equal>> ecs;
+    for (unsigned i = 0; i < sys->get_threads(); ++i)
+      ecs.push_back({*sys, twa, i, stop});
+
+    std::vector<std::thread> threads;
+    for (unsigned i = 0; i < sys->get_threads(); ++i)
+      threads.push_back
+        (std::thread(&ec_renault13lpar<State, Iterator, Hash, Equal>::run,
+                     &ecs[i]));
+
+    for (unsigned i = 0; i < sys->get_threads(); ++i)
+      threads[i].join();
+
+    bool has_ctrx = false;
+    std::string trace = "";
+     std::vector<istats> 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);
+  }
+}

tests/ltsmin/modelcheck.cc

@@ -23,6 +23,8 @@
 #include "bin/common_output.hh"
 
 #include <spot/ltsmin/ltsmin.hh>
+#include <spot/ltsmin/spins_kripke.hh>
+#include <spot/mc/mc.hh>
 #include <spot/twaalgos/dot.hh>
 #include <spot/tl/defaultenv.hh>
 #include <spot/tl/parse.hh>
@@ -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<spot::ltsmin_kripkecube_ptr,
+                                  spot::cspins_state,
+                                  spot::cspins_iterator,
+                                  spot::cspins_state_hash,
+                                  spot::cspins_state_equal>
         (modelcube, propcube, mc_options.compute_counterexample);
       tm.stop("emptiness check");
       memused = spot::memusage() - memused;