20c408e491
- Down buffer is no longer a sliding buffer of size one but just a buffer of size 1. It cannot be pushed into if it is full.
110 lines
No EOL
3.5 KiB
Text
110 lines
No EOL
3.5 KiB
Text
NUM_CLIENTS = 2
|
|
NUM_DB_STATES = 10
|
|
CLIENTS = {0..NUM_CLIENTS-1}
|
|
TIMES = {0..NUM_DB_STATES-1}
|
|
|
|
channel input:CLIENTS
|
|
channel save:CLIENTS
|
|
channel render:CLIENTS.TIMES
|
|
channel up:CLIENTS.TIMES
|
|
channel down:CLIENTS.TIMES.TIMES
|
|
channel bufdown:CLIENTS.TIMES.TIMES
|
|
channel saved:CLIENTS.TIMES
|
|
channel bufsaved:CLIENTS.TIMES
|
|
|
|
next_t(t) = (t + 1) % NUM_DB_STATES
|
|
|
|
CLIENT(i, t) =
|
|
input!i
|
|
-> up!i!t
|
|
-> CLIENT'(i, t)
|
|
[] CLIENT'(i, t)
|
|
|
|
CLIENT'(i, t) =
|
|
bufdown!i?client_t?server_t
|
|
-> render!i!server_t
|
|
-> CLIENT(i, server_t)
|
|
|
|
DOWNBUF(i) = down!i?client_t?server_t -> bufdown!i!client_t!server_t -> DOWNBUF(i)
|
|
|
|
SERVER(i, client_t) =
|
|
up!i?server_t
|
|
-> save!i
|
|
-> saved!i?new_server_t
|
|
-> down!i!server_t!new_server_t
|
|
-> SERVER(i, new_server_t)
|
|
[] bufsaved?j:diff(CLIENTS,{i})?new_server_t
|
|
-> if new_server_t == client_t
|
|
then SERVER(i, client_t)
|
|
else down!i!client_t!new_server_t
|
|
-> SERVER(i, new_server_t)
|
|
|
|
SAVEDBUF(i) = saved?j:diff(CLIENTS,{i})?t -> SAVEDBUF'(i, j, t)
|
|
SAVEDBUF'(i, j, t) = saved?j':diff(CLIENTS,{i})?new_t -> SAVEDBUF'(i, j', new_t)
|
|
[] bufsaved!j!t -> SAVEDBUF(i)
|
|
|
|
DB(t) = save?i
|
|
-> saved!i!next_t(t)
|
|
-> DB(next_t(t))
|
|
|
|
CONN(i, t0) = (CLIENT(i, t0) [|{| bufdown.i |}|] DOWNBUF(i)) [|{| up.i, down.i |}|] (SERVER(i, t0) [|{| bufsaved |}|] SAVEDBUF(i))
|
|
SYSTEM = (CONN(0,0) [|{| save.0, saved |}|] DB(0)) [|{| save.1, saved |}|] CONN(1,0)
|
|
|
|
|
|
-----------------------------------------
|
|
-- Assertions
|
|
-----------------------------------------
|
|
|
|
assert SYSTEM :[deadlock free [F]]
|
|
assert SYSTEM :[divergence-free]
|
|
|
|
-----------------------------------------
|
|
-- One way sync: changes on one client will sync to other client
|
|
-----------------------------------------
|
|
|
|
-- Suppose we limit our specification to say that each
|
|
-- user makes a finite number of changes n.
|
|
MaxInputs(0) = STOP
|
|
MaxInputs(n) = input?i -> MaxInputs(n-1)
|
|
|
|
-- Suppose we limit inputs to client 0.
|
|
|
|
OnlyClient(i) = input!i -> OnlyClient(i)
|
|
ClientZeroInput = OnlyClient(0) [|{| input |}|] SYSTEM
|
|
|
|
OneInputFromClientZero = (OnlyClient(0) [|{| input |}|] MaxInputs(1)) [|{| input |}|] SYSTEM
|
|
|
|
-- Now we show that a change on client 0 will make it to client 1.
|
|
|
|
SyncOneInput = input.0 -> render.1.1 -> STOP
|
|
assert SyncOneInput [FD= OneInputFromClientZero \diff(Events, {input.0, render.1.1})
|
|
|
|
-- Expanding on this: what if we have two changes? We just care that, eventually, both of them get synced.
|
|
SyncTwoInputs = input.0 -> input.0 -> render.1.2 -> STOP
|
|
|
|
assert SyncTwoInputs [FD= (ClientZeroInput [|{| input |}|] MaxInputs(2)) \diff(Events, {input.0, render.1.2})
|
|
|
|
-- Can we do this for an arbitrary n changes?
|
|
OneWaySync(n) = input.0 -> OneWaySync'(n, n-1)
|
|
OneWaySync'(n, 0) = render.1.n -> STOP
|
|
OneWaySync'(n, i) = input.0 -> OneWaySync'(n, i-1)
|
|
|
|
OneSideInputs(n) = (ClientZeroInput [|{| input |}|] MaxInputs(n)) \diff(Events, {input.0, render.1.n})
|
|
|
|
assert OneWaySync(1) [FD= OneSideInputs(1)
|
|
assert OneWaySync(9) [FD= OneSideInputs(9)
|
|
|
|
-----------------------------------------
|
|
-- Two way sync: changes on both clients will sync to both
|
|
-----------------------------------------
|
|
|
|
-- Start simple.
|
|
-- Let's just constrain our system to say, first client 0 does a change then client 1 does a change.
|
|
|
|
AlternateInputs = input.0 -> input.1 -> STOP
|
|
|
|
-- Then our specification becomes simple:
|
|
TwoWaySync = input.0 -> input.1 -> ((render.0.2 -> render.1.2 -> STOP) |~|
|
|
(render.1.2 -> render.0.2 -> STOP))
|
|
|
|
assert TwoWaySync [FD= (SYSTEM [|{| input |}|] AlternateInputs) \diff(Events, {input.0, input.1, render.0.2, render.1.2}) |