[mc] Move the MCer wait_for_requests logic outside of MC_wait_for_requests

diff --git a/src/mc/ModelChecker.hpp b/src/mc/ModelChecker.hpp
index eaed239..ee1a955 100644 (file)
--- a/src/mc/ModelChecker.hpp
+++ b/src/mc/ModelChecker.hpp
@@ -68,6 +68,10 @@ public:
   bool handle_events();
   void wait_client(simgrid::mc::Process& process);
   void simcall_handle(simgrid::mc::Process& process, unsigned long pid, int value);
+  void wait_for_requests()
+  {
+    mc_model_checker->wait_client(mc_model_checker->process());
+  }
 private:
   void setup_ignore();
   bool handle_message(char* buffer, ssize_t size);

diff --git a/src/mc/mc_base.cpp b/src/mc/mc_base.cpp
index 01f56bf..5a7f2f8 100644 (file)
--- a/src/mc/mc_base.cpp
+++ b/src/mc/mc_base.cpp
@@ -40,12 +40,7 @@ int MC_random(int min, int max)
 
 void MC_wait_for_requests(void)
 {
-#ifdef HAVE_MC
-  if (mc_mode == MC_MODE_SERVER) {
-    mc_model_checker->wait_client(mc_model_checker->process());
-    return;
-  }
-#endif
+  assert(mc_mode != MC_MODE_SERVER);
 
   smx_process_t process;
   smx_simcall_t req;

diff --git a/src/mc/mc_comm_determinism.cpp b/src/mc/mc_comm_determinism.cpp
index 41f27e6..019e609 100644 (file)
--- a/src/mc/mc_comm_determinism.cpp
+++ b/src/mc/mc_comm_determinism.cpp
@@ -323,7 +323,7 @@ static void MC_pre_modelcheck_comm_determinism(void)
   XBT_DEBUG("********* Start communication determinism verification *********");
 
   /* Wait for requests (schedules processes) */
-  MC_wait_for_requests();
+  mc_model_checker->wait_for_requests();
 
   /* Get an enabled process and insert it in the interleave set of the initial state */
   MC_EACH_SIMIX_PROCESS(process,
@@ -388,7 +388,7 @@ static int MC_modelcheck_comm_determinism_main(void)
         MC_handle_comm_pattern(call, req, value, NULL, 0);
 
       /* Wait for requests (schedules processes) */
-      MC_wait_for_requests();
+      mc_model_checker->wait_for_requests();
 
       /* Create the new expanded state */
       next_state = MC_state_new();
@@ -470,7 +470,7 @@ int MC_modelcheck_comm_determinism(void)
 {
   XBT_INFO("Check communication determinism");
   mc_reduce_kind = e_mc_reduce_none;
-  MC_wait_for_requests();
+  mc_model_checker->wait_for_requests();
 
   if (mc_mode == MC_MODE_CLIENT) {
     // This will move somehwere else:

diff --git a/src/mc/mc_global.cpp b/src/mc/mc_global.cpp
index 0806e53..62bb75d 100644 (file)
--- a/src/mc/mc_global.cpp
+++ b/src/mc/mc_global.cpp
@@ -263,7 +263,7 @@ void MC_replay(xbt_fifo_t stack)
       if (_sg_mc_comms_determinism || _sg_mc_send_determinism)
         MC_handle_comm_pattern(call, req, value, NULL, 1);
 
-      MC_wait_for_requests();
+      mc_model_checker->wait_for_requests();
 
       count++;
     }
@@ -330,7 +330,7 @@ void MC_replay_liveness(xbt_fifo_t stack)
         }
 
         MC_simcall_handle(req, value);
-        MC_wait_for_requests();
+        mc_model_checker->wait_for_requests();
       }
 
       /* Update statistics */

diff --git a/src/mc/mc_liveness.cpp b/src/mc/mc_liveness.cpp
index 9db185c..7eef307 100644 (file)
--- a/src/mc/mc_liveness.cpp
+++ b/src/mc/mc_liveness.cpp
@@ -174,7 +174,7 @@ static void MC_pre_modelcheck_liveness(void)
   mc_pair_t initial_pair = NULL;
   smx_process_t process;
 
-  MC_wait_for_requests();
+  mc_model_checker->wait_for_requests();
 
   acceptance_pairs = xbt_dynar_new(sizeof(mc_visited_pair_t), NULL);
   if(_sg_mc_visited > 0)
@@ -298,7 +298,7 @@ static int MC_modelcheck_liveness_main(void)
          MC_simcall_handle(req, value);
          
          /* Wait for requests (schedules processes) */
-         MC_wait_for_requests();
+         mc_model_checker->wait_for_requests();
 
          current_pair->requests--;
          current_pair->exploration_started = 1;
@@ -381,7 +381,7 @@ int MC_modelcheck_liveness(void)
     mc_reduce_kind = e_mc_reduce_none;
   XBT_INFO("Check the liveness property %s", _sg_mc_property_file);
   MC_automaton_load(_sg_mc_property_file);
-  MC_wait_for_requests();
+  mc_model_checker->wait_for_requests();
 
   XBT_DEBUG("Starting the liveness algorithm");
   _sg_mc_liveness = 1;

diff --git a/src/mc/mc_safety.cpp b/src/mc/mc_safety.cpp
index b00c31e..89c7076 100644 (file)
--- a/src/mc/mc_safety.cpp
+++ b/src/mc/mc_safety.cpp
@@ -54,7 +54,7 @@ static void MC_pre_modelcheck_safety()
   XBT_DEBUG("Initial state");
 
   /* Wait for requests (schedules processes) */
-  MC_wait_for_requests();
+  mc_model_checker->wait_for_requests();
 
   /* Get an enabled process and insert it in the interleave set of the initial state */
   smx_process_t process;
@@ -119,7 +119,7 @@ int MC_modelcheck_safety(void)
 
       /* Answer the request */
       MC_simcall_handle(req, value);
-      MC_wait_for_requests();
+      mc_model_checker->wait_for_requests();
 
       /* Create the new expanded state */
       next_state = MC_state_new();
@@ -273,7 +273,7 @@ static void MC_modelcheck_safety_init(void)
     XBT_INFO("Check non progressive cycles");
   else
     XBT_INFO("Check a safety property");
-  MC_wait_for_requests();
+  mc_model_checker->wait_for_requests();
 
   XBT_DEBUG("Starting the safety algorithm");