NUM_CLIENTS = 2
NUM_DB_STATES = 10
CLIENTS = {0..NUM_CLIENTS-1}
TIMES = {0..NUM_DB_STATES-1}

channel save:CLIENTS
channel render:CLIENTS.TIMES
channel up:CLIENTS.TIMES
channel down:CLIENTS.TIMES.TIMES
channel saved:CLIENTS.TIMES
channel report_queue:CLIENTS.TIMES

next_t(t) = (t + 1) % NUM_DB_STATES

CLIENT(i, t) = up!i!t -> CLIENT'(i, t) [] CLIENT'(i, t)

CLIENT'(i, t) = 
   down!i?client_t?server_t
   -> render!i!server_t
   -> CLIENT(i, server_t)

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)
[] report_queue?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)

REPORTQUEUE(i) = saved?j:diff(CLIENTS,{i})?t -> REPORTQUEUE'(i, j, t)
REPORTQUEUE'(i, j, t) = saved?j':diff(CLIENTS,{i})?new_t -> REPORTQUEUE'(i, j', new_t)
   [] report_queue!j!t -> REPORTQUEUE(i)

DB(t) = save?i
   -> saved!i!next_t(t)
   -> DB(next_t(t))

CONN(i, t0) = CLIENT(i, t0) [|{| up.i, down.i |}|] (SERVER(i, t0) [|{| report_queue |}|] REPORTQUEUE(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) = up?i?t -> MaxInputs(n-1)

-- Suppose we limit inputs to client 0.

OnlyClient(i) = up!i?t -> OnlyClient(i)
ClientZeroInput = OnlyClient(0) [|{| up |}|] SYSTEM

OneInputFromClientZero = (OnlyClient(0) [|{| up |}|] MaxInputs(1)) [|{| up |}|] SYSTEM

-- Now we show that a change on client 0 will make it to client 1.

SyncOneInput = up.0.0 -> render.1.1 -> STOP
assert SyncOneInput [FD= OneInputFromClientZero \diff(Events, union(productions(up.0), {render.1.1}))

-- Expanding on this: what if we have two changes? We just care that, eventually, both of them get synced.
SyncTwoInputs = up.0.0 -> up.0.1 -> render.1.2 -> STOP

assert SyncTwoInputs [FD= (ClientZeroInput [|{| up |}|] MaxInputs(2)) \diff(Events, union(productions(up.0), {render.1.2}))

-- Can we do this for an arbitrary n changes?
OneWaySync(n) = up.0.0 -> OneWaySync'(n, n-1)
OneWaySync'(n, 0) = render.1.n -> STOP
OneWaySync'(n, i) = up.0.n-i -> OneWaySync'(n, i-1)

OneSideInputs(n) = (ClientZeroInput [|{| up |}|] MaxInputs(n)) \diff(Events, union(productions(up.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 = up.0.0 -> up.1?t -> STOP

-- Then our specification becomes simple. If client 0 inputs something then client one inputs something, at some point both should call render with the state after both changes hit the database (t=2).
TwoWaySync = up.0.0 -> ((up.1.0 -> TwoWaySyncRender) |~|
                        (up.1.1 -> TwoWaySyncRender))
TwoWaySyncRender = ((render.0.2 -> render.1.2 -> STOP) |~|
                    (render.1.2 -> render.0.2 -> STOP))

assert TwoWaySync [FD= (SYSTEM [|{| up |}|] AlternateInputs) \diff(Events, union(union(productions(up.0), productions(up.1)), {render.0.2, render.1.2}))