From 273676982555089ee0253fe7c564c4f80d90437d Mon Sep 17 00:00:00 2001 From: Nicholas Kariniemi Date: Thu, 13 Aug 2015 21:58:03 +0300 Subject: [PATCH] Basic CSP "sync" - some working CSPM --- csp/sync.csp | 7 +++++++ 1 file changed, 7 insertions(+) create mode 100644 csp/sync.csp diff --git a/csp/sync.csp b/csp/sync.csp new file mode 100644 index 0000000..855cadf --- /dev/null +++ b/csp/sync.csp @@ -0,0 +1,7 @@ +channel input:{0,1,2} + +USER(i) = input!i -> USER((i+1)%3) +CLIENT(i) = input?j -> CLIENT(j) +SYSTEM = USER(0) ||| CLIENT(0) + +assert SYSTEM :[deadlock free [F]] \ No newline at end of file