Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
Ensure that the verified application still works if get_max_consider() is not called...
authorMartin Quinson <martin.quinson@ens-rennes.fr>
Mon, 1 Aug 2022 22:15:48 +0000 (00:15 +0200)
committerMartin Quinson <martin.quinson@ens-rennes.fr>
Mon, 1 Aug 2022 22:15:51 +0000 (00:15 +0200)
commitdd493bf4a168bd2b379810313916e1a4e0898388
treeec6a8f100a4259e40b36c42b8249ae4ce405027a
parent67c9ff3524ec0e35477c67a487f906b1fe772ab4
Ensure that the verified application still works if get_max_consider() is not called at a given depth

This can happen after a backtrack: the Checker already knows how many
times this can be considered, but the App was reset in between so it
forgot.

So, make get_max_consider() const, and do the initialization in the
observer constructor, where it belongs. Too bad for the tiny little
tiny loss of performance compared to the lazy initialization.
src/kernel/actor/CommObserver.cpp
src/kernel/actor/CommObserver.hpp
src/kernel/actor/SimcallObserver.cpp
src/kernel/actor/SimcallObserver.hpp
src/mc/mc_base.cpp