Skip to content

Fixes on DPOR algorithm for MC SimGrid and sleep sets addition

Mathieu Laurent requested to merge (removed):master into master

DPOR Bug fix

Several little things prevented the algorithm from being sound when doing DPOR reduction, mostly during the backtrack procedure:

  • transitions from a same processus should be ignored when looking for a dependent one
  • after finding 2 dependent transitions, we can't always mark the process of the latter as todo because it may not be enabled. In this case, either one implement something like Lamport's vector clock to find the best transition to add, or we simply mark each enabled transition as todo (which is what is proposed in this fix)
  • when calling State::next_transition(), actors in done set could still be picked when calling

Sleep set implementation

Sleep set are supposed to be set of actors that we don't need to consider when looking for a next transition in a given state. In the code, it is stored as a std::map<aid_t, Transition>.

  • It starts empty
  • When backtracking from a transition, the transition is added to the sleep set with the corresponding actor
  • When opening a new state during the exploration, if sleep set are enabled, a different constructor is called and will copy the sleep set from the previous state, removing transitions that are dependent with the one just taken, and marking done transitions still in sleep set

Remaining modifications correspond to what I think I needed to do in order to have --cfg=model-check/sleep-set as a command-line option.

Merge request reports