2015-08-15 14:58:59 +03:00
|
|
|
S = 3
|
|
|
|
STATES = {0..S-1}
|
2015-08-15 15:14:27 +03:00
|
|
|
channel input, render, up, down, save, saved:STATES
|
2015-08-13 21:58:03 +03:00
|
|
|
|
2015-08-15 14:58:59 +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
|
|
|
|
2015-08-15 14:58:59 +03:00
|
|
|
CLIENT(i, state, shadow) =
|
2015-08-15 15:14:27 +03:00
|
|
|
input?new_state
|
|
|
|
-> up!diff(shadow, new_state)
|
|
|
|
-> CLIENT(i, new_state, shadow)
|
|
|
|
[] down?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
|
|
|
|
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))
|
2015-08-13 22:41:30 +03:00
|
|
|
|
2015-08-15 15:14:27 +03:00
|
|
|
SERVER(i, shadow) =
|
|
|
|
up?patch
|
|
|
|
-> save!patch
|
|
|
|
-> saved?new_state
|
|
|
|
-> down!diff(apply(shadow, patch), new_state)
|
|
|
|
-> SERVER(i, apply(shadow, patch))
|
|
|
|
[] saved?new_state
|
|
|
|
-> if (new_state == shadow)
|
|
|
|
then SERVER(i, shadow)
|
|
|
|
else down!diff(shadow, new_state) -> SERVER(i, new_state)
|
2015-08-13 22:41:30 +03:00
|
|
|
|
2015-08-15 15:14:27 +03:00
|
|
|
DB(state) = save?patch -> saved!apply(state, patch) -> DB(apply(state, patch))
|
|
|
|
|
|
|
|
state = 0
|
|
|
|
SYSTEM = CLIENT(0, state, state)
|
|
|
|
||| CLIENT(1, state, state)
|
|
|
|
||| SERVER(0, state)
|
|
|
|
||| SERVER(1, state)
|
|
|
|
||| DB(state)
|
2015-08-13 21:58:03 +03:00
|
|
|
|
|
|
|
assert SYSTEM :[deadlock free [F]]
|