grub-fork/csp/sync.csp

N = 3
channel input, up, 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)
SERVER(state, shadow) = 
  up?patch -> save!apply(state, patch) -> SERVER(apply(state, patch), apply(shadow, patch))
SYSTEM = CLIENT(0, 0) ||| SERVER(0, 0)

assert SYSTEM :[deadlock free [F]]