86 lines
No EOL
2.6 KiB
Text
86 lines
No EOL
2.6 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
|
|
-> render!i!t
|
|
-> 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 -> DOWNBUF'(i, client_t, server_t)
|
|
DOWNBUF'(i, client_t, server_t) =
|
|
down!i?client_t'?server_t' -> DOWNBUF'(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]
|
|
|
|
|
|
-----------------------------------------
|
|
-- Simple sync: one change will sync to other client
|
|
-----------------------------------------
|
|
|
|
-- Suppose we limit our specification to say that each
|
|
-- user makes a finite number of changes n.
|
|
LimitedInputs(0) = STOP
|
|
LimitedInputs(n) = input?i -> LimitedInputs(n-1)
|
|
|
|
-- Suppose we limit inputs to client 0.
|
|
|
|
ClientInputs(i) = input!i -> ClientInputs(i)
|
|
ClientZeroInput = ClientInputs(0) [|{| input |}|] SYSTEM
|
|
|
|
OneInputFromClientZero = (ClientZeroInput [|{| input |}|] LimitedInputs(1))
|
|
|
|
-- Now, we want to show that given these constraints, when a change comes in on client 0, the change will be rendered on both client 0 and client 1.
|
|
|
|
SyncOneInputNondeterm = input.0 -> render.0.0 -> (render.0.1 -> render.1.1 -> STOP |~|
|
|
render.1.1 -> render.0.1 -> STOP)
|
|
assert SyncOneInputNondeterm [FD= OneInputFromClientZero \diff(Events, {input.0, render.0.0, render.0.1, render.1.1}) |