diff --git a/csp/sync.csp b/csp/sync.csp index b12d529..7eb48c2 100644 --- a/csp/sync.csp +++ b/csp/sync.csp @@ -1,12 +1,19 @@ N = 3 -channel input, up, save:{0..N-1} +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) +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) -> SERVER(apply(state, patch), apply(shadow, patch)) + 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]] \ No newline at end of file