fact: Definition ClientIOHandler (i : Client_index) (m : Msg) : Handler Data := match m with | Lock => send (Server, Lock) | Unlock => data <- get ;; when (held data) (put (mkData [] false) >> send (Server, Unlock)) | _ => nop end.
imports: Verdi(Verdi HandlerMonad) StructTact(Fin) Verdi(StatePacketPacketDecomposition)