CSP: Clean up syntax of simpler model

spec/sync.csp

@@ -6,16 +6,18 @@ TIMES = {0..NUM_DB_STATES-1}
 channel save:CLIENTS
 channel render:CLIENTS.TIMES
 channel up:CLIENTS.TIMES
-channel down:CLIENTS.TIMES.TIMES
+channel down:CLIENTS.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) = 
+   up!i!t -> CLIENT'(i, t)
+[] CLIENT'(i, t)
 
 CLIENT'(i, t) = 
-   down!i?client_t?server_t
+   down!i?server_t
    -> render!i!server_t
    -> CLIENT(i, server_t)
 
@@ -23,27 +25,31 @@ SERVER(i, client_t) =
    up!i?server_t
    -> save!i
    -> saved!i?new_server_t
-   -> down!i!server_t!new_server_t
+   -> down!i!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
+      else down!i!new_server_t
         -> SERVER(i, new_server_t)
 
-REPORTQUEUE(i) = saved?j:diff(CLIENTS,{i})?t -> REPORTQUEUE'(i, j, t)
+DB(t) =
-REPORTQUEUE'(i, j, t) = saved?j':diff(CLIENTS,{i})?new_t -> REPORTQUEUE'(i, j', new_t)
+   save?i
-   [] 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))
+REPORTQUEUE(i) =
-SYSTEM = ((CONN(0,0) [|{| save.0, saved |}|] DB(0)) [|{| save.1, saved |}|] CONN(1,0)) [| diff(productions(save), {save.0, save.1}) |] STOP
+   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)
 
-CONNS = [| productions(saved) |] i:CLIENTS @ CONN(i, 0)
+SERVER_WITH_REPORTS(i, t0) = (SERVER(i, t0) [|{| report_queue |}|] REPORTQUEUE(i))
-SYSTEM' = DB(0) [|{| save, saved |}|] CONNS
+CONN(i, t0) = CLIENT(i, t0) [|{| up.i, down.i |}|] SERVER_WITH_REPORTS(i, t0)
+CONNS(t0) = [| productions(saved) |] i:CLIENTS @ CONN(i, t0)
+SYSTEM = DB(0) [|{| save, saved |}|] CONNS(0)
 
 -----------------------------------------
 -- Assertions
@@ -131,7 +137,7 @@ SyncThree'(n, 0) =
   (render.2.n -> render.1.n -> render.0.n -> STOP)
 SyncThree'(n, m) = |~| i:CLIENTS, t:TIMES @ up!i!t -> SyncThree'(n, m-1)
 
-MaxInputSystem(n) = SYSTEM' [|{| up |}|] MaxInputs(n)
+MaxInputSystem(n) = SYSTEM [|{| up |}|] MaxInputs(n)
 assert SyncThree(5) [FD= MaxInputSystem(5) \diff(Events, union(productions(up), {render.i.5 | i <- CLIENTS}))
 
 -----------------------------------------