# HG changeset patch
# User Nobuyasu Oshiro  <dimolto@cr.ie.u-ryukyu.ac.jp>
# Date 1340918557 -32400
# Node ID ac6c53a316adbca0d6e5480cedd21501f49379ef
# Parent  86e67be8bc5fc04c962bc57ec17dfb850f0ca0fb
add alt5,6,7

diff -r 86e67be8bc5f -r ac6c53a316ad promela/alt5.pml
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/promela/alt5.pml	Fri Jun 29 06:22:37 2012 +0900
@@ -0,0 +1,30 @@
+// Multiple Process to run alternately
+// atomic operation
+// assert 
+// version 5
+
+mtype = { F, S, N };
+mtype turn = F;
+pid who;
+
+active [2] proctype Producer()
+{
+  do
+    :: atomic{ (turn == F ) -> turn = N; who = _pid };
+       printf("Producer-%d\n",_pid);
+       assert(who == _pid);
+       atomic{ turn = S; who = 0 }
+  od
+}
+
+active [2] proctype Consumer()
+{
+  do
+    :: atomic{ (turn == S) -> turn = N; who = _pid };
+       printf("Consumer-%d\n",_pid);
+       assert(who == _pid);
+       atomic{ turn = F; who = 0; }
+  od
+}
+
+
diff -r 86e67be8bc5f -r ac6c53a316ad promela/alt6.pml
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/promela/alt6.pml	Fri Jun 29 06:22:37 2012 +0900
@@ -0,0 +1,30 @@
+// Multiple Process to run alternately
+// atomic operation
+// assert 
+// version 5
+
+mtype = { F, S, N };
+mtype turn = F;
+pid who;
+
+active [2] proctype Producer()
+{
+  do
+    :: (turn == F ) -> turn = N; who = _pid;
+       printf("Producer-%d\n",_pid);
+       assert(who == _pid);
+       atomic{ turn = S; who = 0 }
+  od
+}
+
+active [2] proctype Consumer()
+{
+  do
+    :: (turn == S) -> turn = N; who = _pid;
+       printf("Consumer-%d\n",_pid);
+       assert(who == _pid);
+       atomic{ turn = F; who = 0; }
+  od
+}
+
+
diff -r 86e67be8bc5f -r ac6c53a316ad promela/alt7.pml
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/promela/alt7.pml	Fri Jun 29 06:22:37 2012 +0900
@@ -0,0 +1,38 @@
+#define NFP 2
+#define NSP 2
+
+mtype = { F, S, N };
+mtype turn = F;
+pid who;
+
+inline request(x,y,z) {
+  atomic{ (x == y) -> x = z; who = _pid;  }
+}
+
+inline check() {
+  assert(who == _pid)
+}
+
+inline release(x, y) {
+  atomic{ x = y; who = 0  }
+}
+
+active [NFP] proctype Producer()
+{
+  do
+    :: request(turn, F, N);
+       printf("Producer-%d\n",_pid); check();
+       release(turn, S);
+  od
+}
+
+
+active [NSP] proctype Consumer()
+{
+  do
+    :: request(turn, S, N);
+       printf("Consumer-%d\n",_pid); check();
+       release(turn, F);
+  od
+}
+