___________________________________________________________________
Fully defined deterministic scheduler with 2 memory states:
model state:     memory:     choice(s)     memory updates:     
    0: [s=0]    m       0    0 {a0}            model state' = 1: -> (m' = 0), model state' = 2: -> (m' = 1)
    1: [s=1]    m       0    1 {b}            model state' = 3: -> (m' = 0)
    2: [s=3]    m       1    0 {}            model state' = 2: -> (m' = 1)
    3: [s=4]    m       0    0 {}            model state' = 3: -> (m' = 0)
___________________________________________________________________