fact: Definition PB_input_handler (h : name) (i : PB_input) (d : PB_data) : list PB_output * PB_data * list (name * msg) := runGenHandler_ignore d ( match h, i with | Primary, Request r => d <- get ;; when (null (queue d)) (send (Backup, BackItUp r)) ;; set_queue (queue d ++ [r]) | _, Read => d <- get ;; write_output (ReadResponse (state d)) | _, _ => nop end).
imports: Verdi(Verdi HandlerMonad)