fact: Definition operate (op : input) (curr : option value) := match op with | Get _ => (curr, curr) | Put _ v => (Some v, curr) | Del _ => (None, curr) | CAS _ v v' => if val_eq_dec curr v then (Some v', curr) else (curr, curr) | CAD _ v => if val_eq_dec curr (Some v) then (None, curr) else (curr, curr) end.
imports: Verdi(Verdi) Coq(FMapList String) Verdi(FMapVeryWeak StateMachineHandlerMonad)