2015-08-15 13:51:25 +00:00
|
|
|
N = 2
|
2015-08-15 11:58:59 +00:00
|
|
|
S = 3
|
2015-08-15 13:51:25 +00:00
|
|
|
CLIENTS = {0..N-1}
|
2015-08-15 11:58:59 +00:00
|
|
|
STATES = {0..S-1}
|
2015-08-26 19:21:40 +00:00
|
|
|
PATCHES = {0..S-1}
|
|
|
|
channel input, render, saved, bufsaved:CLIENTS.STATES
|
|
|
|
channel up, down, save, bufdown:CLIENTS.PATCHES
|
2015-08-13 18:58:03 +00:00
|
|
|
|
2015-08-15 11:58:59 +00:00
|
|
|
apply(state, patch) = (state + patch) % S
|
2015-08-26 18:35:22 +00:00
|
|
|
diffS(state1, state2) = (state2 - state1) % S
|
2015-08-15 13:38:20 +00:00
|
|
|
empty(patch) = patch == 0
|
2015-08-13 19:25:18 +00:00
|
|
|
|
2015-08-15 11:58:59 +00:00
|
|
|
CLIENT(i, state, shadow) =
|
2015-08-26 18:35:22 +00:00
|
|
|
input!i?new_state:diff(STATES,{state})
|
|
|
|
-> up!i!diffS(shadow, new_state)
|
|
|
|
-> CLIENT'(i, new_state, shadow)
|
2015-08-15 15:32:25 +00:00
|
|
|
[] CLIENT'(i, state, shadow)
|
|
|
|
|
2015-08-26 19:21:40 +00:00
|
|
|
CLIENT'(i, state, shadow) = bufdown!i?patch
|
2015-08-15 13:38:20 +00:00
|
|
|
-> if empty(patch)
|
|
|
|
then CLIENT(i, state, state)
|
|
|
|
else
|
2015-08-26 19:09:10 +00:00
|
|
|
render!i!apply(state, patch)
|
|
|
|
-> if diffS(apply(shadow, patch), apply(state, patch)) != 0
|
2015-08-15 13:51:25 +00:00
|
|
|
then
|
2015-08-26 19:09:10 +00:00
|
|
|
up!i!diffS(apply(shadow, patch), apply(state, patch))
|
2015-08-15 13:51:25 +00:00
|
|
|
-> CLIENT(i, apply(state, patch), apply(shadow, patch))
|
2015-08-26 19:09:10 +00:00
|
|
|
else CLIENT(i, apply(state, patch), apply(shadow, patch))
|
2015-08-13 19:41:30 +00:00
|
|
|
|
2015-08-26 19:21:40 +00:00
|
|
|
DOWNBUF(i) = down!i?patch -> DOWNBUF'(i, patch)
|
|
|
|
DOWNBUF'(i, patch) = down!i?patch' -> DOWNBUF'(i, patch')
|
|
|
|
[] bufdown!i!patch -> DOWNBUF(i)
|
|
|
|
|
2015-08-15 12:14:27 +00:00
|
|
|
SERVER(i, shadow) =
|
2015-08-15 15:18:04 +00:00
|
|
|
up!i?patch
|
2015-08-15 13:51:25 +00:00
|
|
|
-> save!i!patch
|
2015-08-26 18:35:22 +00:00
|
|
|
-> saved!i?new_state
|
|
|
|
-> down!i!diffS(apply(shadow, patch), new_state)
|
2015-08-15 12:14:27 +00:00
|
|
|
-> SERVER(i, apply(shadow, patch))
|
2015-08-26 19:09:10 +00:00
|
|
|
[] bufsaved?j:diff(CLIENTS,{i})?new_state
|
2015-08-15 12:14:27 +00:00
|
|
|
-> if (new_state == shadow)
|
|
|
|
then SERVER(i, shadow)
|
2015-08-26 18:35:22 +00:00
|
|
|
else down!i!diffS(shadow, new_state) -> SERVER(i, new_state)
|
2015-08-13 19:41:30 +00:00
|
|
|
|
2015-08-26 19:21:40 +00:00
|
|
|
SAVEDBUF(i) = saved?j:diff(CLIENTS,{i})?new_state -> SAVEDBUF'(i, j, new_state)
|
|
|
|
SAVEDBUF'(i, j, new_state) = saved?j':diff(CLIENTS,{i})?new_state' -> SAVEDBUF'(i, j', new_state')
|
|
|
|
[] bufsaved!j!new_state -> SAVEDBUF(i)
|
2015-08-24 15:38:38 +00:00
|
|
|
|
|
|
|
DB(state) = save?i?patch
|
|
|
|
-> saved!i!apply(state, patch)
|
2015-08-19 17:50:08 +00:00
|
|
|
-> DB(apply(state, patch))
|
2015-08-15 12:14:27 +00:00
|
|
|
|
2015-08-26 19:21:40 +00:00
|
|
|
CONN(i, init) = (CLIENT(i, init, init) [|{| bufdown.i |}|] DOWNBUF(i)) [|{| up.i, down.i |}|] (SERVER(i, init) [|{| bufsaved |}|] SAVEDBUF(i))
|
2015-08-19 17:50:08 +00:00
|
|
|
SYSTEM = (CONN(0,0) [|{| save.0, saved |}|] DB(0)) [|{| save.1, saved |}|] CONN(1,0)
|
2015-08-13 18:58:03 +00:00
|
|
|
|
2015-08-26 18:35:22 +00:00
|
|
|
assert SYSTEM :[deadlock free [F]]
|
|
|
|
assert SYSTEM :[divergence-free]
|
|
|
|
|
|
|
|
-- Suppose that there are a finite number n of inputs.
|
|
|
|
-- I.e. users click around and then, at some point, after
|
|
|
|
-- n actions.
|
|
|
|
LimitedInputs(0) = STOP
|
|
|
|
LimitedInputs(n) = input?i?state -> LimitedInputs(n-1)
|
|
|
|
|
|
|
|
-- For instance, maybe only 3 actions occur.
|
|
|
|
LimitedSystem = LimitedInputs(3) [|{| input |}|] SYSTEM
|
|
|
|
|
|
|
|
-- If we look only at render events on each side
|
|
|
|
channel rend:STATES
|
|
|
|
Rends = render?i?state -> rend!state -> Rends
|
|
|
|
RendersLeft = (LimitedSystem [|{| render |}|] Rends) \diff(Events, productions(rend))
|
|
|
|
RendersRight = LimitedSystem \diff(Events, productions(render.1)) [|{| render |}|] Rends
|
|
|
|
|
|
|
|
-- Then (for any chosen n) the final event on both side
|
|
|
|
-- should be a render of the same final state s
|
|
|
|
-- i.e. the final events are render.0.s and render.1.s
|
|
|
|
-- for some s.
|
|
|
|
|
|
|
|
-- Can we specify this as a trace refinement?
|
|
|
|
|
|
|
|
-- The trace of the renders of each side should look like this:
|
|
|
|
-- T^<render.0.s>
|
|
|
|
-- S^<render.1.s>
|
|
|
|
|
|
|
|
-- What does it mean to say A [T= B? B trace-refines A i.e. traces(B) subset traces(A)
|
|
|
|
-- i.e. all possible traces of B occur within A
|
|
|
|
|
|
|
|
-- What if we force each side to coordinate with a process that, when done, emits a certain render event and then stops. Like renderLeft, renderRight?
|
|
|
|
-- We could force it to behave in such a way that it can only stop if both render the same event at the same time.
|
|
|
|
-- And then assert that it stops and does not diverge?
|
|
|
|
|
|
|
|
-- What does diverging mean again?
|
|
|
|
|
|
|
|
-- assert SYSTEM [T= InputsLeftS
|
|
|
|
-- assert RendersLeft [T= RendersRight
|
|
|
|
-- assert RendersRight [T= RendersLeft
|
|
|
|
|
|
|
|
|
|
|
|
-- Suppose an event occurs every time the system is in sync.
|
|
|
|
-- Or, more simplified, every time the two clients are in sync (excluding the database).
|
|
|
|
channel sync
|
|
|
|
SYNC(state) = sync -> SYNC'(state, state)
|
|
|
|
SYNC'(state0, state1) =
|
|
|
|
render!0?state -> (if state == state1 then sync -> SYNC'(state, state) else SYNC'(state, state1))
|
|
|
|
[] render!1?state -> (if state == state0 then sync -> SYNC'(state, state) else SYNC'(state0, state))
|
|
|
|
[] input?a?b -> SYNC'(state0, state1)
|
|
|
|
[] up?a?b -> SYNC'(state0, state1)
|
|
|
|
[] down?a?b -> SYNC'(state0, state1)
|
|
|
|
[] save?a?b -> SYNC'(state0, state1)
|
|
|
|
[] saved?a?b -> SYNC'(state0, state1)
|
|
|
|
[] bufsaved?a?b -> SYNC'(state0, state1)
|
|
|
|
|
|
|
|
--[] e:diff(Events, {sync}) @ e -> SYNC'(state0, state1)
|
|
|
|
--DoNothingOnNonSyncEvents = [] e:diff(Events, {sync}) @ e -> DoNothingOnNonSyncEvents
|
|
|
|
|
|
|
|
SyncSystem = SYSTEM [| diff(Events, {sync}) |] SYNC(0)
|