Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
CommunicationDeterminismChecker class doesn't use RemotePtr, it passes paramaters
[simgrid.git] / src / mc / checker / LivenessChecker.cpp
index e22741d..4d36052 100644 (file)
 #include "src/mc/mc_private.hpp"
 #include "src/mc/mc_request.hpp"
 #include "src/mc/mc_smx.hpp"
+#include "src/mc/mc_api.hpp"
 
 #include <boost/range/algorithm.hpp>
 #include <cstring>
 
 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_liveness, mc, "Logging specific to algorithms for liveness properties verification");
 
+using mcapi = simgrid::mc::mc_api;
+
 /********* Static functions *********/
 
 namespace simgrid {
@@ -82,9 +85,8 @@ std::shared_ptr<const std::vector<int>> LivenessChecker::get_proposition_values(
 
 std::shared_ptr<VisitedPair> LivenessChecker::insert_acceptance_pair(simgrid::mc::Pair* pair)
 {
-  std::shared_ptr<VisitedPair> new_pair = std::make_shared<VisitedPair>(
-    pair->num, pair->automaton_state, pair->atomic_propositions,
-    pair->graph_state);
+  auto new_pair =
+      std::make_shared<VisitedPair>(pair->num, pair->automaton_state, pair->atomic_propositions, pair->graph_state);
 
   auto res = boost::range::equal_range(acceptance_pairs_, new_pair.get(), DerefAndCompareByActorsCountAndUsedHeap());
 
@@ -145,16 +147,14 @@ void LivenessChecker::replay()
 
       smx_simcall_t req = nullptr;
 
-      if (saved_req != nullptr) {
-        /* because we got a copy of the executed request, we have to fetch the
-             real one, pointed by the request field of the issuer process */
-        const smx_actor_t issuer = MC_smx_simcall_get_issuer(saved_req);
-        req                      = &issuer->simcall_;
+      /* because we got a copy of the executed request, we have to fetch the
+         real one, pointed by the request field of the issuer process */
+      const smx_actor_t issuer = MC_smx_simcall_get_issuer(saved_req);
+      req                      = &issuer->simcall_;
 
-        /* Debug information */
-        XBT_DEBUG("Replay (depth = %d) : %s (%p)", depth,
-                  request_to_string(req, req_num, simgrid::mc::RequestType::simix).c_str(), state.get());
-      }
+      /* Debug information */
+      XBT_DEBUG("Replay (depth = %d) : %s (%p)", depth,
+                request_to_string(req, req_num, simgrid::mc::RequestType::simix).c_str(), state.get());
 
       this->get_session().execute(state->transition_);
     }
@@ -254,7 +254,7 @@ std::vector<std::string> LivenessChecker::get_textual_trace() // override
   for (std::shared_ptr<Pair> const& pair : exploration_stack_) {
     int req_num       = pair->graph_state->transition_.argument_;
     smx_simcall_t req = &pair->graph_state->executed_req_;
-    if (req && req->call_ != SIMCALL_NONE)
+    if (req->call_ != simix::Simcall::NONE)
       trace.push_back(request_to_string(req, req_num, RequestType::executed));
   }
   return trace;
@@ -263,10 +263,11 @@ std::vector<std::string> LivenessChecker::get_textual_trace() // override
 std::shared_ptr<Pair> LivenessChecker::create_pair(const Pair* current_pair, xbt_automaton_state_t state,
                                                    std::shared_ptr<const std::vector<int>> propositions)
 {
-  expanded_pairs_count_++;
-  std::shared_ptr<Pair> next_pair = std::make_shared<Pair>(expanded_pairs_count_);
+  ++expanded_pairs_count_;
+  ++expanded_states_count_;
+  auto next_pair                  = std::make_shared<Pair>(expanded_pairs_count_);
   next_pair->automaton_state      = state;
-  next_pair->graph_state          = std::shared_ptr<State>(new State(++expanded_states_count_));
+  next_pair->graph_state          = std::make_shared<State>(expanded_states_count_);
   next_pair->atomic_propositions  = std::move(propositions);
   if (current_pair)
     next_pair->depth = current_pair->depth + 1;
@@ -370,7 +371,7 @@ void LivenessChecker::run()
       }
     }
 
-    smx_simcall_t req = MC_state_choose_request(current_pair->graph_state.get());
+    smx_simcall_t req = mcapi::get().mc_state_choose_request(current_pair->graph_state.get());
     int req_num       = current_pair->graph_state->transition_.argument_;
 
     if (dot_output != nullptr) {