[mc] Move initial state into Session

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

diff --git a/src/mc/SafetyChecker.cpp b/src/mc/SafetyChecker.cpp
index 664379d..4064b6a 100644 (file)
--- a/src/mc/SafetyChecker.cpp
+++ b/src/mc/SafetyChecker.cpp
@@ -25,6 +25,8 @@
 #include "src/mc/Checker.hpp"
 #include "src/mc/SafetyChecker.hpp"
 #include "src/mc/VisitedState.hpp"
+#include "src/mc/Transition.hpp"
+#include "src/mc/Session.hpp"
 
 #include "src/xbt/mmalloc/mmprivate.h"
 
@@ -41,7 +43,7 @@ static void MC_show_non_termination(void)
   XBT_INFO("Counter-example execution trace:");
   for (auto& s : mc_model_checker->getChecker()->getTextualTrace())
     XBT_INFO("%s", s.c_str());
-  MC_print_statistics(mc_stats);
+  simgrid::mc::session->logState();
 }
 
 static int snapshot_compare(simgrid::mc::State* state1, simgrid::mc::State* state2)
@@ -68,7 +70,7 @@ RecordTrace SafetyChecker::getRecordTrace() // override
 {
   RecordTrace res;
   for (auto const& state : stack_)
-    res.push_back(state->getRecordElement());
+    res.push_back(state->getTransition());
   return res;
 }
 
@@ -76,7 +78,7 @@ std::vector<std::string> SafetyChecker::getTextualTrace() // override
 {
   std::vector<std::string> trace;
   for (auto const& state : stack_) {
-    int value = state->req_num;
+    int value = state->transition.argument;
     smx_simcall_t req = &state->executed_req;
     if (req)
       trace.push_back(simgrid::mc::request_to_string(
@@ -85,12 +87,18 @@ std::vector<std::string> SafetyChecker::getTextualTrace() // override
   return trace;
 }
 
+void SafetyChecker::logState() // override
+{
+  Checker::logState();
+  XBT_INFO("Expanded states = %lu", expandedStatesCount_);
+  XBT_INFO("Visited states = %lu", mc_model_checker->visited_states);
+  XBT_INFO("Executed transitions = %lu", mc_model_checker->executed_transitions);
+}
+
 int SafetyChecker::run()
 {
   this->init();
 
-  int value;
-
   while (!stack_.empty()) {
 
     /* Get current state */
@@ -102,13 +110,13 @@ int SafetyChecker::run()
       stack_.size(), state, state->num,
       state->interleaveSize());
 
-    mc_stats->visited_states++;
+    mc_model_checker->visited_states++;
 
     // The interleave set is empty or the maximum depth is reached,
     // let's back-track.
     smx_simcall_t req = nullptr;
     if (stack_.size() > (std::size_t) _sg_mc_max_depth
-        || (req = MC_state_get_request(state, &value)) == nullptr
+        || (req = MC_state_get_request(state)) == nullptr
         || visitedState_ != nullptr) {
       int res = this->backtrack();
       if (res)
@@ -121,24 +129,20 @@ int SafetyChecker::run()
     // reached then perform one step of the exploration algorithm.
     XBT_DEBUG("Execute: %s",
       simgrid::mc::request_to_string(
-        req, value, simgrid::mc::RequestType::simix).c_str());
+        req, state->transition.argument, simgrid::mc::RequestType::simix).c_str());
 
     std::string req_str;
     if (dot_output != nullptr)
-      req_str = simgrid::mc::request_get_dot_output(req, value);
+      req_str = simgrid::mc::request_get_dot_output(req, state->transition.argument);
 
-    mc_stats->executed_transitions++;
-
-    // TODO, bundle both operations in a single message
-    //   MC_execute_transition(req, value)
+    mc_model_checker->executed_transitions++;
 
     /* Answer the request */
-    simgrid::mc::handle_simcall(req, value);
-    mc_model_checker->wait_for_requests();
+    this->getSession().execute(state->transition);
 
     /* Create the new expanded state */
     std::unique_ptr<simgrid::mc::State> next_state =
-      std::unique_ptr<simgrid::mc::State>(MC_state_new());
+      std::unique_ptr<simgrid::mc::State>(MC_state_new(++expandedStatesCount_));
 
     if (_sg_mc_termination && this->checkNonTermination(next_state.get())) {
         MC_show_non_termination();
@@ -146,7 +150,7 @@ int SafetyChecker::run()
     }
 
     if (_sg_mc_visited == 0
-        || (visitedState_ = visitedStates_.addVisitedState(next_state.get(), true)) == nullptr) {
+        || (visitedState_ = visitedStates_.addVisitedState(expandedStatesCount_, next_state.get(), true)) == nullptr) {
 
       /* Get an enabled process and insert it in the interleave set of the next state */
       for (auto& p : mc_model_checker->process().simix_processes())
@@ -169,8 +173,7 @@ int SafetyChecker::run()
   }
 
   XBT_INFO("No property violation found.");
-  MC_print_statistics(mc_stats);
-  initial_global_state = nullptr;
+  simgrid::mc::session->logState();
   return SIMGRID_MC_EXIT_SUCCESS;
 }
 
@@ -220,13 +223,13 @@ int SafetyChecker::backtrack()
             && simgrid::mc::request_depend(req, &prev_state->internal_req)) {
           if (XBT_LOG_ISENABLED(mc_safety, xbt_log_priority_debug)) {
             XBT_DEBUG("Dependent Transitions:");
-            int value = prev_state->req_num;
+            int value = prev_state->transition.argument;
             smx_simcall_t prev_req = &prev_state->executed_req;
             XBT_DEBUG("%s (state=%d)",
               simgrid::mc::request_to_string(
                 prev_req, value, simgrid::mc::RequestType::internal).c_str(),
               prev_state->num);
-            value = state->req_num;
+            value = state->transition.argument;
             prev_req = &state->executed_req;
             XBT_DEBUG("%s (state=%d)",
               simgrid::mc::request_to_string(
@@ -289,19 +292,16 @@ void SafetyChecker::init()
     XBT_INFO("Check non progressive cycles");
   else
     XBT_INFO("Check a safety property");
-  mc_model_checker->wait_for_requests();
+  simgrid::mc::session->initialize();
 
   XBT_DEBUG("Starting the safety algorithm");
 
   std::unique_ptr<simgrid::mc::State> initial_state =
-    std::unique_ptr<simgrid::mc::State>(MC_state_new());
+    std::unique_ptr<simgrid::mc::State>(MC_state_new(++expandedStatesCount_));
 
   XBT_DEBUG("**************************************************");
   XBT_DEBUG("Initial state");
 
-  /* Wait for requests (schedules processes) */
-  mc_model_checker->wait_for_requests();
-
   /* Get an enabled process and insert it in the interleave set of the initial state */
   for (auto& p : mc_model_checker->process().simix_processes())
     if (simgrid::mc::process_is_enabled(&p.copy)) {
@@ -311,10 +311,6 @@ void SafetyChecker::init()
     }
 
   stack_.push_back(std::move(initial_state));
-
-  /* Save the initial state */
-  initial_global_state = std::unique_ptr<s_mc_global_t>(new s_mc_global_t());
-  initial_global_state->snapshot = simgrid::mc::take_snapshot(0);
 }
 
 SafetyChecker::SafetyChecker(Session& session) : Checker(session)