N = 3
channel input, render, up, down, save:{0..N-1}

apply(state, patch) = (state + patch) % N
diff(state1, state2) = (state2 - state1) % N

CLIENT(state, shadow) = 
   input?new_state -> up!diff(shadow, new_state) -> CLIENT(new_state, shadow)
[] down?patch -> if patch != 0 
     then render!apply(state, patch) -> CLIENT(apply(state, patch), apply(shadow, patch))
     else CLIENT(state, state)

SERVER(state, shadow) = 
  up?patch -> save!apply(state, patch) -> down!diff(apply(shadow, patch), apply(state, patch))
  -> SERVER(apply(state, patch), apply(shadow, patch))

SYSTEM = CLIENT(0, 0) ||| SERVER(0, 0)

assert SYSTEM :[deadlock free [F]]