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]

-----------------------------------------
-- 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)