more info to the user.

[simgrid.git] / src / mc / checker / SafetyChecker.cpp

diff --git a/src/mc/checker/SafetyChecker.cpp b/src/mc/checker/SafetyChecker.cpp
index 088841a..d81492c 100644 (file)
--- a/src/mc/checker/SafetyChecker.cpp
+++ b/src/mc/checker/SafetyChecker.cpp
@@ -93,7 +93,7 @@ void SafetyChecker::run()
 {
   /* This function runs the DFS algorithm the state space.
    * We do so iteratively instead of recursively, dealing with the call stack manually.
-   * This allows to explore the call stack when we want to. */
+   * This allows to explore the call stack at wish. */
 
   while (!stack_.empty()) {
 
@@ -116,7 +116,7 @@ void SafetyChecker::run()
     // Backtrack if we are revisiting a state we saw previously
     if (visitedState_ != nullptr) {
       XBT_DEBUG("State already visited (equal to state %d), exploration stopped on this path.",
-                visitedState_->other_num == -1 ? visitedState_->num : visitedState_->other_num);
+                visitedState_->original_num == -1 ? visitedState_->num : visitedState_->original_num);
 
       visitedState_ = nullptr;
       this->backtrack();
@@ -124,7 +124,10 @@ void SafetyChecker::run()
     }
 
     // Search an enabled transition in the current state; backtrack if the interleave set is empty
+    // get_request also sets state.transition to be the one corresponding to the returned req
     smx_simcall_t req = MC_state_get_request(state);
+    // req is now the transition of the process that was selected to be executed
+
     if (req == nullptr) {
       XBT_DEBUG("There are no more processes to interleave. (depth %zi)", stack_.size() + 1);
 
@@ -144,10 +147,10 @@ void SafetyChecker::run()
 
     mc_model_checker->executed_transitions++;
 
-    /* Answer the request */
+    /* Actually answer the request: let execute the selected request (MCed does one step) */
     this->getSession().execute(state->transition);
 
-    /* Create the new expanded state */
+    /* Create the new expanded state (copy the state of MCed into our MCer data) */
     std::unique_ptr<simgrid::mc::State> next_state =
         std::unique_ptr<simgrid::mc::State>(new simgrid::mc::State(++expandedStatesCount_));
 
@@ -155,7 +158,7 @@ void SafetyChecker::run()
       this->checkNonTermination(next_state.get());
 
     /* Check whether we already explored next_state in the past (but only if interested in state-equality reduction) */
-    if (_sg_mc_visited == true)
+    if (_sg_mc_max_visited_states == true)
       visitedState_ = visitedStates_.addVisitedState(expandedStatesCount_, next_state.get(), true);
 
     /* If this is a new state (or if we don't care about state-equality reduction) */
@@ -174,9 +177,9 @@ void SafetyChecker::run()
           state->num, next_state->num, req_str.c_str());
 
     } else if (dot_output != nullptr)
-      std::fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n",
-        state->num,
-        visitedState_->other_num == -1 ? visitedState_->num : visitedState_->other_num, req_str.c_str());
+      std::fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num,
+                   visitedState_->original_num == -1 ? visitedState_->num : visitedState_->original_num,
+                   req_str.c_str());
 
     stack_.push_back(std::move(next_state));
   }
@@ -208,8 +211,8 @@ void SafetyChecker::backtrack()
     if (reductionMode_ == simgrid::mc::ReductionMode::dpor) {
       smx_simcall_t req = &state->internal_req;
       if (req->call == SIMCALL_MUTEX_LOCK || req->call == SIMCALL_MUTEX_TRYLOCK)
-        xbt_die("Mutex is currently not supported with DPOR, "
-          "use --cfg=model-check/reduction:none");
+        xbt_die("Mutex is currently not supported with DPOR,  use --cfg=model-check/reduction:none");
+
       const smx_actor_t issuer = MC_smx_simcall_get_issuer(req);
       for (auto i = stack_.rbegin(); i != stack_.rend(); ++i) {
         simgrid::mc::State* prev_state = i->get();
@@ -230,7 +233,7 @@ void SafetyChecker::backtrack()
               state->num);
           }
 
-          if (!prev_state->processStates[issuer->pid].isDone())
+          if (!prev_state->actorStates[issuer->pid].isDone())
             prev_state->interleave(issuer);
           else
             XBT_DEBUG("Process %p is in done set", req->issuer);
@@ -258,8 +261,7 @@ void SafetyChecker::backtrack()
     if (state->interleaveSize()
         && stack_.size() < (std::size_t) _sg_mc_max_depth) {
       /* We found a back-tracking point, let's loop */
-      XBT_DEBUG("Back-tracking to state %d at depth %zi",
-        state->num, stack_.size() + 1);
+      XBT_DEBUG("Back-tracking to state %d at depth %zi", state->num, stack_.size() + 1);
       stack_.push_back(std::move(state));
       this->restoreState();
       XBT_DEBUG("Back-tracking to state %d at depth %zi done",
@@ -306,7 +308,9 @@ SafetyChecker::SafetyChecker(Session& session) : Checker(session)
   if (_sg_mc_termination)
     XBT_INFO("Check non progressive cycles");
   else
-    XBT_INFO("Check a safety property");
+    XBT_INFO("Check a safety property. Reduction is: %s.",
+        (reductionMode_ == simgrid::mc::ReductionMode::none ? "none":
+            (reductionMode_ == simgrid::mc::ReductionMode::dpor ? "dpor": "unknown")));
   simgrid::mc::session->initialize();
 
   XBT_DEBUG("Starting the safety algorithm");