From 97890f029cd8f18dcf5acad193cc45cc1b946c3c Mon Sep 17 00:00:00 2001 From: Marion Guthmuller Date: Tue, 18 Feb 2014 14:26:28 +0100 Subject: [PATCH] model-checker : wait with timeout is always dependant with another transition --- src/mc/mc_request.c | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/src/mc/mc_request.c b/src/mc/mc_request.c index 5b7ce40864..98565b0837 100644 --- a/src/mc/mc_request.c +++ b/src/mc/mc_request.c @@ -17,7 +17,11 @@ int MC_request_depend(smx_simcall_t r1, smx_simcall_t r2) { return TRUE; if (r1->issuer == r2->issuer) - return FALSE; + return FALSE; + + /* Wait with timeout transitions are not considered by the independance theorem, thus we consider them as dependant with all other transitions */ + if((r1->call == SIMCALL_COMM_WAIT && simcall_comm_wait__get__timeout(r1) > 0) || (r2->call == SIMCALL_COMM_WAIT && simcall_comm_wait__get__timeout(r2) > 0)) + return TRUE; if(r1->call == SIMCALL_COMM_ISEND && r2->call == SIMCALL_COMM_IRECV) return FALSE; -- 2.20.1