michael/grub-fork
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

Add identifiers to events

Browse source
This commit is contained in:
Nicholas Kariniemi 2015-08-15 16:51:25 +03:00
parent da0541518e
commit 1b99e49563
1 changed files with 20 additions and 16 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

36
csp/sync.csp
View file

@ -1,38 +1,42 @@
N = 2
S = 3 S = 3
CLIENTS = {0..N-1}
STATES = {0..S-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 apply(state, patch) = (state + patch) % S
diff(state1, state2) = (state2 - state1) % S diff(state1, state2) = (state2 - state1) % S
empty(patch) = patch == 0 empty(patch) = patch == 0
CLIENT(i, state, shadow) = CLIENT(i, state, shadow) =
input?new_state input.i?new_state
-> up!diff(shadow, new_state) -> up!i!diff(shadow, new_state)
-> CLIENT(i, new_state, shadow) -> CLIENT(i, new_state, shadow)
[] down?patch [] down.i?patch
-> if empty(patch) -> if empty(patch)
then CLIENT(i, state, state) then CLIENT(i, state, state)
else else
if diff(apply(shadow, patch), apply(state, patch)) != 0 if diff(apply(shadow, patch), apply(state, patch)) != 0
then up!diff(apply(shadow, patch), apply(state, patch)) then
-> render!apply(state, patch) render!i!apply(state, patch)
-> CLIENT(i, apply(shadow, patch), apply(state, patch)) -> up!i!diff(apply(shadow, patch), apply(state, patch))
else render!apply(state, patch) -> CLIENT(i, apply(state, patch), apply(shadow, patch))
-> CLIENT(i, apply(shadow, patch), apply(state, patch)) else
render!i!apply(state, patch)
-> CLIENT(i, apply(state, patch), apply(shadow, patch))
SERVER(i, shadow) = SERVER(i, shadow) =
up?patch up.i?patch
-> save!patch -> save!i!patch
-> saved?new_state -> saved.i?new_state
-> down!diff(apply(shadow, patch), new_state) -> down!i!diff(apply(shadow, patch), new_state)
-> SERVER(i, apply(shadow, patch)) -> SERVER(i, apply(shadow, patch))
[] saved?new_state [] saved?j?new_state
-> if (new_state == shadow) -> if (new_state == shadow)
then SERVER(i, 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 state = 0
SYSTEM = CLIENT(0, state, state) SYSTEM = CLIENT(0, state, state)