Mercurial > hg > Members > nobuyasu > Spin
changeset 1:ac6c53a316ad draft
add alt5,6,7
author | Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp> |
---|---|
date | Fri, 29 Jun 2012 06:22:37 +0900 |
parents | 86e67be8bc5f |
children | a2dac3fa7383 |
files | promela/alt5.pml promela/alt6.pml promela/alt7.pml |
diffstat | 3 files changed, 98 insertions(+), 0 deletions(-) [+] |
line wrap: on
line diff
--- /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 +} +