diff --git a/csp/sync.csp b/csp/sync.csp index 855cadf..b12d529 100644 --- a/csp/sync.csp +++ b/csp/sync.csp @@ -1,7 +1,12 @@ -channel input:{0,1,2} +N = 3 +channel input, up, save:{0..N-1} -USER(i) = input!i -> USER((i+1)%3) -CLIENT(i) = input?j -> CLIENT(j) -SYSTEM = USER(0) ||| CLIENT(0) +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]] \ No newline at end of file