Mercurial > hg > Members > nobuyasu > Spin

annotate promela/alt2.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
86e67be8bc5f add some files
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
3 mtype = { F, S};
86e67be8bc5f add some files
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
4 mtype turn = F;
86e67be8bc5f add some files
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
5
86e67be8bc5f add some files
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
6 active [2] proctype Producer()
86e67be8bc5f add some files
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
7 {
86e67be8bc5f add some files
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
8 do
86e67be8bc5f add some files
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
9 :: (turn == F) -> printf("Producer-%d\n",_pid); turn = S;
86e67be8bc5f add some files
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
10 od
86e67be8bc5f add some files
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
11 }
86e67be8bc5f add some files
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
12
86e67be8bc5f add some files
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
13 active [2] proctype Consumer()
86e67be8bc5f add some files
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
14 {
86e67be8bc5f add some files
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
15 do
86e67be8bc5f add some files
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
16 :: (turn == S) -> printf("Consumer-%d\n",_pid); turn = F;
86e67be8bc5f add some files
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
17 od
86e67be8bc5f add some files
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
18 }
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