From 20c408e491bd536c4327e5b931a5e4e208b89126 Mon Sep 17 00:00:00 2001
From: Nicholas Kariniemi <nicholas.kariniemi@gmail.com>
Date: Sun, 29 Nov 2015 23:28:48 +0200
Subject: [PATCH] Add two-way sync assertion and simplify down buffer

- Down buffer is no longer a sliding buffer of size one but just
 a buffer of size 1. It cannot be pushed into if it is full.
---
 csp/sync.csp | 22 +++++++++++++++++-----
 1 file changed, 17 insertions(+), 5 deletions(-)

diff --git a/csp/sync.csp b/csp/sync.csp
index 69ff4c2..b0d47f0 100644
--- a/csp/sync.csp
+++ b/csp/sync.csp
@@ -25,10 +25,7 @@ CLIENT'(i, 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)
+DOWNBUF(i) = down!i?client_t?server_t -> bufdown!i!client_t!server_t -> DOWNBUF(i)
 
 SERVER(i, client_t) = 
    up!i?server_t
@@ -95,4 +92,19 @@ 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)
\ No newline at end of file
+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 = input.0 -> input.1 -> STOP
+
+-- Then our specification becomes simple:
+TwoWaySync = input.0 -> input.1 -> ((render.0.2 -> render.1.2 -> STOP) |~|
+                                    (render.1.2 -> render.0.2 -> STOP))
+
+assert TwoWaySync [FD= (SYSTEM [|{| input |}|] AlternateInputs) \diff(Events, {input.0, input.1, render.0.2, render.1.2})
\ No newline at end of file