Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
model-checker : fix dpor algorithm
authorMarion Guthmuller <marion.guthmuller@loria.fr>
Fri, 16 Nov 2012 16:04:05 +0000 (17:04 +0100)
committerMarion Guthmuller <marion.guthmuller@loria.fr>
Fri, 16 Nov 2012 16:04:05 +0000 (17:04 +0100)
commitead8b3a1775defecebc316cb5e4fcddbd283df4c
tree377aa6bfa43bceeb0a7e7d8bf7419ade0f624090
parent01bcdf570c06d71a9a6daa471733915fef91bb1f
model-checker : fix dpor algorithm

  - Interleave all enabled processes for each state
  - If max_depth reached and last state still have processes interleaved, backtrack on this state (reduction not applied)"
  - If independant transitions, corresponding process interleaved in previous state is disabled (MC_DONE)
src/mc/mc_dpor.c
src/mc/mc_private.h
src/mc/mc_state.c