From 1b99e495635ba2190df60f54d1089a56d9bf3ffd Mon Sep 17 00:00:00 2001 From: Nicholas Kariniemi Date: Sat, 15 Aug 2015 16:51:25 +0300 Subject: [PATCH] Add identifiers to events --- csp/sync.csp | 36 ++++++++++++++++++++---------------- 1 file changed, 20 insertions(+), 16 deletions(-) diff --git a/csp/sync.csp b/csp/sync.csp index d864493..e47230d 100644 --- a/csp/sync.csp +++ b/csp/sync.csp @@ -1,38 +1,42 @@ +N = 2 S = 3 +CLIENTS = {0..N-1} STATES = {0..S-1} -channel input, render, up, down, save, saved:STATES +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?new_state - -> up!diff(shadow, new_state) + input.i?new_state + -> up!i!diff(shadow, new_state) -> CLIENT(i, new_state, shadow) -[] down?patch +[] down.i?patch -> if empty(patch) then CLIENT(i, state, state) else if diff(apply(shadow, patch), apply(state, patch)) != 0 - then up!diff(apply(shadow, patch), apply(state, patch)) - -> render!apply(state, patch) - -> CLIENT(i, apply(shadow, patch), apply(state, patch)) - else render!apply(state, patch) - -> CLIENT(i, apply(shadow, patch), apply(state, patch)) + 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?patch - -> save!patch - -> saved?new_state - -> down!diff(apply(shadow, patch), new_state) + up.i?patch + -> save!i!patch + -> saved.i?new_state + -> down!i!diff(apply(shadow, patch), new_state) -> SERVER(i, apply(shadow, patch)) -[] saved?new_state +[] saved?j?new_state -> if (new_state == shadow) then SERVER(i, shadow) - else down!diff(shadow, new_state) -> SERVER(i, new_state) + else down!i!diff(shadow, new_state) -> SERVER(i, new_state) -DB(state) = save?patch -> saved!apply(state, patch) -> DB(apply(state, patch)) +DB(state) = save?i?patch -> saved!i!apply(state, patch) -> DB(apply(state, patch)) state = 0 SYSTEM = CLIENT(0, state, state)