[mc] s/value/req_num/ because 'value' does not convey any meaning

[simgrid.git] / src / mc / LivenessChecker.cpp

diff --git a/src/mc/LivenessChecker.cpp b/src/mc/LivenessChecker.cpp
index 8dcb3b9..f84e892 100644 (file)
--- a/src/mc/LivenessChecker.cpp
+++ b/src/mc/LivenessChecker.cpp
@@ -199,8 +199,8 @@ void LivenessChecker::replay()
 
     if (pair->exploration_started) {
 
-      int value;
-      smx_simcall_t saved_req = MC_state_get_executed_request(state.get(), &value);
+      int req_num = state->req_num;
+      smx_simcall_t saved_req = &state->executed_req;
 
       smx_simcall_t req = nullptr;
 
@@ -214,11 +214,11 @@ void LivenessChecker::replay()
         XBT_DEBUG("Replay (depth = %d) : %s (%p)",
           depth,
           simgrid::mc::request_to_string(
-            req, value, simgrid::mc::RequestType::simix).c_str(),
+            req, req_num, simgrid::mc::RequestType::simix).c_str(),
           state.get());
       }
 
-      simgrid::mc::handle_simcall(req, value);
+      simgrid::mc::handle_simcall(req, req_num);
       mc_model_checker->wait_for_requests();
     }
 
@@ -296,15 +296,8 @@ LivenessChecker::~LivenessChecker()
 RecordTrace LivenessChecker::getRecordTrace() // override
 {
   RecordTrace res;
-  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) {
-      smx_process_t issuer = MC_smx_simcall_get_issuer(req);
-      const int pid = issuer->pid;
-      res.push_back(RecordTraceElement(pid, value));
-    }
-  }
+  for (std::shared_ptr<Pair> const& pair : explorationStack_)
+    res.push_back(pair->graph_state->getRecordElement());
   return res;
 }
 
@@ -325,11 +318,11 @@ std::vector<std::string> LivenessChecker::getTextualTrace() // override
 {
   std::vector<std::string> trace;
   for (std::shared_ptr<Pair> const& pair : explorationStack_) {
-    int value;
-    smx_simcall_t req = MC_state_get_executed_request(pair->graph_state.get(), &value);
+    int req_num = pair->graph_state->req_num;
+    smx_simcall_t req = &pair->graph_state->executed_req;
     if (req && req->call != SIMCALL_NONE)
       trace.push_back(simgrid::mc::request_to_string(
-        req, value, simgrid::mc::RequestType::executed));
+        req, req_num, simgrid::mc::RequestType::executed));
   }
   return trace;
 }
@@ -377,8 +370,8 @@ int LivenessChecker::main(void)
       continue;
     }
 
-    int value;
-    smx_simcall_t req = MC_state_get_request(current_pair->graph_state.get(), &value);
+    smx_simcall_t req = MC_state_get_request(current_pair->graph_state.get());
+    int req_num = current_pair->graph_state->req_num;
 
     if (dot_output != nullptr) {
       if (initial_global_state->prev_pair != 0 && initial_global_state->prev_pair != current_pair->num) {
@@ -388,7 +381,7 @@ int LivenessChecker::main(void)
         initial_global_state->prev_req.clear();
       }
       initial_global_state->prev_pair = current_pair->num;
-      initial_global_state->prev_req = simgrid::mc::request_get_dot_output(req, value);
+      initial_global_state->prev_req = 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);
@@ -396,7 +389,7 @@ int LivenessChecker::main(void)
 
     XBT_DEBUG("Execute: %s",
       simgrid::mc::request_to_string(
-        req, value, simgrid::mc::RequestType::simix).c_str());
+        req, req_num, simgrid::mc::RequestType::simix).c_str());
 
     /* Update mc_stats */
     mc_stats->executed_transitions++;
@@ -404,7 +397,7 @@ int LivenessChecker::main(void)
       mc_stats->visited_pairs++;
 
     /* Answer the request */
-    simgrid::mc::handle_simcall(req, value);
+    simgrid::mc::handle_simcall(req, req_num);
 
     /* Wait for requests (schedules processes) */
     mc_model_checker->wait_for_requests();