Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
model-checker : fix dependance theorem according to TLA+ specification
authorMarion Guthmuller <marion.guthmuller@loria.fr>
Thu, 15 Nov 2012 20:53:16 +0000 (21:53 +0100)
committerMarion Guthmuller <marion.guthmuller@loria.fr>
Thu, 15 Nov 2012 21:03:14 +0000 (22:03 +0100)
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

index cdd8c33..332e857 100644 (file)
@@ -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)