From 864cdc455e38de68e3666a03e17d5a4cb0d7acaf Mon Sep 17 00:00:00 2001 From: Marion Guthmuller Date: Thu, 15 Nov 2012 21:53:16 +0100 Subject: [PATCH] model-checker : fix dependance theorem according to TLA+ specification iSend and iRecv requests are dependant with Test requests if process issuer is different. On the path iRecv->iSend->Test, test return true but on the path iRecv/Test/iSend, test return false. So, each interleaving must be explored. --- src/mc/mc_request.c | 9 ++++----- 1 file changed, 4 insertions(+), 5 deletions(-) diff --git a/src/mc/mc_request.c b/src/mc/mc_request.c index cdd8c33679..332e85764d 100644 --- a/src/mc/mc_request.c +++ b/src/mc/mc_request.c @@ -15,7 +15,6 @@ int MC_request_depend(smx_simcall_t r1, smx_simcall_t r2) { if(mc_reduce_kind == e_mc_reduce_none) return TRUE; - if (r1->issuer == r2->issuer) return FALSE; @@ -64,16 +63,16 @@ int MC_request_depend(smx_simcall_t r1, smx_simcall_t r2) { /* FIXME: the following rule assumes that the result of the * isend/irecv call is not stored in a buffer used in the * test call. */ - if( (r1->call == SIMCALL_COMM_ISEND || r1->call == SIMCALL_COMM_IRECV) + /*if( (r1->call == SIMCALL_COMM_ISEND || r1->call == SIMCALL_COMM_IRECV) && r2->call == SIMCALL_COMM_TEST) - return FALSE; + return FALSE;*/ /* FIXME: the following rule assumes that the result of the * isend/irecv call is not stored in a buffer used in the * test call.*/ - if( (r2->call == SIMCALL_COMM_ISEND || r2->call == SIMCALL_COMM_IRECV) + /*if( (r2->call == SIMCALL_COMM_ISEND || r2->call == SIMCALL_COMM_IRECV) && r1->call == SIMCALL_COMM_TEST) - return FALSE; + return FALSE;*/ if(r1->call == SIMCALL_COMM_ISEND && r2->call == SIMCALL_COMM_ISEND && r1->comm_isend.rdv != r2->comm_isend.rdv) -- 2.20.1