Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
Have the application execute its transition before returning SIMCALL_EXECUTE_ANSWER
authorMartin Quinson <martin.quinson@ens-rennes.fr>
Fri, 18 Feb 2022 16:10:54 +0000 (17:10 +0100)
committerMartin Quinson <martin.quinson@ens-rennes.fr>
Fri, 18 Feb 2022 18:24:36 +0000 (19:24 +0100)
commit934f086b51d328c46cb8fb20db2ad3efd4668ac9
treea507cf0af9dda98f800eff9a9e6c886fe27f3566
parenta5b7657cca5d32f087dd62f2eca67f6a93c892ae
Have the application execute its transition before returning SIMCALL_EXECUTE_ANSWER

This makes the RPC protocol somewhat more complex, but it's mandatory
to get the updated observer.

This is useful in particular to Isend/Irecv observers that have a
set_comm() field that cannot be set before executing the simcall.
CommDet need that field anyway, so let's change the protocol that way.
src/mc/ModelChecker.cpp
src/mc/remote/AppSide.cpp