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)
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.


No differences found