X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/3086f8693ca7977af2f666bca46f733046b22996..9d7dca1d2de1e6d67027e4ba33fefe1eb09550e3:/src/mc/LivenessChecker.cpp

diff --git a/src/mc/LivenessChecker.cpp b/src/mc/LivenessChecker.cpp
index 74751880bd..4f60bc148a 100644
--- a/src/mc/LivenessChecker.cpp
+++ b/src/mc/LivenessChecker.cpp
@@ -6,10 +6,11 @@
 
 #include <cstring>
 
-#include <algorithm>
 #include <memory>
 #include <list>
 
+#include <boost/range/algorithm.hpp>
+
 #include <unistd.h>
 #include <sys/wait.h>
 
@@ -30,6 +31,7 @@
 #include "src/mc/mc_safety.h"
 #include "src/mc/mc_exit.h"
 #include "src/mc/Transition.hpp"
+#include "src/mc/Session.hpp"
 
 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_liveness, mc,
                                 "Logging specific to algorithms for liveness properties verification");
@@ -93,7 +95,7 @@ static bool evaluate_label(
   }
 }
 
-Pair::Pair() : num(++mc_stats->expanded_pairs)
+Pair::Pair(unsigned long expanded_pairs) : num(expanded_pairs)
 {}
 
 Pair::~Pair() {}
@@ -123,7 +125,7 @@ std::shared_ptr<VisitedPair> LivenessChecker::insertAcceptancePair(simgrid::mc::
     pair->num, pair->automaton_state, pair->atomic_propositions,
     pair->graph_state);
 
-  auto res = std::equal_range(acceptancePairs_.begin(), acceptancePairs_.end(),
+  auto res = boost::range::equal_range(acceptancePairs_,
     new_pair.get(), simgrid::mc::DerefAndCompareByNbProcessesAndUsedHeap());
 
   if (pair->search_cycle) for (auto i = res.first; i != res.second; ++i) {
@@ -138,8 +140,8 @@ std::shared_ptr<VisitedPair> LivenessChecker::insertAcceptancePair(simgrid::mc::
     explorationStack_.pop_back();
     if (dot_output != nullptr)
       fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n",
-        initial_global_state->prev_pair, pair_test->num,
-        initial_global_state->prev_req.c_str());
+        this->previousPair_, pair_test->num,
+        this->previousRequest_.c_str());
     return nullptr;
   }
 
@@ -158,9 +160,7 @@ void LivenessChecker::removeAcceptancePair(int pair_num)
 
 void LivenessChecker::prepare(void)
 {
-  mc_model_checker->wait_for_requests();
-  initial_global_state->snapshot = simgrid::mc::take_snapshot(0);
-  initial_global_state->prev_pair = 0;
+  this->previousPair_ = 0;
 
   std::shared_ptr<const std::vector<int>> propos = this->getPropositionValues();
 
@@ -188,7 +188,7 @@ void LivenessChecker::replay()
   }
 
   /* Restore the initial state */
-  simgrid::mc::restore_snapshot(initial_global_state->snapshot);
+  simgrid::mc::session->restoreInitialState();
 
   /* Traverse the stack from the initial state and re-execute the transitions */
   int depth = 1;
@@ -219,13 +219,12 @@ void LivenessChecker::replay()
           state.get());
       }
 
-      mc_model_checker->handle_simcall(state->transition);
-      mc_model_checker->wait_for_requests();
+      this->getSession().execute(state->transition);
     }
 
     /* Update statistics */
-    mc_stats->visited_pairs++;
-    mc_stats->executed_transitions++;
+    visitedPairsCount_++;
+    mc_model_checker->executed_transitions++;
 
     depth++;
 
@@ -247,7 +246,7 @@ int LivenessChecker::insertVisitedPair(std::shared_ptr<VisitedPair> visited_pair
       pair->num, pair->automaton_state, pair->atomic_propositions,
       pair->graph_state);
 
-  auto range = std::equal_range(visitedPairs_.begin(), visitedPairs_.end(),
+  auto range = boost::range::equal_range(visitedPairs_,
     visited_pair.get(), simgrid::mc::DerefAndCompareByNbProcessesAndUsedHeap());
 
   for (auto i = range.first; i != range.second; ++i) {
@@ -279,8 +278,7 @@ void LivenessChecker::purgeVisitedPairs()
 {
   if (_sg_mc_visited != 0 && visitedPairs_.size() > (std::size_t) _sg_mc_visited) {
     // Remove the oldest entry with a linear search:
-    visitedPairs_.erase(std::min_element(
-      visitedPairs_.begin(), visitedPairs_.end(),
+    visitedPairs_.erase(boost::min_element(visitedPairs_,
       [](std::shared_ptr<VisitedPair> const a, std::shared_ptr<VisitedPair> const& b) {
         return a->num < b->num; } ));
   }
@@ -298,10 +296,18 @@ RecordTrace LivenessChecker::getRecordTrace() // override
 {
   RecordTrace res;
   for (std::shared_ptr<Pair> const& pair : explorationStack_)
-    res.push_back(pair->graph_state->getRecordElement());
+    res.push_back(pair->graph_state->getTransition());
   return res;
 }
 
+void LivenessChecker::logState() // override
+{
+  Checker::logState();
+  XBT_INFO("Expanded pairs = %lu", expandedPairsCount_);
+  XBT_INFO("Visited pairs = %lu", visitedPairsCount_);
+  XBT_INFO("Executed transitions = %lu", mc_model_checker->executed_transitions);
+}
+
 void LivenessChecker::showAcceptanceCycle(std::size_t depth)
 {
   XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
@@ -311,7 +317,7 @@ void LivenessChecker::showAcceptanceCycle(std::size_t depth)
   simgrid::mc::dumpRecordPath();
   for (auto& s : this->getTextualTrace())
     XBT_INFO("%s", s.c_str());
-  MC_print_statistics(mc_stats);
+  simgrid::mc::session->logState();
   XBT_INFO("Counter-example depth : %zd", depth);
 }
 
@@ -361,8 +367,8 @@ int LivenessChecker::main(void)
         reached_pair, current_pair.get())) != -1) {
       if (dot_output != nullptr){
         fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n",
-          initial_global_state->prev_pair, visited_num,
-          initial_global_state->prev_req.c_str());
+          this->previousPair_, visited_num,
+          this->previousRequest_.c_str());
         fflush(dot_output);
       }
       XBT_DEBUG("Pair already visited (equal to pair %d), exploration on the current path stopped.", visited_num);
@@ -375,14 +381,14 @@ int LivenessChecker::main(void)
     int req_num = current_pair->graph_state->transition.argument;
 
     if (dot_output != nullptr) {
-      if (initial_global_state->prev_pair != 0 && initial_global_state->prev_pair != current_pair->num) {
+      if (this->previousPair_ != 0 && this->previousPair_ != current_pair->num) {
         fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n",
-          initial_global_state->prev_pair, current_pair->num,
-          initial_global_state->prev_req.c_str());
-        initial_global_state->prev_req.clear();
+          this->previousPair_, current_pair->num,
+          this->previousRequest_.c_str());
+        this->previousRequest_.clear();
       }
-      initial_global_state->prev_pair = current_pair->num;
-      initial_global_state->prev_req = simgrid::mc::request_get_dot_output(req, req_num);
+      this->previousPair_ = current_pair->num;
+      this->previousRequest_ = simgrid::mc::request_get_dot_output(req, req_num);
       if (current_pair->search_cycle)
         fprintf(dot_output, "%d [shape=doublecircle];\n", current_pair->num);
       fflush(dot_output);
@@ -392,10 +398,10 @@ int LivenessChecker::main(void)
       simgrid::mc::request_to_string(
         req, req_num, simgrid::mc::RequestType::simix).c_str());
 
-    /* Update mc_stats */
-    mc_stats->executed_transitions++;
+    /* Update stats */
+    mc_model_checker->executed_transitions++;
     if (!current_pair->exploration_started)
-      mc_stats->visited_pairs++;
+      visitedPairsCount_++;
 
     /* Answer the request */
     mc_model_checker->handle_simcall(current_pair->graph_state->transition);
@@ -423,15 +429,15 @@ int LivenessChecker::main(void)
   }
 
   XBT_INFO("No property violation found.");
-  MC_print_statistics(mc_stats);
+  simgrid::mc::session->logState();
   return SIMGRID_MC_EXIT_SUCCESS;
 }
 
 std::shared_ptr<Pair> LivenessChecker::newPair(Pair* current_pair, xbt_automaton_state_t state, std::shared_ptr<const std::vector<int>> propositions)
 {
-  std::shared_ptr<Pair> next_pair = std::make_shared<Pair>();
+  std::shared_ptr<Pair> next_pair = std::make_shared<Pair>(++expandedPairsCount_);
   next_pair->automaton_state = state;
-  next_pair->graph_state = std::shared_ptr<simgrid::mc::State>(MC_state_new());
+  next_pair->graph_state = std::shared_ptr<simgrid::mc::State>(MC_state_new(++expandedStatesCount_));
   next_pair->atomic_propositions = std::move(propositions);
   if (current_pair)
     next_pair->depth = current_pair->depth + 1;
@@ -439,8 +445,8 @@ std::shared_ptr<Pair> LivenessChecker::newPair(Pair* current_pair, xbt_automaton
     next_pair->depth = 1;
   /* Get enabled processes and insert them in the interleave set of the next graph_state */
   for (auto& p : mc_model_checker->process().simix_processes())
-    if (simgrid::mc::process_is_enabled(&p.copy))
-      next_pair->graph_state->interleave(&p.copy);
+    if (simgrid::mc::process_is_enabled(p.copy.getBuffer()))
+      next_pair->graph_state->interleave(p.copy.getBuffer());
   next_pair->requests = next_pair->graph_state->interleaveSize();
   /* FIXME : get search_cycle value for each acceptant state */
   if (next_pair->automaton_state->type == 1 ||
@@ -477,16 +483,12 @@ int LivenessChecker::run()
 {
   XBT_INFO("Check the liveness property %s", _sg_mc_property_file);
   MC_automaton_load(_sg_mc_property_file);
-  mc_model_checker->wait_for_requests();
 
   XBT_DEBUG("Starting the liveness algorithm");
-
-  /* Create the initial state */
-  simgrid::mc::initial_global_state = std::unique_ptr<s_mc_global_t>(new s_mc_global_t());
-
+  simgrid::mc::session->initialize();
   this->prepare();
+
   int res = this->main();
-  simgrid::mc::initial_global_state = nullptr;
 
   return res;
 }