Mercurial > hg > Members > nobuyasu > Spin

comparison promela/alt4.pml @ 0:86e67be8bc5f draft

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
add some files
author Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
date Fri, 29 Jun 2012 01:14:43 +0900
parents
children
comparison
equal deleted inserted replaced
-1:000000000000 0:86e67be8bc5f
1 // Multiple Process to run alternately
2 // atomic operation
3 // assert
4
5 mtype = { F, S };
6 mtype turn = F;
7 pid who;
8
9 active [2] proctype Producer()
10 {
11 do
12 :: atomic{ (turn == F ) -> who = _pid };
13 printf("Producer-%d\n",_pid);
14 assert(who == _pid); turn = S;
15 od
16 }
17
18 active [2] proctype Consumer()
19 {
20 do
21 :: atomic{ (turn == S) -> who = _pid };
22 printf("Consumer-%d\n",_pid);
23 assert(who == _pid); turn = F;
24 od
25 }
26
27