N = 2
S = 3
CLIENTS = {0..N-1}
STATES = {0..S-1}
channel input, render, up, down, save, saved:CLIENTS.STATES

apply(state, patch) = (state + patch) % S
diff(state1, state2) = (state2 - state1) % S
empty(patch) = patch == 0

CLIENT(i, state, shadow) = 
   input!i?new_state
   -> up!i!diff(shadow, new_state)
   -> CLIENT'(i, state, shadow)
[] CLIENT'(i, state, shadow)

CLIENT'(i, state, shadow) = down!i?patch
   -> if empty(patch)
     then CLIENT(i, state, state)
     else 
       if diff(apply(shadow, patch), apply(state, patch)) != 0
       then 
         render!i!apply(state, patch)
         -> up!i!diff(apply(shadow, patch), apply(state, patch))
         -> CLIENT(i, apply(state, patch), apply(shadow, patch))
       else
         render!i!apply(state, patch)
         -> CLIENT(i, apply(state, patch), apply(shadow, patch))

SERVER(i, shadow) = 
   up!i?patch
   -> save!i!patch
   -> saved!i?new_state
   -> down!i!diff(apply(shadow, patch), new_state)
   -> SERVER(i, apply(shadow, patch))
[] saved?j?new_state
   -> if (new_state == shadow)
      then SERVER(i, shadow)
      else down!i!diff(shadow, new_state) -> SERVER(i, new_state)

DB(state) = save?i?patch 
   -> saved!i!apply(state, patch) 
   -> DB(apply(state, patch))

CONN(i, init) = CLIENT(i, init, init) [|{| up.i, down.i |}|] SERVER(i, init)

SYSTEM = (CONN(0,0) [|{| save.0, saved |}|] DB(0)) [|{| save.1, saved |}|] CONN(1,0)

assert SYSTEM :[deadlock free [F]]