Logo AND Algorithmique Numérique Distribuée
Public GIT Repository
projects / simgrid.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 427ce11) | patch
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)
commit864cdc455e38de68e3666a03e17d5a4cb0d7acaf
tree34e00ed88a354ee6623d352656be72dd411c24c7tree | snapshot
parent427ce11c29a6a5b78045e0c0f703dd52a400e8eacommit | diff
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 diff | blob | history
Clone of SimGrid repository with local patches