X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/878c6247eb42cc7435bb39dd1f41e35b1b845c72..4a6b0a991a67e6f2f67c03fed43529e078da7115:/src/mc/mc_safety.cpp

diff --git a/src/mc/mc_safety.cpp b/src/mc/mc_safety.cpp
index b00c31e253..1642b3add9 100644
--- a/src/mc/mc_safety.cpp
+++ b/src/mc/mc_safety.cpp
@@ -6,14 +6,14 @@
 
 #include <assert.h>
 
-#include "mc_state.h"
-#include "mc_request.h"
-#include "mc_safety.h"
-#include "mc_private.h"
-#include "mc_record.h"
-#include "mc_smx.h"
-#include "mc_client.h"
-#include "mc_exit.h"
+#include "src/mc/mc_state.h"
+#include "src/mc/mc_request.h"
+#include "src/mc/mc_safety.h"
+#include "src/mc/mc_private.h"
+#include "src/mc/mc_record.h"
+#include "src/mc/mc_smx.h"
+#include "src/mc/mc_client.h"
+#include "src/mc/mc_exit.h"
 
 #include "src/xbt/mmalloc/mmprivate.h"
 
@@ -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");