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
model-checker : iSend/iRecv independent with Wait but not with WaitTimeout
[simgrid.git]
/
src
/
mc
/
mc_request.c
diff --git
a/src/mc/mc_request.c
b/src/mc/mc_request.c
index
c57dc08
..
f92580b
100644
(file)
--- a/
src/mc/mc_request.c
+++ b/
src/mc/mc_request.c
@@
-32,13
+32,13
@@
int MC_request_depend(smx_simcall_t r1, smx_simcall_t r2) {
smx_rdv_t rdv = r1->call == SIMCALL_COMM_ISEND ? simcall_comm_isend__get__rdv(r1) : simcall_comm_irecv__get__rdv(r1);
smx_rdv_t rdv = r1->call == SIMCALL_COMM_ISEND ? simcall_comm_isend__get__rdv(r1) : simcall_comm_irecv__get__rdv(r1);
- if(
simcall_comm_wait__get__comm(r2)->comm.rdv != rdv
)
+ if(
(simcall_comm_wait__get__comm(r2)->comm.rdv != rdv) && (simcall_comm_wait__get__timeout(r2) <= 0)
)
return FALSE;
return FALSE;
- if(
simcall_comm_wait__get__comm(r2)->comm.type == SIMIX_COMM_SEND && r1->call == SIMCALL_COMM_ISEND
)
+ if(
(simcall_comm_wait__get__comm(r2)->comm.type == SIMIX_COMM_SEND) && (r1->call == SIMCALL_COMM_ISEND) && (simcall_comm_wait__get__timeout(r2) <= 0)
)
return FALSE;
return FALSE;
- if(
simcall_comm_wait__get__comm(r2)->comm.type == SIMIX_COMM_RECEIVE && r1->call == SIMCALL_COMM_IRECV
)
+ if(
(simcall_comm_wait__get__comm(r2)->comm.type == SIMIX_COMM_RECEIVE) && (r1->call == SIMCALL_COMM_IRECV) && (simcall_comm_wait__get__timeout(r2) <= 0)
)
return FALSE;
}
return FALSE;
}
@@
-50,13
+50,13
@@
int MC_request_depend(smx_simcall_t r1, smx_simcall_t r2) {
smx_rdv_t rdv = r2->call == SIMCALL_COMM_ISEND ? simcall_comm_isend__get__rdv(r2) : simcall_comm_irecv__get__rdv(r2);
smx_rdv_t rdv = r2->call == SIMCALL_COMM_ISEND ? simcall_comm_isend__get__rdv(r2) : simcall_comm_irecv__get__rdv(r2);
- if(
simcall_comm_wait__get__comm(r1)->comm.rdv != rdv
)
+ if(
(simcall_comm_wait__get__comm(r1)->comm.rdv != rdv) && (simcall_comm_wait__get__timeout(r1) <= 0)
)
return FALSE;
return FALSE;
- if(
simcall_comm_wait__get__comm(r1)->comm.type == SIMIX_COMM_SEND && r2->call == SIMCALL_COMM_ISEND
)
+ if(
(simcall_comm_wait__get__comm(r1)->comm.type == SIMIX_COMM_SEND) && (r2->call == SIMCALL_COMM_ISEND) && (simcall_comm_wait__get__timeout(r1) <= 0)
)
return FALSE;
return FALSE;
- if(
simcall_comm_wait__get__comm(r1)->comm.type == SIMIX_COMM_RECEIVE && r2->call == SIMCALL_COMM_IRECV
)
+ if(
(simcall_comm_wait__get__comm(r1)->comm.type == SIMIX_COMM_RECEIVE) && (r2->call == SIMCALL_COMM_IRECV) && (simcall_comm_wait__get__timeout(r1) <= 0)
)
return FALSE;
}
return FALSE;
}