mc: bloemen emptiness check

* spot/mc/bloemen_ec.hh,
spot/mc/mc.hh,
tests/ltsmin/check.test,
tests/ltsmin/modelcheck.cc: here.

spot/mc/mc.hh

 // -*- coding: utf-8 -*-
-// Copyright (C) 2015, 2016, 2017 Laboratoire de Recherche et
+// Copyright (C) 2015, 2016, 2017, 2019 Laboratoire de Recherche et
 // Developpement de l'Epita
 //
 // This file is part of Spot, a model checking library.
@@ -29,6 +29,7 @@
 #include <spot/mc/ec.hh>
 #include <spot/mc/deadlock.hh>
 #include <spot/mc/bloemen.hh>
+#include <spot/mc/bloemen_ec.hh>
 #include <spot/misc/common.hh>
 #include <spot/misc/timer.hh>
 
@@ -232,4 +233,98 @@ namespace spot
       }
     return std::make_pair(stats, tm);
   }
+
+  /// \brief Perform the SCC computation algorithm of bloemen.16.ppopp
+  /// with emptiness check
+  template<typename kripke_ptr, typename State,
+           typename Iterator, typename Hash, typename Equal>
+  static std::tuple<bool,
+                    std::string,
+                    std::vector<bloemen_ec_stats>,
+                    spot::timer_map>
+  bloemen_ec(kripke_ptr sys, spot::twacube_ptr prop, bool compute_ctrx = false)
+  {
+    spot::timer_map tm;
+    using algo_name = spot::swarmed_bloemen_ec<State, Iterator, Hash, Equal>;
+    using uf_name = spot::iterable_uf_ec<State, Hash, Equal>;
+
+    unsigned  nbth = sys->get_threads();
+    typename uf_name::shared_map map;
+
+    tm.start("Initialisation");
+    std::vector<algo_name*> swarmed(nbth);
+    std::vector<uf_name*> ufs(nbth);
+    std::atomic<bool> stop(false);
+    for (unsigned i = 0; i < nbth; ++i)
+      {
+        ufs[i] = new uf_name(map, i);
+        swarmed[i] = new algo_name(*sys, prop, *ufs[i], i, stop);
+      }
+    tm.stop("Initialisation");
+
+    std::mutex iomutex;
+    std::atomic<bool> barrier(true);
+    std::vector<std::thread> threads(nbth);
+    for (unsigned i = 0; i < nbth; ++i)
+      {
+        threads[i] = std::thread ([&swarmed, &iomutex, i, & barrier]
+        {
+#if defined(unix) || defined(__unix__) || defined(__unix)
+            {
+              std::lock_guard<std::mutex> iolock(iomutex);
+              std::cout << "Thread #" << i
+                        << ": on CPU " << sched_getcpu() << '\n';
+            }
+#endif
+
+            // Wait all threads to be instanciated.
+            while (barrier)
+              continue;
+            swarmed[i]->run();
+         });
+
+#if defined(unix) || defined(__unix__) || defined(__unix)
+        //  Pins threads to a dedicated core.
+        cpu_set_t cpuset;
+        CPU_ZERO(&cpuset);
+        CPU_SET(i, &cpuset);
+        int rc = pthread_setaffinity_np(threads[i].native_handle(),
+                                        sizeof(cpu_set_t), &cpuset);
+        if (rc != 0)
+          {
+            std::lock_guard<std::mutex> iolock(iomutex);
+            std::cerr << "Error calling pthread_setaffinity_np: " << rc << '\n';
+          }
+#endif
+      }
+
+    tm.start("Run");
+    barrier.store(false);
+
+    for (auto& t : threads)
+      t.join();
+    tm.stop("Run");
+
+    std::string trace;
+    std::vector<bloemen_ec_stats> stats;
+    bool is_empty = true;
+    for (unsigned i = 0; i < sys->get_threads(); ++i)
+      {
+        if (!swarmed[i]->is_empty())
+          {
+            is_empty = false;
+            if (compute_ctrx)
+              trace = swarmed[i]->trace();
+          }
+
+        stats.push_back(swarmed[i]->stats());
+      }
+
+    for (unsigned i = 0; i < nbth; ++i)
+      {
+        delete swarmed[i];
+        delete ufs[i];
+      }
+    return std::make_tuple(is_empty, trace, stats, tm);
+  }
 }

tests/ltsmin/check.test

 #!/bin/sh
 # -*- coding: utf-8 -*-
-# Copyright (C) 2011, 2012, 2014, 2015, 2016, 2017 Laboratoire de Recherche
+# Copyright (C) 2011, 2012, 2014, 2015, 2016, 2017, 2019 Laboratoire de Recherche
 # et Développement de l'Epita (LRDE).
 #
 # This file is part of Spot, a model checking library.
@@ -91,3 +91,5 @@ run 0 ../modelcheck --model beem-peterson.4.dve2C \
     --csv --bloemen -p 3 >stdout
 test `grep "#" stdout | awk -F',' '{print $7}'` -eq 29115
 
+run 0 ../modelcheck --model beem-peterson.4.dve2C \
+    --formula '!GF(P_0.CS|P_1.CS|P_2.CS|P_3.CS)' --csv --bloemen-ec -p 3 >stdout

tests/ltsmin/modelcheck.cc

@@ -74,6 +74,7 @@ struct mc_options_
   bool csv = false;
   bool has_deadlock = false;
   bool bloemen = false;
+  bool bloemen_ec = false;
 } mc_options;
 
 
@@ -86,6 +87,9 @@ parse_opt_finput(int key, char* arg, struct argp_state*)
     case CSV:
       mc_options.csv = true;
       break;
+    case 'B':
+      mc_options.bloemen_ec = true;
+      break;
     case 'b':
       mc_options.bloemen = true;
       break;
@@ -150,6 +154,8 @@ static const argp_option options[] =
     { "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 SCC computation of Bloemen et al. (PPOPP'16) with EC", 0},
     { "bloemen", 'b', nullptr, 0,
       "run the SCC computation of Bloemen et al. (PPOPP'16)", 0 },
     { "counterexample", 'c', nullptr, 0,
@@ -297,7 +303,8 @@ static int checked_main()
 
   if (mc_options.nb_threads == 1 &&
       mc_options.formula != nullptr &&
-      mc_options.model != nullptr)
+      mc_options.model != nullptr &&
+      !mc_options.bloemen_ec)
     {
       product = spot::otf_product(model, prop);
 
@@ -409,7 +416,8 @@ static int checked_main()
 
     if (mc_options.nb_threads != 1 &&
         mc_options.formula != nullptr &&
-        mc_options.model != nullptr)
+        mc_options.model != nullptr &&
+        !mc_options.bloemen_ec)
     {
       unsigned int hc = std::thread::hardware_concurrency();
       if (mc_options.nb_threads > hc)
@@ -711,6 +719,126 @@ static int checked_main()
         }
       }
 
+    if (mc_options.bloemen_ec
+        && mc_options.model != nullptr && mc_options.formula != nullptr)
+      {
+        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";
+
+        tm.start("twa to twacube");
+        auto propcube = spot::twa_to_twacube(prop);
+        tm.stop("twa to twacube");
+
+        tm.start("load kripkecube");
+        spot::ltsmin_kripkecube_ptr modelcube = nullptr;
+        try
+          {
+            modelcube = spot::ltsmin_model::load(mc_options.model)
+              .kripkecube(propcube->get_ap(), 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("bloemen emptiness check");
+        auto res = spot::bloemen_ec<spot::ltsmin_kripkecube_ptr,
+                                    spot::cspins_state,
+                                    spot::cspins_iterator,
+                                    spot::cspins_state_hash,
+                                    spot::cspins_state_equal>
+          (modelcube, propcube);
+        tm.stop("bloemen emptiness check");
+        memused = spot::memusage() - memused;
+
+        if (!modelcube)
+          {
+            exit_code = 2;
+            goto safe_exit;
+          }
+
+        // Display statistics
+        unsigned sccs = 0;
+        unsigned st = 0;
+        unsigned tr = 0;
+        unsigned inserted = 0;
+        for (unsigned i = 0; i < std::get<2>(res).size(); ++i)
+          {
+            std::cout << "\n---- Thread number : " << i << '\n';
+            std::cout << std::get<2>(res)[i].states
+                      << " unique states visited\n";
+            std::cout << std::get<2>(res)[i].inserted
+                      << " unique states inserted\n";
+            std::cout << std::get<2>(res)[i].transitions
+                      << " transitions explored\n";
+            std::cout << std::get<2>(res)[i].sccs << " sccs found\n";
+            std::cout << std::get<2>(res)[i].walltime
+                      << " milliseconds\n";
+
+            sccs += std::get<2>(res)[i].sccs;
+            st += std::get<2>(res)[i].states;
+            tr += std::get<2>(res)[i].transitions;
+            inserted += std::get<2>(res)[i].inserted;
+
+            if (mc_options.csv)
+              {
+                std::cout << "Find following the csv: "
+                          << "thread_id,walltimems,type,"
+                          << "states,transitions,sccs\n";
+                std::cout << "@th_" << i << ','
+                          << std::get<2>(res)[i].walltime << ','
+                          << (std::get<2>(res)[i].is_empty ?
+                              "EMPTY," : "NONEMPTY,")
+                          << std::get<2>(res)[i].states << ','
+                          << std::get<2>(res)[i].inserted << ','
+                          << std::get<2>(res)[i].transitions << ','
+                          << std::get<2>(res)[i].sccs
+                          << std::endl;
+              }
+          }
+
+        if (mc_options.csv)
+          {
+            std::cout << "\nSummary :\n";
+            if (std::get<0>(res))
+              std::cout << "no accepting run 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"
+                        << std::get<1>(res) << '\n';
+
+
+            std::cout << "Find following the csv: "
+                      << "model,walltimems,memused,"
+                      << "type,inserted_states,"
+                      << "cumulated_states,cumulated_transitions,"
+                      << "cumulated_sccs\n";
+
+            std::cout << '#'
+                      << split_filename(mc_options.model)
+                      << ','
+                      << tm.timer("bloemen emptiness check").walltime() << ','
+                      << memused << ','
+                      << (std::get<0>(res) ? "EMPTY," : "NONEMPTY,")
+                      << inserted << ','
+                      << st << ','
+                      << tr << ','
+                      << sccs
+                      << '\n';
+          }
+      }
+
  safe_exit:
   if (mc_options.use_timer)
     tm.print(std::cout);