Mercurial > hg > Members > nobuyasu > Spin

annotate 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
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
0
86e67be8bc5f add some files
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
1 // Multiple Process to run alternately
86e67be8bc5f add some files
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
2 // atomic operation
86e67be8bc5f add some files
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
3 // assert
86e67be8bc5f add some files
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
4
86e67be8bc5f add some files
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
5 mtype = { F, S };
86e67be8bc5f add some files
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
6 mtype turn = F;
86e67be8bc5f add some files
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
7 pid who;
86e67be8bc5f add some files
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
8
86e67be8bc5f add some files
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
9 active [2] proctype Producer()
86e67be8bc5f add some files
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
10 {
86e67be8bc5f add some files
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
11 do
86e67be8bc5f add some files
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
12 :: atomic{ (turn == F ) -> who = _pid };
86e67be8bc5f add some files
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
13 printf("Producer-%d\n",_pid);
86e67be8bc5f add some files
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
14 assert(who == _pid); turn = S;
86e67be8bc5f add some files
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
15 od
86e67be8bc5f add some files
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
16 }
86e67be8bc5f add some files
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
17
86e67be8bc5f add some files
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
18 active [2] proctype Consumer()
86e67be8bc5f add some files
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
19 {
86e67be8bc5f add some files
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
20 do
86e67be8bc5f add some files
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
21 :: atomic{ (turn == S) -> who = _pid };
86e67be8bc5f add some files
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
22 printf("Consumer-%d\n",_pid);
86e67be8bc5f add some files
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
23 assert(who == _pid); turn = F;
86e67be8bc5f add some files
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
24 od
86e67be8bc5f add some files
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
25 }
86e67be8bc5f add some files
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
26
86e67be8bc5f add some files
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
27