A
lgorithmique
N
umérique
D
istribuée
Public GIT Repository
projects
/
simgrid.git
/ blobdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
raw
|
inline
| side by side
[mc] Move the MCer wait_for_requests logic outside of MC_wait_for_requests
[simgrid.git]
/
src
/
mc
/
mc_safety.cpp
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) */
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;
/* 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);
/* 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();
/* 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");
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");
XBT_DEBUG("Starting the safety algorithm");