--- /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
+}
+
+

--- /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
+}
+
+

--- /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
+}
+