Implement Optimal DPOR #40
Description
"Source-set DPOR" (described in #39) may still search what is termed "sleep-set blocked" traces, i.e. traces that are ultimately equivalent to one already searched. The paper presents a (provably) optimal implementation of DPOR using wakeup trees. Wakeup trees guarantee that each Mazurkiewicz trace that is searched is distinct (i.e. not equivalent) to any other trace searched by McMini. In other words, it performs as best as it can. This would add significant complexity to McMini though, as the wakeup tree data structure is rather complicated.