From 9f32a03d0443a010ff98e72d73465e6d18e784a3 Mon Sep 17 00:00:00 2001
From: Nicholas Kariniemi <nicholas.kariniemi@gmail.com>
Date: Sat, 15 Aug 2015 18:18:04 +0300
Subject: [PATCH] Force processes to synchronize on communication

Use parallel operation || instead of the (unsynchronized) interleave
	operation |||.
---
 csp/sync.csp | 17 +++++++----------
 1 file changed, 7 insertions(+), 10 deletions(-)

diff --git a/csp/sync.csp b/csp/sync.csp
index e47230d..6ff5f35 100644
--- a/csp/sync.csp
+++ b/csp/sync.csp
@@ -9,10 +9,10 @@ diff(state1, state2) = (state2 - state1) % S
 empty(patch) = patch == 0
 
 CLIENT(i, state, shadow) = 
-   input.i?new_state
+   input!i?new_state
    -> up!i!diff(shadow, new_state)
    -> CLIENT(i, new_state, shadow)
-[] down.i?patch
+[] down!i?patch
    -> if empty(patch)
      then CLIENT(i, state, state)
      else 
@@ -26,9 +26,9 @@ CLIENT(i, state, shadow) =
          -> CLIENT(i, apply(state, patch), apply(shadow, patch))
 
 SERVER(i, shadow) = 
-   up.i?patch
+   up!i?patch
    -> save!i!patch
-   -> saved.i?new_state
+   -> saved!i?new_state
    -> down!i!diff(apply(shadow, patch), new_state)
    -> SERVER(i, apply(shadow, patch))
 [] saved?j?new_state
@@ -38,11 +38,8 @@ SERVER(i, shadow) =
 
 DB(state) = save?i?patch -> saved!i!apply(state, patch) -> DB(apply(state, patch))
 
-state = 0
-SYSTEM = CLIENT(0, state, state)
-  ||| CLIENT(1, state, state)
-  ||| SERVER(0, state)
-  ||| SERVER(1, state) 
-  ||| DB(state)
+CONN(i, init) = (CLIENT(i, init, init) [|{| up.i, down.i |}|] SERVER(i, init)) [|{| save, saved |}|] DB(init)
+
+SYSTEM = CONN(0,0) ||| CONN(1,0)
 
 assert SYSTEM :[deadlock free [F]]
\ No newline at end of file