grub-fork/csp/sync.csp

55 lines
1.6 KiB
Text
Raw Normal View History

2015-08-15 16:51:25 +03:00
N = 2
S = 3
2015-08-15 16:51:25 +03:00
CLIENTS = {0..N-1}
STATES = {0..S-1}
channel input, render, up, down, save, saved, bufsave, bufsaved:CLIENTS.STATES
2015-08-13 21:58:03 +03:00
apply(state, patch) = (state + patch) % S
diff(state1, state2) = (state2 - state1) % S
2015-08-15 16:38:20 +03:00
empty(patch) = patch == 0
2015-08-13 22:25:18 +03:00
CLIENT(i, state, shadow) =
input!i?new_state
2015-08-15 16:51:25 +03:00
-> up!i!diff(shadow, new_state)
-> CLIENT'(i, state, shadow)
[] CLIENT'(i, state, shadow)
CLIENT'(i, state, shadow) = down!i?patch
2015-08-15 16:38:20 +03:00
-> if empty(patch)
then CLIENT(i, state, state)
else
if diff(apply(shadow, patch), apply(state, patch)) != 0
2015-08-15 16:51:25 +03:00
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))
2015-08-13 22:41:30 +03:00
2015-08-15 15:14:27 +03:00
SERVER(i, shadow) =
up!i?patch
2015-08-15 16:51:25 +03:00
-> save!i!patch
-> bufsaved!i?new_state
2015-08-15 16:51:25 +03:00
-> down!i!diff(apply(shadow, patch), new_state)
2015-08-15 15:14:27 +03:00
-> SERVER(i, apply(shadow, patch))
[] bufsaved?j?new_state
2015-08-15 15:14:27 +03:00
-> if (new_state == shadow)
then SERVER(i, shadow)
2015-08-15 16:51:25 +03:00
else down!i!diff(shadow, new_state) -> SERVER(i, new_state)
2015-08-13 22:41:30 +03:00
BUF(i) = saved?j?new_state -> BUF'(i, j, new_state)
BUF'(i, j, new_state) = saved?j'?new_state' -> BUF'(i, j', new_state')
[] bufsaved!j!new_state -> BUF(i)
DB(state) = save?i?patch
-> saved!i!apply(state, patch)
-> DB(apply(state, patch))
2015-08-15 15:14:27 +03:00
DBB = DB(0)
CONN(i, init) = (CLIENT(i, init, init) [|{| up.i, down.i |}|] SERVER(i, init)) [|{| bufsaved |}|] BUF(i)
SYSTEM = (CONN(0,0) [|{| save.0, saved |}|] DB(0)) [|{| save.1, saved |}|] CONN(1,0)
2015-08-13 21:58:03 +03:00
assert SYSTEM :[deadlock free [F]]