[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 5ded308..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;
   }
 
@@ -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;
 }
 
@@ -366,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);
@@ -380,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);
@@ -394,9 +391,6 @@ int LivenessChecker::main(void)
       simgrid::mc::request_to_string(
         req, value, simgrid::mc::RequestType::simix).c_str());
 
-    /* Set request as executed */
-    MC_state_set_executed_request(current_pair->graph_state.get(), req, value);
-
     /* Update mc_stats */
     mc_stats->executed_transitions++;
     if (!current_pair->exploration_started)
@@ -445,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 ||