Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
model-checker : last fix in DPOR algorithm if max depth is reached
authorMarion Guthmuller <marion.guthmuller@loria.fr>
Mon, 25 Mar 2013 21:02:50 +0000 (22:02 +0100)
committerMarion Guthmuller <marion.guthmuller@loria.fr>
Mon, 25 Mar 2013 22:11:00 +0000 (23:11 +0100)
commitd2bf506bf4ebad03e01464d88a0635165ca8a4ed
tree80a20e3c17dbe226874f8672e48633763664aa02
parent5909c08d89f790f21908c7d2d392a63212df31e8
model-checker : last fix in DPOR algorithm if max depth is reached

If max_depth is reached, the last state in stack may have a process
interleaved with a request not executed yet. In that case, we start to
apply the independence theorem with this last request not executed
yet. Otherwise (no more process to interleave in the last state of the
stack), last state is deleted before starting to apply independence theorem.
src/mc/mc_dpor.c
src/mc/mc_global.c