X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/4241b524e565e4fb4a3f1a4fa24d1d05106ee7cb..2b32f4ae7739666694f8f27ff5122c829daa94dc:/src/mc/LivenessChecker.cpp

diff --git a/src/mc/LivenessChecker.cpp b/src/mc/LivenessChecker.cpp
index dd526a306b..cc3ae5dc8d 100644
--- a/src/mc/LivenessChecker.cpp
+++ b/src/mc/LivenessChecker.cpp
@@ -8,6 +8,7 @@
 
 #include <algorithm>
 #include <memory>
+#include <list>
 
 #include <unistd.h>
 #include <sys/wait.h>
@@ -15,7 +16,6 @@
 #include <xbt/automaton.h>
 #include <xbt/dynar.h>
 #include <xbt/dynar.hpp>
-#include <xbt/fifo.h>
 #include <xbt/log.h>
 #include <xbt/sysdep.h>
 
@@ -33,21 +33,18 @@
 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_liveness, mc,
                                 "Logging specific to algorithms for liveness properties verification");
 
-/********* Global variables *********/
-
-xbt_dynar_t acceptance_pairs;
-static xbt_fifo_t liveness_stack;
-
 /********* Static functions *********/
 
 namespace simgrid {
 namespace mc {
 
-VisitedPair::VisitedPair(int pair_num, xbt_automaton_state_t automaton_state, xbt_dynar_t atomic_propositions, simgrid::mc::State* graph_state)
+VisitedPair::VisitedPair(
+  int pair_num, xbt_automaton_state_t automaton_state,
+  std::vector<int> const& atomic_propositions, std::shared_ptr<simgrid::mc::State> graph_state)
 {
   simgrid::mc::Process* process = &(mc_model_checker->process());
 
-  this->graph_state = graph_state;
+  this->graph_state = std::move(graph_state);
   if(this->graph_state->system_state == nullptr)
     this->graph_state->system_state = simgrid::mc::take_snapshot(pair_num);
   this->heap_bytes_used = mmalloc_get_bytes_used_remote(
@@ -60,91 +57,66 @@ VisitedPair::VisitedPair(int pair_num, xbt_automaton_state_t automaton_state, xb
   this->automaton_state = automaton_state;
   this->num = pair_num;
   this->other_num = -1;
-  this->acceptance_removed = 0;
-  this->visited_removed = 0;
-  this->acceptance_pair = 0;
-  this->atomic_propositions = simgrid::xbt::unique_ptr<s_xbt_dynar_t>(
-    xbt_dynar_new(sizeof(int), nullptr));
-
-  unsigned int cursor = 0;
-  int value;
-  xbt_dynar_foreach(atomic_propositions, cursor, value)
-      xbt_dynar_push_as(this->atomic_propositions.get(), int, value);
-}
-
-static int is_exploration_stack_pair(simgrid::mc::VisitedPair* pair){
-  xbt_fifo_item_t item = xbt_fifo_get_first_item(liveness_stack);
-  while (item) {
-    if (((simgrid::mc::Pair*)xbt_fifo_get_item_content(item))->num == pair->num){
-      ((simgrid::mc::Pair*)xbt_fifo_get_item_content(item))->visited_pair_removed = 1;
-      return 1;
-    }
-    item = xbt_fifo_get_next_item(item);
-  }
-  return 0;
+  this->atomic_propositions = atomic_propositions;
 }
 
 VisitedPair::~VisitedPair()
 {
-  if( !is_exploration_stack_pair(this))
-    MC_state_delete(this->graph_state, 1);
 }
 
-static int MC_automaton_evaluate_label(xbt_automaton_exp_label_t l,
-                                       xbt_dynar_t atomic_propositions_values)
+static int MC_automaton_evaluate_label(
+  xbt_automaton_exp_label_t l,
+  std::vector<int> const& atomic_propositions_values)
 {
 
   switch (l->type) {
-  case 0:{
-      int left_res = MC_automaton_evaluate_label(l->u.or_and.left_exp, atomic_propositions_values);
-      int right_res = MC_automaton_evaluate_label(l->u.or_and.right_exp, atomic_propositions_values);
+  case xbt_automaton_exp_label::AUT_OR:{
+      int left_res = MC_automaton_evaluate_label(
+        l->u.or_and.left_exp, atomic_propositions_values);
+      int right_res = MC_automaton_evaluate_label(
+        l->u.or_and.right_exp, atomic_propositions_values);
       return (left_res || right_res);
     }
-  case 1:{
-      int left_res = MC_automaton_evaluate_label(l->u.or_and.left_exp, atomic_propositions_values);
-      int right_res = MC_automaton_evaluate_label(l->u.or_and.right_exp, atomic_propositions_values);
+  case xbt_automaton_exp_label::AUT_AND:{
+      int left_res = MC_automaton_evaluate_label(
+        l->u.or_and.left_exp, atomic_propositions_values);
+      int right_res = MC_automaton_evaluate_label(
+        l->u.or_and.right_exp, atomic_propositions_values);
       return (left_res && right_res);
     }
-  case 2:{
-      int res = MC_automaton_evaluate_label(l->u.exp_not, atomic_propositions_values);
+  case xbt_automaton_exp_label::AUT_NOT:{
+      int res = MC_automaton_evaluate_label(
+        l->u.exp_not, atomic_propositions_values);
       return (!res);
     }
-  case 3:{
+  case xbt_automaton_exp_label::AUT_PREDICAT:{
       unsigned int cursor = 0;
       xbt_automaton_propositional_symbol_t p = nullptr;
       xbt_dynar_foreach(simgrid::mc::property_automaton->propositional_symbols, cursor, p) {
         if (std::strcmp(xbt_automaton_propositional_symbol_get_name(p), l->u.predicat) == 0)
-          return (int) xbt_dynar_get_as(atomic_propositions_values, cursor, int);
+          return atomic_propositions_values[cursor];
       }
       return -1;
     }
-  case 4:
+  case xbt_automaton_exp_label::AUT_ONE:
     return 2;
   default:
     return -1;
   }
 }
 
-static xbt_dynar_t visited_pairs;
-
-Pair::Pair() : num(++mc_stats->expanded_pairs),
-  visited_pair_removed(_sg_mc_visited > 0 ? 0 : 1)
+Pair::Pair() : num(++mc_stats->expanded_pairs)
 {}
 
-Pair::~Pair() {
-  if (this->visited_pair_removed)
-    MC_state_delete(this->graph_state, 1);
-}
+Pair::~Pair() {}
 
-simgrid::xbt::unique_ptr<s_xbt_dynar_t> LivenessChecker::getPropositionValues()
+std::vector<int> LivenessChecker::getPropositionValues()
 {
+  std::vector<int> values;
   unsigned int cursor = 0;
   xbt_automaton_propositional_symbol_t ps = nullptr;
-  simgrid::xbt::unique_ptr<s_xbt_dynar_t> values = simgrid::xbt::unique_ptr<s_xbt_dynar_t>(xbt_dynar_new(sizeof(int), nullptr));
-  xbt_dynar_foreach(simgrid::mc::property_automaton->propositional_symbols, cursor, ps) {
-    int res = xbt_automaton_propositional_symbol_evaluate(ps);
-    xbt_dynar_push_as(values.get(), int, res);
-  }
+  xbt_dynar_foreach(simgrid::mc::property_automaton->propositional_symbols, cursor, ps)
+    values.push_back(xbt_automaton_propositional_symbol_evaluate(ps));
   return values;
 }
 
@@ -157,28 +129,23 @@ int LivenessChecker::compare(simgrid::mc::VisitedPair* state1, simgrid::mc::Visi
   return simgrid::mc::snapshot_compare(num1, s1, num2, s2);
 }
 
-simgrid::mc::VisitedPair* LivenessChecker::insertAcceptancePair(simgrid::mc::Pair* pair)
+std::shared_ptr<VisitedPair> LivenessChecker::insertAcceptancePair(simgrid::mc::Pair* pair)
 {
-  auto acceptance_pairs = simgrid::xbt::range<simgrid::mc::VisitedPair*>(::acceptance_pairs);
-  auto new_pair =
-    std::unique_ptr<simgrid::mc::VisitedPair>(new VisitedPair(
-      pair->num, pair->automaton_state, pair->atomic_propositions.get(),
-      pair->graph_state));
-  new_pair->acceptance_pair = 1;
+  std::shared_ptr<VisitedPair> new_pair = std::make_shared<VisitedPair>(
+    pair->num, pair->automaton_state, pair->atomic_propositions,
+    pair->graph_state);
 
-  auto res = std::equal_range(acceptance_pairs.begin(), acceptance_pairs.end(),
-    new_pair, simgrid::mc::DerefAndCompareByNbProcessesAndUsedHeap());
+  auto res = std::equal_range(acceptancePairs_.begin(), acceptancePairs_.end(),
+    new_pair.get(), simgrid::mc::DerefAndCompareByNbProcessesAndUsedHeap());
 
-  if (pair->search_cycle == 1)
+  if (pair->search_cycle)
     for (auto i = res.first; i != res.second; ++i) {
-      simgrid::mc::VisitedPair* pair_test = *i;
+      std::shared_ptr<simgrid::mc::VisitedPair> const& pair_test = *i;
       if (xbt_automaton_state_compare(pair_test->automaton_state, new_pair->automaton_state) == 0) {
-        if (xbt_automaton_propositional_symbols_compare_value(
-            pair_test->atomic_propositions.get(),
-            new_pair->atomic_propositions.get()) == 0) {
-          if (this->compare(pair_test, new_pair.get()) == 0) {
+        if (pair_test->atomic_propositions == new_pair->atomic_propositions) {
+          if (this->compare(pair_test.get(), new_pair.get()) == 0) {
             XBT_INFO("Pair %d already reached (equal to pair %d) !", new_pair->num, pair_test->num);
-            xbt_fifo_shift(liveness_stack);
+            livenessStack_.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);
             return nullptr;
@@ -187,42 +154,23 @@ simgrid::mc::VisitedPair* LivenessChecker::insertAcceptancePair(simgrid::mc::Pai
       }
     }
 
-  auto new_raw_pair = new_pair.release();
-  xbt_dynar_insert_at(
-    ::acceptance_pairs, res.first - acceptance_pairs.begin(), &new_raw_pair);
-  return new_raw_pair;
+  acceptancePairs_.insert(res.first, new_pair);
+  return new_pair;
 }
 
 void LivenessChecker::removeAcceptancePair(int pair_num)
 {
-  unsigned int cursor = 0;
-  simgrid::mc::VisitedPair* pair_test = nullptr;
-  int pair_found = 0;
-
-  xbt_dynar_foreach(acceptance_pairs, cursor, pair_test)
-    if (pair_test->num == pair_num) {
-       pair_found = 1;
+  for (auto i = acceptancePairs_.begin(); i != acceptancePairs_.end(); ++i)
+    if ((*i)->num == pair_num) {
+      acceptancePairs_.erase(i);
       break;
     }
-
-  if(pair_found == 1) {
-    xbt_dynar_remove_at(acceptance_pairs, cursor, &pair_test);
-
-    pair_test->acceptance_removed = 1;
-
-    if (_sg_mc_visited == 0 || pair_test->visited_removed == 1) 
-      delete pair_test;
-
-  }
 }
 
 void LivenessChecker::prepare(void)
 {
   simgrid::mc::Pair* initial_pair = nullptr;
   mc_model_checker->wait_for_requests();
-  acceptance_pairs = xbt_dynar_new(sizeof(simgrid::mc::VisitedPair*), nullptr);
-  if(_sg_mc_visited > 0)
-    simgrid::mc::visited_pairs = xbt_dynar_new(sizeof(simgrid::mc::VisitedPair*), nullptr);
 
   initial_global_state->snapshot = simgrid::mc::take_snapshot(0);
   initial_global_state->prev_pair = 0;
@@ -235,29 +183,26 @@ void LivenessChecker::prepare(void)
 
       initial_pair = new Pair();
       initial_pair->automaton_state = automaton_state;
-      initial_pair->graph_state = MC_state_new();
+      initial_pair->graph_state = std::shared_ptr<simgrid::mc::State>(MC_state_new());
       initial_pair->atomic_propositions = this->getPropositionValues();
       initial_pair->depth = 1;
 
       /* Get enabled processes and insert them in the interleave set of the graph_state */
       for (auto& p : mc_model_checker->process().simix_processes())
         if (simgrid::mc::process_is_enabled(&p.copy))
-          MC_state_interleave_process(initial_pair->graph_state, &p.copy);
+          MC_state_interleave_process(initial_pair->graph_state.get(), &p.copy);
 
-      initial_pair->requests = MC_state_interleave_size(initial_pair->graph_state);
-      initial_pair->search_cycle = 0;
+      initial_pair->requests = MC_state_interleave_size(initial_pair->graph_state.get());
+      initial_pair->search_cycle = false;
 
-      xbt_fifo_unshift(liveness_stack, initial_pair);
+      livenessStack_.push_back(initial_pair);
     }
   }
 }
 
 
-void LivenessChecker::replay(xbt_fifo_t stack)
+void LivenessChecker::replay()
 {
-  xbt_fifo_item_t item;
-  simgrid::mc::Pair* pair = nullptr;
-  simgrid::mc::State* state = nullptr;
   smx_simcall_t req = nullptr, saved_req = NULL;
   int value, depth = 1;
   char *req_str;
@@ -266,8 +211,7 @@ void LivenessChecker::replay(xbt_fifo_t stack)
 
   /* Intermediate backtracking */
   if(_sg_mc_checkpoint > 0) {
-    item = xbt_fifo_get_first_item(stack);
-    pair = (simgrid::mc::Pair*) xbt_fifo_get_item_content(item);
+    simgrid::mc::Pair* pair = livenessStack_.back();
     if(pair->graph_state->system_state){
       simgrid::mc::restore_snapshot(pair->graph_state->system_state);
       return;
@@ -277,18 +221,16 @@ void LivenessChecker::replay(xbt_fifo_t stack)
   /* Restore the initial state */
   simgrid::mc::restore_snapshot(initial_global_state->snapshot);
 
-    /* Traverse the stack from the initial state and re-execute the transitions */
-    for (item = xbt_fifo_get_last_item(stack);
-         item != xbt_fifo_get_first_item(stack);
-         item = xbt_fifo_get_prev_item(item)) {
-
-      pair = (simgrid::mc::Pair*) xbt_fifo_get_item_content(item);
+  /* Traverse the stack from the initial state and re-execute the transitions */
+  for (simgrid::mc::Pair* pair : livenessStack_) {
+    if (pair == livenessStack_.back())
+      break;
 
-      state = (simgrid::mc::State*) pair->graph_state;
+      std::shared_ptr<State> state = pair->graph_state;
 
       if (pair->exploration_started) {
 
-        saved_req = MC_state_get_executed_request(state, &value);
+        saved_req = MC_state_get_executed_request(state.get(), &value);
 
         if (saved_req != nullptr) {
           /* because we got a copy of the executed request, we have to fetch the
@@ -299,7 +241,7 @@ void LivenessChecker::replay(xbt_fifo_t stack)
           /* Debug information */
           if (XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug)) {
             req_str = simgrid::mc::request_to_string(req, value, simgrid::mc::RequestType::simix);
-            XBT_DEBUG("Replay (depth = %d) : %s (%p)", depth, req_str, state);
+            XBT_DEBUG("Replay (depth = %d) : %s (%p)", depth, req_str, state.get());
             xbt_free(req_str);
           }
 
@@ -315,7 +257,7 @@ void LivenessChecker::replay(xbt_fifo_t stack)
 
       depth++;
 
-    }
+  }
 
   XBT_DEBUG("**** End Replay ****");
 }
@@ -323,69 +265,55 @@ void LivenessChecker::replay(xbt_fifo_t stack)
 /**
  * \brief Checks whether a given pair has already been visited by the algorithm.
  */
-int LivenessChecker::insertVisitedPair(simgrid::mc::VisitedPair* visited_pair, simgrid::mc::Pair* pair)
+int LivenessChecker::insertVisitedPair(std::shared_ptr<VisitedPair> visited_pair, simgrid::mc::Pair* pair)
 {
   if (_sg_mc_visited == 0)
     return -1;
 
-  simgrid::mc::VisitedPair* new_visited_pair = nullptr;
   if (visited_pair == nullptr)
-    new_visited_pair = new simgrid::mc::VisitedPair(
-      pair->num, pair->automaton_state, pair->atomic_propositions.get(),
+    visited_pair = std::make_shared<VisitedPair>(
+      pair->num, pair->automaton_state, pair->atomic_propositions,
       pair->graph_state);
-  else
-    new_visited_pair = visited_pair;
 
-  auto visited_pairs = simgrid::xbt::range<simgrid::mc::VisitedPair*>(simgrid::mc::visited_pairs);
-
-  auto range = std::equal_range(visited_pairs.begin(), visited_pairs.end(),
-    new_visited_pair, simgrid::mc::DerefAndCompareByNbProcessesAndUsedHeap());
+  auto range = std::equal_range(visitedPairs_.begin(), visitedPairs_.end(),
+    visited_pair.get(), simgrid::mc::DerefAndCompareByNbProcessesAndUsedHeap());
 
   for (auto i = range.first; i != range.second; ++i) {
-    simgrid::mc::VisitedPair* pair_test = *i;
-    std::size_t cursor = i - visited_pairs.begin();
-    if (xbt_automaton_state_compare(pair_test->automaton_state, new_visited_pair->automaton_state) == 0) {
-      if (xbt_automaton_propositional_symbols_compare_value(
-          pair_test->atomic_propositions.get(),
-          new_visited_pair->atomic_propositions.get()) == 0) {
-        if (this->compare(pair_test, new_visited_pair) == 0) {
+    VisitedPair* pair_test = i->get();
+    if (xbt_automaton_state_compare(pair_test->automaton_state, visited_pair->automaton_state) == 0) {
+      if (pair_test->atomic_propositions == visited_pair->atomic_propositions) {
+        if (this->compare(pair_test, visited_pair.get()) == 0) {
           if (pair_test->other_num == -1)
-            new_visited_pair->other_num = pair_test->num;
+            visited_pair->other_num = pair_test->num;
           else
-            new_visited_pair->other_num = pair_test->other_num;
+            visited_pair->other_num = pair_test->other_num;
           if (dot_output == nullptr)
-            XBT_DEBUG("Pair %d already visited ! (equal to pair %d)", new_visited_pair->num, pair_test->num);
+            XBT_DEBUG("Pair %d already visited ! (equal to pair %d)",
+            visited_pair->num, pair_test->num);
           else
-            XBT_DEBUG("Pair %d already visited ! (equal to pair %d (pair %d in dot_output))", new_visited_pair->num, pair_test->num, new_visited_pair->other_num);
-          xbt_dynar_remove_at(simgrid::mc::visited_pairs, cursor, &pair_test);
-          xbt_dynar_insert_at(simgrid::mc::visited_pairs, cursor, &new_visited_pair);
-          pair_test->visited_removed = 1;
-          if (!pair_test->acceptance_pair
-              || pair_test->acceptance_removed == 1)
-            delete pair_test;
-          return new_visited_pair->other_num;
+            XBT_DEBUG("Pair %d already visited ! (equal to pair %d (pair %d in dot_output))",
+              visited_pair->num, pair_test->num, visited_pair->other_num);
+          (*i) = std::move(visited_pair);
+          return (*i)->other_num;
         }
       }
     }
   }
 
-  xbt_dynar_insert_at(simgrid::mc::visited_pairs, range.first - visited_pairs.begin(), &new_visited_pair);
+  visitedPairs_.insert(range.first, std::move(visited_pair));
 
-  if ((ssize_t) visited_pairs.size() > _sg_mc_visited) {
+  if (visitedPairs_.size() > (std::size_t) _sg_mc_visited) {
     int min2 = mc_stats->expanded_pairs;
-    unsigned int index2 = 0;
-    for (std::size_t i = 0; i != (std::size_t) visited_pairs.size(); ++i) {
-      simgrid::mc::VisitedPair* pair_test = visited_pairs[i];
-      if (pair_test->num < min2) {
+
+    std::list<std::shared_ptr<VisitedPair>>::iterator index2;
+    for (auto i = visitedPairs_.begin(); i != visitedPairs_.end(); ++i) {
+      if ((*i)->num < min2) {
         index2 = i;
-        min2 = pair_test->num;
+        min2 = (*i)->num;
       }
     }
-    simgrid::mc::VisitedPair* pair_test = nullptr;
-    xbt_dynar_remove_at(simgrid::mc::visited_pairs, index2, &pair_test);
-    pair_test->visited_removed = 1;
-    if (!pair_test->acceptance_pair || pair_test->acceptance_removed)
-      delete pair_test;
+
+    visitedPairs_.erase(index2);
   }
 
   return -1;
@@ -402,12 +330,9 @@ LivenessChecker::~LivenessChecker()
 RecordTrace LivenessChecker::getRecordTrace() // override
 {
   RecordTrace res;
-
-  xbt_fifo_item_t start = xbt_fifo_get_last_item(liveness_stack);
-  for (xbt_fifo_item_t item = start; item; item = xbt_fifo_get_prev_item(item)) {
-    simgrid::mc::Pair* pair = (simgrid::mc::Pair*) xbt_fifo_get_item_content(item);
+  for (simgrid::mc::Pair* pair : livenessStack_) {
     int value;
-    smx_simcall_t req = MC_state_get_executed_request(pair->graph_state, &value);
+    smx_simcall_t req = MC_state_get_executed_request(pair->graph_state.get(), &value);
     if (req && req->call != SIMCALL_NONE) {
       smx_process_t issuer = MC_smx_simcall_get_issuer(req);
       const int pid = issuer->pid;
@@ -416,7 +341,6 @@ RecordTrace LivenessChecker::getRecordTrace() // override
       res.push_back(RecordTraceElement(pid, value));
     }
   }
-
   return res;
 }
 
@@ -436,11 +360,9 @@ void LivenessChecker::showAcceptanceCycle(std::size_t depth)
 std::vector<std::string> LivenessChecker::getTextualTrace() // override
 {
   std::vector<std::string> trace;
-  for (xbt_fifo_item_t item = xbt_fifo_get_last_item(liveness_stack);
-       item; item = xbt_fifo_get_prev_item(item)) {
-    simgrid::mc::Pair* pair = (simgrid::mc::Pair*) xbt_fifo_get_item_content(item);
+  for (simgrid::mc::Pair* pair : livenessStack_) {
     int value;
-    smx_simcall_t req = MC_state_get_executed_request(pair->graph_state, &value);
+    smx_simcall_t req = MC_state_get_executed_request(pair->graph_state.get(), &value);
     if (req && req->call != SIMCALL_NONE) {
       char* req_str = simgrid::mc::request_to_string(req, value, simgrid::mc::RequestType::executed);
       trace.push_back(std::string(req_str));
@@ -457,26 +379,24 @@ int LivenessChecker::main(void)
   smx_simcall_t req = nullptr;
   xbt_automaton_transition_t transition_succ = nullptr;
   int cursor = 0;
-  simgrid::mc::Pair* next_pair = nullptr;
-  simgrid::xbt::unique_ptr<s_xbt_dynar_t> prop_values;
-  simgrid::mc::VisitedPair* reached_pair = nullptr;
+  std::shared_ptr<VisitedPair> reached_pair = nullptr;
 
-  while(xbt_fifo_size(liveness_stack) > 0){
+  while (!livenessStack_.empty()){
 
     /* Get current pair */
-    current_pair = (simgrid::mc::Pair*) xbt_fifo_get_item_content(xbt_fifo_get_first_item(liveness_stack));
+    current_pair = livenessStack_.back();
 
     /* Update current state in buchi automaton */
     simgrid::mc::property_automaton->current_state = current_pair->automaton_state;
 
     XBT_DEBUG("********************* ( Depth = %d, search_cycle = %d, interleave size = %d, pair_num = %d, requests = %d)",
        current_pair->depth, current_pair->search_cycle,
-       MC_state_interleave_size(current_pair->graph_state), current_pair->num,
+       MC_state_interleave_size(current_pair->graph_state.get()), current_pair->num,
        current_pair->requests);
 
     if (current_pair->requests > 0) {
 
-      if (current_pair->automaton_state->type == 1 && current_pair->exploration_started == 0) {
+      if (current_pair->automaton_state->type == 1 && !current_pair->exploration_started) {
         /* If new acceptance pair, return new pair */
         if ((reached_pair = this->insertAcceptancePair(current_pair)) == nullptr) {
           this->showAcceptanceCycle(current_pair->depth);
@@ -485,7 +405,7 @@ int LivenessChecker::main(void)
       }
 
       /* Pair already visited ? stop the exploration on the current path */
-      if ((current_pair->exploration_started == 0)
+      if ((!current_pair->exploration_started)
         && (visited_num = this->insertVisitedPair(
           reached_pair, current_pair)) != -1) {
 
@@ -500,7 +420,7 @@ int LivenessChecker::main(void)
 
       }else{
 
-        req = MC_state_get_request(current_pair->graph_state, &value);
+        req = MC_state_get_request(current_pair->graph_state.get(), &value);
 
          if (dot_output != nullptr) {
            if (initial_global_state->prev_pair != 0 && initial_global_state->prev_pair != current_pair->num) {
@@ -519,11 +439,11 @@ int LivenessChecker::main(void)
          xbt_free(req_str);
 
          /* Set request as executed */
-         MC_state_set_executed_request(current_pair->graph_state, req, value);
+         MC_state_set_executed_request(current_pair->graph_state.get(), req, value);
 
          /* Update mc_stats */
          mc_stats->executed_transitions++;
-         if(current_pair->exploration_started == 0)
+         if (!current_pair->exploration_started)
            mc_stats->visited_pairs++;
 
          /* Answer the request */
@@ -533,35 +453,35 @@ int LivenessChecker::main(void)
          mc_model_checker->wait_for_requests();
 
          current_pair->requests--;
-         current_pair->exploration_started = 1;
+         current_pair->exploration_started = true;
 
          /* Get values of atomic propositions (variables used in the property formula) */
-         prop_values = this->getPropositionValues();
+         std::vector<int> prop_values = this->getPropositionValues();
 
          /* Evaluate enabled/true transitions in automaton according to atomic propositions values and create new pairs */
          cursor = xbt_dynar_length(current_pair->automaton_state->out) - 1;
          while (cursor >= 0) {
            transition_succ = (xbt_automaton_transition_t)xbt_dynar_get_as(current_pair->automaton_state->out, cursor, xbt_automaton_transition_t);
-           res = MC_automaton_evaluate_label(transition_succ->label, prop_values.get());
+           res = MC_automaton_evaluate_label(transition_succ->label, prop_values);
            if (res == 1 || res == 2) { /* 1 = True transition (always enabled), 2 = enabled transition according to atomic prop values */
-              next_pair = new Pair();
-              next_pair->graph_state = MC_state_new();
+              Pair* next_pair = new Pair();
+              next_pair->graph_state = std::shared_ptr<simgrid::mc::State>(MC_state_new());
               next_pair->automaton_state = transition_succ->dst;
               next_pair->atomic_propositions = this->getPropositionValues();
               next_pair->depth = current_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))
-                  MC_state_interleave_process(next_pair->graph_state, &p.copy);
+                  MC_state_interleave_process(next_pair->graph_state.get(), &p.copy);
 
-              next_pair->requests = MC_state_interleave_size(next_pair->graph_state);
+              next_pair->requests = MC_state_interleave_size(next_pair->graph_state.get());
 
               /* FIXME : get search_cycle value for each acceptant state */
               if (next_pair->automaton_state->type == 1 || current_pair->search_cycle)
-                next_pair->search_cycle = 1;
+                next_pair->search_cycle = true;
 
               /* Add new pair to the exploration stack */
-              xbt_fifo_unshift(liveness_stack, next_pair);
+              livenessStack_.push_back(next_pair);
 
            }
            cursor--;
@@ -575,16 +495,16 @@ int LivenessChecker::main(void)
       if(visited_num == -1)
         XBT_DEBUG("No more request to execute. Looking for backtracking point.");
 
-      prop_values.reset();
-
       /* Traverse the stack backwards until a pair with a non empty interleave
          set is found, deleting all the pairs that have it empty in the way. */
-      while ((current_pair = (simgrid::mc::Pair*) xbt_fifo_shift(liveness_stack)) != nullptr) {
+      while (!livenessStack_.empty()) {
+        current_pair = livenessStack_.back();
+        livenessStack_.pop_back();
         if (current_pair->requests > 0) {
           /* We found a backtracking point */
           XBT_DEBUG("Backtracking to depth %d", current_pair->depth);
-          xbt_fifo_unshift(liveness_stack, current_pair);
-          this->replay(liveness_stack);
+          livenessStack_.push_back(current_pair);
+          this->replay();
           XBT_DEBUG("Backtracking done");
           break;
         }else{
@@ -598,7 +518,7 @@ int LivenessChecker::main(void)
 
     } /* End of if (current_pair->requests > 0) else ... */
 
-  } /* End of while(xbt_fifo_size(liveness_stack) > 0) */
+  }
 
   XBT_INFO("No property violation found.");
   MC_print_statistics(mc_stats);
@@ -612,10 +532,6 @@ int LivenessChecker::run()
   mc_model_checker->wait_for_requests();
 
   XBT_DEBUG("Starting the liveness algorithm");
-  _sg_mc_liveness = 1;
-
-  /* Create exploration stack */
-  liveness_stack = xbt_fifo_new();
 
   /* Create the initial state */
   simgrid::mc::initial_global_state = std::unique_ptr<s_mc_global_t>(new s_mc_global_t());
@@ -623,8 +539,14 @@ int LivenessChecker::run()
   this->prepare();
   int res = this->main();
   simgrid::mc::initial_global_state = nullptr;
+
   return res;
 }
 
+Checker* createLivenessChecker(Session& session)
+{
+  return new LivenessChecker(session);
+}
+
 }
 }