From bc5921b2dcc8813e82c926f201df18f506c7fd18 Mon Sep 17 00:00:00 2001
From: Nicholas Kariniemi <nicholas.kariniemi@reaktor.com>
Date: Tue, 15 Dec 2015 15:37:49 +0200
Subject: [PATCH] CSP: Clean up syntax of simpler model

---
 spec/sync.csp | 36 +++++++++++++++++++++---------------
 1 file changed, 21 insertions(+), 15 deletions(-)

diff --git a/spec/sync.csp b/spec/sync.csp
index 2ddceb1..028935e 100644
--- a/spec/sync.csp
+++ b/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)
-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
+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)) [| diff(productions(save), {save.0, save.1}) |] STOP
+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)
 
-CONNS = [| productions(saved) |] i:CLIENTS @ CONN(i, 0)
-SYSTEM' = DB(0) [|{| save, saved |}|] CONNS
+SERVER_WITH_REPORTS(i, t0) = (SERVER(i, t0) [|{| report_queue |}|] REPORTQUEUE(i))
+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}))
 
 -----------------------------------------