fact: Definition PB_net (dst src : name) (m : msg) : PB_data -> list PB_output * PB_data * list (name * msg) := fun x => runGenHandler_ignore x ( match dst, m with | Primary, Ack => d <- get ;; match queue d with | [] => nop | x :: xs => match xs with | [] => nop | y :: ys => send (Backup, BackItUp y) end ;; let (os, st') := handler x (state d) in write_output (RequestResponse x os) ;; set_state st' ;; set_queue xs end | Backup, BackItUp i => d <- get ;; set_state (snd (handler i (state d))) ;; send (Primary, Ack) | _, _ => nop end).
imports: Verdi(Verdi HandlerMonad)