From: Gabriel Corona <gabriel.corona@loria.fr>
Date: Fri, 1 Apr 2016 10:01:32 +0000 (+0200)
Subject: [mc] Rename livenessStack to explorationStack
X-Git-Tag: v3_13~180^2~12^2^2
X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/commitdiff_plain/947e36b8b2d9cd9dbdd44170d4cc4b034f4f7a99

[mc] Rename livenessStack to explorationStack
---

diff --git a/src/mc/LivenessChecker.cpp b/src/mc/LivenessChecker.cpp
index c1ceaabb8c..abf36efed1 100644
--- a/src/mc/LivenessChecker.cpp
+++ b/src/mc/LivenessChecker.cpp
@@ -133,7 +133,7 @@ std::shared_ptr<VisitedPair> LivenessChecker::insertAcceptancePair(simgrid::mc::
       continue;
     XBT_INFO("Pair %d already reached (equal to pair %d) !",
       new_pair->num, pair_test->num);
-    livenessStack_.pop_back();
+    explorationStack_.pop_back();
     if (dot_output != nullptr)
       fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n",
         initial_global_state->prev_pair, pair_test->num,
@@ -166,7 +166,7 @@ void LivenessChecker::prepare(void)
   xbt_automaton_state_t automaton_state;
   xbt_dynar_foreach(simgrid::mc::property_automaton->states, cursor, automaton_state)
     if (automaton_state->type == -1)
-      livenessStack_.push_back(this->newPair(nullptr, automaton_state));
+      explorationStack_.push_back(this->newPair(nullptr, automaton_state));
 }
 
 
@@ -176,7 +176,7 @@ void LivenessChecker::replay()
 
   /* Intermediate backtracking */
   if(_sg_mc_checkpoint > 0) {
-    simgrid::mc::Pair* pair = livenessStack_.back().get();
+    simgrid::mc::Pair* pair = explorationStack_.back().get();
     if(pair->graph_state->system_state){
       simgrid::mc::restore_snapshot(pair->graph_state->system_state);
       return;
@@ -188,8 +188,8 @@ void LivenessChecker::replay()
 
   /* Traverse the stack from the initial state and re-execute the transitions */
   int depth = 1;
-  for (std::shared_ptr<Pair> const& pair : livenessStack_) {
-    if (pair == livenessStack_.back())
+  for (std::shared_ptr<Pair> const& pair : explorationStack_) {
+    if (pair == explorationStack_.back())
       break;
 
     std::shared_ptr<State> state = pair->graph_state;
@@ -294,7 +294,7 @@ LivenessChecker::~LivenessChecker()
 RecordTrace LivenessChecker::getRecordTrace() // override
 {
   RecordTrace res;
-  for (std::shared_ptr<Pair> const& pair : livenessStack_) {
+  for (std::shared_ptr<Pair> const& pair : explorationStack_) {
     int value;
     smx_simcall_t req = MC_state_get_executed_request(pair->graph_state.get(), &value);
     if (req && req->call != SIMCALL_NONE) {
@@ -322,7 +322,7 @@ void LivenessChecker::showAcceptanceCycle(std::size_t depth)
 std::vector<std::string> LivenessChecker::getTextualTrace() // override
 {
   std::vector<std::string> trace;
-  for (std::shared_ptr<Pair> const& pair : livenessStack_) {
+  for (std::shared_ptr<Pair> const& pair : explorationStack_) {
     int value;
     smx_simcall_t req = MC_state_get_executed_request(pair->graph_state.get(), &value);
     if (req && req->call != SIMCALL_NONE) {
@@ -336,8 +336,8 @@ std::vector<std::string> LivenessChecker::getTextualTrace() // override
 
 int LivenessChecker::main(void)
 {
-  while (!livenessStack_.empty()){
-    std::shared_ptr<Pair> current_pair = livenessStack_.back();
+  while (!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;
@@ -419,7 +419,7 @@ int LivenessChecker::main(void)
     while (cursor >= 0) {
       xbt_automaton_transition_t transition_succ = (xbt_automaton_transition_t)xbt_dynar_get_as(current_pair->automaton_state->out, cursor, xbt_automaton_transition_t);
       if (evaluate_label(transition_succ->label, prop_values))
-          livenessStack_.push_back(this->newPair(
+          explorationStack_.push_back(this->newPair(
             current_pair.get(), transition_succ->dst));
        cursor--;
      }
@@ -459,13 +459,13 @@ 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 (!livenessStack_.empty()) {
-    std::shared_ptr<simgrid::mc::Pair> current_pair = livenessStack_.back();
-    livenessStack_.pop_back();
+  while (!explorationStack_.empty()) {
+    std::shared_ptr<simgrid::mc::Pair> current_pair = explorationStack_.back();
+    explorationStack_.pop_back();
     if (current_pair->requests > 0) {
       /* We found a backtracking point */
       XBT_DEBUG("Backtracking to depth %d", current_pair->depth);
-      livenessStack_.push_back(std::move(current_pair));
+      explorationStack_.push_back(std::move(current_pair));
       this->replay();
       XBT_DEBUG("Backtracking done");
       break;
diff --git a/src/mc/LivenessChecker.hpp b/src/mc/LivenessChecker.hpp
index b595fc71fc..f12c0b3be1 100644
--- a/src/mc/LivenessChecker.hpp
+++ b/src/mc/LivenessChecker.hpp
@@ -83,8 +83,9 @@ private:
   void backtrack();
   std::shared_ptr<Pair> newPair(Pair* pair, xbt_automaton_state_t state);
 public:
+  // A stack of (application_state, automaton_state) pairs for DFS exploration:
+  std::list<std::shared_ptr<Pair>> explorationStack_;
   std::list<std::shared_ptr<VisitedPair>> acceptancePairs_;
-  std::list<std::shared_ptr<Pair>> livenessStack_;
   std::list<std::shared_ptr<VisitedPair>> visitedPairs_;
 };