X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/ab92608267358b56adf7a803480fa2ad9608ed1b..a3445662ab8382ff70d83585c98c0041735f4a5d:/src/mc/checker/LivenessChecker.cpp?ds=sidebyside

diff --git a/src/mc/checker/LivenessChecker.cpp b/src/mc/checker/LivenessChecker.cpp
index 3a24b367e5..42ce4dc61e 100644
--- a/src/mc/checker/LivenessChecker.cpp
+++ b/src/mc/checker/LivenessChecker.cpp
@@ -1,4 +1,4 @@
-/* Copyright (c) 2011-2015. The SimGrid Team.
+/* Copyright (c) 2011-2017. The SimGrid Team.
  * All rights reserved.                                                     */
 
 /* This program is free software; you can redistribute it and/or modify it
@@ -29,7 +29,6 @@
 #include "src/mc/mc_record.h"
 #include "src/mc/mc_replay.h"
 #include "src/mc/mc_request.h"
-#include "src/mc/mc_safety.h"
 #include "src/mc/mc_smx.h"
 #include "src/mc/remote/Client.hpp"
 
@@ -40,24 +39,20 @@ XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_liveness, mc, "Logging specific to algorithms
 namespace simgrid {
 namespace mc {
 
-VisitedPair::VisitedPair(
-  int pair_num, xbt_automaton_state_t automaton_state,
-  std::shared_ptr<const std::vector<int>> atomic_propositions,
-  std::shared_ptr<simgrid::mc::State> graph_state)
+VisitedPair::VisitedPair(int pair_num, xbt_automaton_state_t automaton_state,
+                         std::shared_ptr<const std::vector<int>> atomic_propositions,
+                         std::shared_ptr<simgrid::mc::State> graph_state)
+    : num(pair_num), automaton_state(automaton_state)
 {
-  simgrid::mc::Process* process = &(mc_model_checker->process());
+  simgrid::mc::RemoteClient* process = &(mc_model_checker->process());
 
   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(
-    process->get_heap()->heaplimit,
-    process->get_malloc_info());
+  this->heap_bytes_used = mmalloc_get_bytes_used_remote(process->get_heap()->heaplimit, process->get_malloc_info());
 
   this->actors_count = mc_model_checker->process().actors().size();
 
-  this->automaton_state = automaton_state;
-  this->num = pair_num;
   this->other_num = -1;
   this->atomic_propositions = std::move(atomic_propositions);
 }
@@ -72,7 +67,7 @@ static bool evaluate_label(xbt_automaton_exp_label_t l, std::vector<int> const&
     return evaluate_label(l->u.or_and.left_exp, values)
       && evaluate_label(l->u.or_and.right_exp, values);
   case xbt_automaton_exp_label::AUT_NOT:
-    return !evaluate_label(l->u.exp_not, values);
+    return not evaluate_label(l->u.exp_not, values);
   case xbt_automaton_exp_label::AUT_PREDICAT:{
       unsigned int cursor = 0;
       xbt_automaton_propositional_symbol_t p = nullptr;
@@ -284,10 +279,10 @@ void LivenessChecker::showAcceptanceCycle(std::size_t depth)
   XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
   XBT_INFO("Counter-example that violates formula :");
   simgrid::mc::dumpRecordPath();
-  for (auto& s : this->getTextualTrace())
+  for (auto const& s : this->getTextualTrace())
     XBT_INFO("%s", s.c_str());
   simgrid::mc::session->logState();
-  XBT_INFO("Counter-example depth : %zd", depth);
+  XBT_INFO("Counter-example depth : %zu", depth);
 }
 
 std::vector<std::string> LivenessChecker::getTextualTrace() // override
@@ -317,7 +312,7 @@ std::shared_ptr<Pair> LivenessChecker::newPair(Pair* current_pair, xbt_automaton
   /* Get enabled actors and insert them in the interleave set of the next graph_state */
   for (auto& actor : mc_model_checker->process().actors())
     if (simgrid::mc::actor_is_enabled(actor.copy.getBuffer()))
-      next_pair->graph_state->interleave(actor.copy.getBuffer());
+      next_pair->graph_state->addInterleavingSet(actor.copy.getBuffer());
   next_pair->requests = next_pair->graph_state->interleaveSize();
   /* FIXME : get search_cycle value for each accepting state */
   if (next_pair->automaton_state->type == 1 || (current_pair && current_pair->search_cycle))
@@ -331,7 +326,7 @@ void LivenessChecker::backtrack()
 {
   /* 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 (!explorationStack_.empty()) {
+  while (not explorationStack_.empty()) {
     std::shared_ptr<simgrid::mc::Pair> current_pair = explorationStack_.back();
     explorationStack_.pop_back();
     if (current_pair->requests > 0) {
@@ -371,17 +366,16 @@ void LivenessChecker::run()
       explorationStack_.push_back(this->newPair(nullptr, automaton_state, propos));
 
   /* Actually run the double DFS search for counter-examples */
-  while (!explorationStack_.empty()){
+  while (not explorationStack_.empty()) {
     std::shared_ptr<Pair> current_pair = explorationStack_.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 = %zd, pair_num = %d, requests = %d)",
-       current_pair->depth, current_pair->search_cycle,
-       current_pair->graph_state->interleaveSize(),
-       current_pair->num,
-       current_pair->requests);
+    XBT_DEBUG(
+        "********************* ( Depth = %d, search_cycle = %d, interleave size = %zu, pair_num = %d, requests = %d)",
+        current_pair->depth, current_pair->search_cycle, current_pair->graph_state->interleaveSize(), current_pair->num,
+        current_pair->requests);
 
     if (current_pair->requests == 0) {
       this->backtrack();
@@ -389,27 +383,28 @@ void LivenessChecker::run()
     }
 
     std::shared_ptr<VisitedPair> reached_pair;
-    if (current_pair->automaton_state->type == 1 && !current_pair->exploration_started
-        && (reached_pair = this->insertAcceptancePair(current_pair.get())) == nullptr) {
-      this->showAcceptanceCycle(current_pair->depth);
-      throw simgrid::mc::LivenessError();
+    if (current_pair->automaton_state->type == 1 && not current_pair->exploration_started) {
+      reached_pair = this->insertAcceptancePair(current_pair.get());
+      if (reached_pair == nullptr) {
+        this->showAcceptanceCycle(current_pair->depth);
+        throw simgrid::mc::LivenessError();
+      }
     }
 
     /* Pair already visited ? stop the exploration on the current path */
-    int visited_num = -1;
-    if ((!current_pair->exploration_started)
-      && (visited_num = this->insertVisitedPair(
-        reached_pair, current_pair.get())) != -1) {
-      if (dot_output != nullptr){
-        fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n",
-          this->previousPair_, visited_num,
-          this->previousRequest_.c_str());
-        fflush(dot_output);
+    if (not current_pair->exploration_started) {
+      int visited_num = this->insertVisitedPair(reached_pair, current_pair.get());
+      if (visited_num != -1) {
+        if (dot_output != nullptr) {
+          fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", 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);
+        current_pair->requests = 0;
+        this->backtrack();
+        continue;
       }
-      XBT_DEBUG("Pair already visited (equal to pair %d), exploration on the current path stopped.", visited_num);
-      current_pair->requests = 0;
-      this->backtrack();
-      continue;
     }
 
     smx_simcall_t req = MC_state_get_request(current_pair->graph_state.get());
@@ -435,7 +430,7 @@ void LivenessChecker::run()
 
     /* Update stats */
     mc_model_checker->executed_transitions++;
-    if (!current_pair->exploration_started)
+    if (not current_pair->exploration_started)
       visitedPairsCount_++;
 
     /* Answer the request */