[mc] Add Factor some gorry code to State::getRecordElement()

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

diff --git a/src/mc/LivenessChecker.cpp b/src/mc/LivenessChecker.cpp
index 086d122..2837d43 100644 (file)
--- a/src/mc/LivenessChecker.cpp
+++ b/src/mc/LivenessChecker.cpp
@@ -138,7 +138,7 @@ std::shared_ptr<VisitedPair> LivenessChecker::insertAcceptancePair(simgrid::mc::
     if (dot_output != nullptr)
       fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n",
         initial_global_state->prev_pair, pair_test->num,
-        initial_global_state->prev_req);
+        initial_global_state->prev_req.c_str());
     return nullptr;
   }
 
@@ -211,12 +211,11 @@ void LivenessChecker::replay()
         req = &issuer->simcall;
 
         /* Debug information */
-        if (XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug)) {
-          char* req_str = simgrid::mc::request_to_string(req, value, simgrid::mc::RequestType::simix);
-          XBT_DEBUG("Replay (depth = %d) : %s (%p)", depth, req_str, state.get());
-          xbt_free(req_str);
-        }
-
+        XBT_DEBUG("Replay (depth = %d) : %s (%p)",
+          depth,
+          simgrid::mc::request_to_string(
+            req, value, simgrid::mc::RequestType::simix).c_str(),
+          state.get());
       }
 
       simgrid::mc::handle_simcall(req, value);
@@ -297,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;
 }
 
@@ -328,11 +320,9 @@ std::vector<std::string> LivenessChecker::getTextualTrace() // override
   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) {
-      char* req_str = simgrid::mc::request_to_string(req, value, simgrid::mc::RequestType::executed);
-      trace.push_back(std::string(req_str));
-      xbt_free(req_str);
-    }
+    if (req && req->call != SIMCALL_NONE)
+      trace.push_back(simgrid::mc::request_to_string(
+        req, value, simgrid::mc::RequestType::executed));
   }
   return trace;
 }
@@ -369,7 +359,9 @@ int LivenessChecker::main(void)
       && (visited_num = this->insertVisitedPair(
         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);
+        fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n",
+          initial_global_state->prev_pair, visited_num,
+          initial_global_state->prev_req.c_str());
         fflush(dot_output);
       }
       XBT_DEBUG("Pair already visited (equal to pair %d), exploration on the current path stopped.", visited_num);
@@ -383,8 +375,10 @@ int LivenessChecker::main(void)
 
     if (dot_output != nullptr) {
       if (initial_global_state->prev_pair != 0 && initial_global_state->prev_pair != current_pair->num) {
-        fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", initial_global_state->prev_pair, current_pair->num, initial_global_state->prev_req);
-        xbt_free(initial_global_state->prev_req);
+        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();
       }
       initial_global_state->prev_pair = current_pair->num;
       initial_global_state->prev_req = simgrid::mc::request_get_dot_output(req, value);
@@ -393,12 +387,9 @@ int LivenessChecker::main(void)
       fflush(dot_output);
     }
 
-    char* req_str = simgrid::mc::request_to_string(req, value, simgrid::mc::RequestType::simix);
-    XBT_DEBUG("Execute: %s", req_str);
-    xbt_free(req_str);
-
-    /* Set request as executed */
-    MC_state_set_executed_request(current_pair->graph_state.get(), req, value);
+    XBT_DEBUG("Execute: %s",
+      simgrid::mc::request_to_string(
+        req, value, simgrid::mc::RequestType::simix).c_str());
 
     /* Update mc_stats */
     mc_stats->executed_transitions++;
@@ -448,7 +439,7 @@ std::shared_ptr<Pair> LivenessChecker::newPair(Pair* current_pair, xbt_automaton
   /* 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.get(), &p.copy);
+      next_pair->graph_state->interleave(&p.copy);
   next_pair->requests = next_pair->graph_state->interleaveSize();
   /* FIXME : get search_cycle value for each acceptant state */
   if (next_pair->automaton_state->type == 1 ||