[mc] Remove useless model-checker/model-checked round trip

diff --git a/src/mc/Client.cpp b/src/mc/Client.cpp
index 9fc8688..c05696f 100644 (file)
--- a/src/mc/Client.cpp
+++ b/src/mc/Client.cpp
@@ -156,10 +156,10 @@ void Client::handleMessages()
 void Client::mainLoop(void)
 {
   while (1) {
+    simgrid::mc::wait_for_requests();
     if (channel_.send(MC_MESSAGE_WAITING))
       xbt_die("Could not send WAITING mesage to model-checker");
     this->handleMessages();
-    simgrid::mc::wait_for_requests();
   }
 }
 

diff --git a/src/mc/CommunicationDeterminismChecker.cpp b/src/mc/CommunicationDeterminismChecker.cpp
index 2c09269..2b20a33 100644 (file)
--- a/src/mc/CommunicationDeterminismChecker.cpp
+++ b/src/mc/CommunicationDeterminismChecker.cpp
@@ -351,9 +351,6 @@ void CommunicationDeterminismChecker::prepare()
 
   XBT_DEBUG("********* Start communication determinism verification *********");
 
-  /* 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))

diff --git a/src/mc/LivenessChecker.cpp b/src/mc/LivenessChecker.cpp
index 2ea5b22..e33db3a 100644 (file)
--- a/src/mc/LivenessChecker.cpp
+++ b/src/mc/LivenessChecker.cpp
@@ -158,7 +158,6 @@ void LivenessChecker::removeAcceptancePair(int pair_num)
 
 void LivenessChecker::prepare(void)
 {
-  mc_model_checker->wait_for_requests();
   initial_global_state->snapshot = simgrid::mc::take_snapshot(0);
   initial_global_state->prev_pair = 0;
 

diff --git a/src/mc/SafetyChecker.cpp b/src/mc/SafetyChecker.cpp
index 698b546..d565169 100644 (file)
--- a/src/mc/SafetyChecker.cpp
+++ b/src/mc/SafetyChecker.cpp
@@ -295,9 +295,6 @@ void SafetyChecker::init()
   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)) {