Mercurial > hg > Members > nobuyasu > Spin

changeset 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 ac6c53a316ad
files Samples/App.F.datalink.h Samples/App.F.defines.h Samples/App.F.flow_cl.h Samples/App.F.fserver.h Samples/App.F.pftp.pml Samples/App.F.present.h Samples/App.F.session.h Samples/App.F.user.h Samples/README.txt Samples/p101.pml Samples/p102.pml Samples/p104.1.pml Samples/p104.2.pml Samples/p105.1.pml Samples/p105.2.pml Samples/p107.pml Samples/p108.pml Samples/p116.pml Samples/p117.pml Samples/p123.pml Samples/p248.pml Samples/p312.pml Samples/p319.pml Samples/p320.pml Samples/p325.test.h Samples/p327.upper.h Samples/p329.pml Samples/p330.pml Samples/p337.defines2.h Samples/p337.fserver.h Samples/p337.pftp.ses.pml Samples/p337.session.h Samples/p337.user.h Samples/p342.pftp.ses1.h Samples/p343.claim.h Samples/p347.pftp.ses5.pml Samples/p347.pres.sim.h Samples/p347.session.prog.h Samples/p94.pml Samples/p95.1.pml Samples/p95.2.pml Samples/p96.1.pml Samples/p96.2.pml Samples/p97.1.pml Samples/p97.2.pml Samples/p99.pml promela/alt1.pml promela/alt2.pml promela/alt3.pml promela/alt4.pml
diffstat 50 files changed, 1737 insertions(+), 0 deletions(-) [+]
line wrap: on
line diff
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Samples/App.F.datalink.h	Fri Jun 29 01:14:43 2012 +0900
@@ -0,0 +1,20 @@
+/*
+ * Datalink Layer Validation Model
+ */
+
+proctype data_link()
+{	byte type, seq;
+
+end:    do
+	:: flow_to_dll[0]?type,seq ->
+		if
+		:: dll_to_flow[1]!type,seq
+		:: skip	/* lose message */
+		fi
+	:: flow_to_dll[1]?type,seq ->
+		if
+		:: dll_to_flow[0]!type,seq
+		:: skip	/* lose message */
+		fi
+	od
+}
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Samples/App.F.defines.h	Fri Jun 29 01:14:43 2012 +0900
@@ -0,0 +1,25 @@
+/*
+ * Global Definitions
+ */
+
+#define LOSS		0	/* message loss   */
+#define DUPS		0	/* duplicate msgs */
+#define QSZ		2	/* queue size     */
+
+mtype = {
+	red, white, blue,
+	abort, accept, ack, sync_ack, close, connect,
+	create, data, eof, open, reject, sync, transfer,
+	FATAL, NON_FATAL, COMPLETE
+	}
+
+chan use_to_pres[2] = [QSZ] of { byte };
+chan pres_to_use[2] = [QSZ] of { byte };
+chan pres_to_ses[2] = [QSZ] of { byte };
+chan ses_to_pres[2] = [QSZ] of { byte, byte };
+chan ses_to_flow[2] = [QSZ] of { byte, byte };
+chan flow_to_ses[2] = [QSZ] of { byte, byte };
+chan dll_to_flow[2] = [QSZ] of { byte, byte };
+chan flow_to_dll[2] = [QSZ] of { byte, byte };
+chan ses_to_fsrv[2] = [0] of { byte };
+chan fsrv_to_ses[2] = [0] of { byte };
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Samples/App.F.flow_cl.h	Fri Jun 29 01:14:43 2012 +0900
@@ -0,0 +1,114 @@
+/*
+ * Flow Control Layer Validation Model
+ */
+
+#define true	1
+#define false	0
+
+#define M	4	/* range sequence numbers   */
+#define W	2	/* window size: M/2         */
+
+proctype fc(bit n)
+{	bool	busy[M];	/* outstanding messages    */
+	byte	q;		/* seq# oldest unacked msg */
+	byte	m;		/* seq# last msg received  */
+	byte	s;		/* seq# next msg to send   */
+	byte	window;		/* nr of outstanding msgs  */
+	byte	type;		/* msg type                */
+	bit	received[M];	/* receiver housekeeping   */
+	bit	x;		/* scratch variable        */
+	byte	p;		/* seq# of last msg acked  */
+	byte	I_buf[M], O_buf[M];	/* message buffers */
+
+	/* sender part */
+end:	do
+	:: atomic {
+	   (window < W	&& len(ses_to_flow[n]) >  0
+			&& len(flow_to_dll[n]) < QSZ) ->
+			ses_to_flow[n]?type,x;
+			window = window + 1;
+			busy[s] = true;
+			O_buf[s] = type;
+			flow_to_dll[n]!type,s;
+			if
+			:: (type != sync) ->
+				s = (s+1)%M
+			:: (type == sync) ->
+				window = 0;
+				s = M;
+				do
+				:: (s > 0) ->
+					s = s-1;
+					busy[s] = false
+				:: (s == 0) ->
+					break
+				od
+			fi
+		}
+	:: atomic {
+		(window > 0 && busy[q] == false) ->
+		window = window - 1;
+		q = (q+1)%M
+	   }
+#if DUPS
+	:: atomic {
+		(len(flow_to_dll[n]) < QSZ
+		 && window > 0 && busy[q] == true) ->
+		flow_to_dll[n]!	O_buf[q],q
+	   }
+#endif
+	:: atomic {
+		(timeout && len(flow_to_dll[n]) < QSZ
+		 && window > 0 && busy[q] == true) ->
+		flow_to_dll[n]!	O_buf[q],q
+	   }
+
+	/* receiver part */
+#if LOSS
+	:: dll_to_flow[n]?type,m /* lose any message */
+#endif
+	:: dll_to_flow[n]?type,m ->
+		if
+		:: atomic {
+			(type == ack) ->
+			busy[m] = false
+		   }
+		:: atomic {
+			(type == sync) ->
+			flow_to_dll[n]!sync_ack,m;
+			m = 0;
+			do
+			:: (m < M) ->
+				received[m] = 0;
+				m = m+1
+			:: (m == M) ->
+				break
+			od
+		   }
+		:: (type == sync_ack) ->
+			flow_to_ses[n]!sync_ack,m
+		:: (type != ack && type != sync && type != sync_ack)->
+			if
+			:: atomic {
+				(received[m] == true) ->
+					x = ((0<p-m   && p-m<=W)
+					||   (0<p-m+M && p-m+M<=W)) };
+					if
+					:: (x) -> flow_to_dll[n]!ack,m
+					:: (!x)	/* else skip */
+					fi
+			:: atomic {
+				(received[m] == false) ->
+					I_buf[m] = type;
+					received[m] = true;
+					received[(m-W+M)%M] = false
+		  	 }
+			fi
+		fi
+	:: (received[p] == true && len(flow_to_ses[n])<QSZ
+				&& len(flow_to_dll[n])<QSZ) ->
+		flow_to_ses[n]!I_buf[p],0;
+		flow_to_dll[n]!ack,p;
+		p = (p+1)%M
+	od
+}
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Samples/App.F.fserver.h	Fri Jun 29 01:14:43 2012 +0900
@@ -0,0 +1,29 @@
+/*
+ * File Server Validation Model
+ */
+
+proctype fserver(bit n)
+{
+end:	do
+	:: ses_to_fsrv[n]?create ->	/* incoming */
+		if
+		:: fsrv_to_ses[n]!reject
+		:: fsrv_to_ses[n]!accept ->
+			do
+			:: ses_to_fsrv[n]?data
+			:: ses_to_fsrv[n]?eof -> break
+			:: ses_to_fsrv[n]?close -> break
+			od
+		fi
+	:: ses_to_fsrv[n]?open ->		/* outgoing */
+		if
+		:: fsrv_to_ses[n]!reject
+		:: fsrv_to_ses[n]!accept ->
+			do
+			:: fsrv_to_ses[n]!data -> progress: skip
+			:: ses_to_fsrv[n]?close -> break
+			:: fsrv_to_ses[n]!eof -> break
+			od
+		fi
+	od
+}
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Samples/App.F.pftp.pml	Fri Jun 29 01:14:43 2012 +0900
@@ -0,0 +1,22 @@
+/*
+ * PROMELA Validation Model - startup script
+ */
+
+#include "App.F.defines.h"
+#include "App.F.user.h"
+#include "App.F.present.h"
+#include "App.F.session.h"
+#include "App.F.fserver.h"
+#include "App.F.flow_cl.h"
+#include "App.F.datalink.h"
+
+init
+{	atomic {
+	  run userprc(0); run userprc(1);
+	  run present(0); run present(1);
+	  run session(0); run session(1);
+	  run fserver(0); run fserver(1);
+	  run fc(0);      run fc(1);
+	  run data_link()
+	}
+}
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Samples/App.F.present.h	Fri Jun 29 01:14:43 2012 +0900
@@ -0,0 +1,44 @@
+/*
+ * Presentation Layer Validation Model
+ */
+
+proctype present(bit n)
+{	byte status, uabort;
+
+endIDLE:
+	do
+	:: use_to_pres[n]?transfer ->
+		uabort = 0;
+		break
+	:: use_to_pres[n]?abort ->
+		skip
+	od;
+
+TRANSFER:
+	pres_to_ses[n]!transfer;
+	do
+	:: use_to_pres[n]?abort ->
+		if
+		:: (!uabort) ->
+			uabort = 1;
+			pres_to_ses[n]!abort
+		:: (uabort) ->
+			assert(1+1!=2)
+		fi
+	:: ses_to_pres[n]?accept,0 ->
+		goto DONE
+	:: ses_to_pres[n]?reject(status) ->
+		if
+		:: (status == FATAL || uabort) ->
+			goto FAIL
+		:: (status == NON_FATAL && !uabort) ->
+progress:		goto TRANSFER
+		fi
+	od;
+DONE:
+	pres_to_use[n]!accept;
+	goto endIDLE;
+FAIL:
+	pres_to_use[n]!reject;
+	goto endIDLE
+}
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Samples/App.F.session.h	Fri Jun 29 01:14:43 2012 +0900
@@ -0,0 +1,128 @@
+/*
+ * Session Layer Validation Model
+ */
+
+proctype session(bit n)
+{	bit toggle;
+	byte type, status;
+
+endIDLE:
+	do
+	:: pres_to_ses[n]?type ->
+		if
+		:: (type == transfer) ->
+			goto DATA_OUT
+		:: (type != transfer)	/* ignore */
+		fi
+	:: flow_to_ses[n]?type,0 ->
+		if
+		:: (type == connect) ->
+			goto DATA_IN
+		:: (type != connect)	/* ignore */
+		fi
+	od;
+
+DATA_IN:		/* 1. prepare local file fsrver */
+	ses_to_fsrv[n]!create;
+	do
+	:: fsrv_to_ses[n]?reject ->
+		ses_to_flow[n]!reject,0;
+		goto endIDLE
+	:: fsrv_to_ses[n]?accept ->
+		ses_to_flow[n]!accept,0;
+		break
+	od;
+			/* 2. Receive the data, upto eof */
+	do
+	:: flow_to_ses[n]?data,0 ->
+		ses_to_fsrv[n]!data
+	:: flow_to_ses[n]?eof,0 ->
+		ses_to_fsrv[n]!eof;
+		break
+	:: pres_to_ses[n]?transfer ->
+		ses_to_pres[n]!reject(NON_FATAL)
+	:: flow_to_ses[n]?close,0 ->	/* remote user aborted */
+		ses_to_fsrv[n]!close;
+		break
+	:: timeout ->		/* got disconnected */
+		ses_to_fsrv[n]!close;
+		goto endIDLE
+	od;
+			/* 3. Close the connection */
+	ses_to_flow[n]!close,0;
+	goto endIDLE;
+
+DATA_OUT:		/* 1. prepare local file fsrver */
+	ses_to_fsrv[n]!open;
+	if
+	:: fsrv_to_ses[n]?reject ->
+		ses_to_pres[n]!reject(FATAL);
+		goto endIDLE
+	:: fsrv_to_ses[n]?accept ->
+		skip
+	fi;
+			/* 2. initialize flow control */
+	ses_to_flow[n]!sync,toggle;
+	do
+	:: atomic {
+		flow_to_ses[n]?sync_ack,type ->
+		if
+		:: (type != toggle)
+		:: (type == toggle) -> break
+		fi
+	   }
+	:: timeout ->
+		ses_to_fsrv[n]!close;
+		ses_to_pres[n]!reject(FATAL);
+		goto endIDLE
+	od;
+	toggle = 1 - toggle;
+			/* 3. prepare remote file fsrver */
+	ses_to_flow[n]!connect,0;
+	if
+	:: flow_to_ses[n]?reject,0 ->
+		ses_to_fsrv[n]!close;
+		ses_to_pres[n]!reject(FATAL);
+		goto endIDLE
+	:: flow_to_ses[n]?connect,0 ->
+		ses_to_fsrv[n]!close;
+		ses_to_pres[n]!reject(NON_FATAL);
+		goto endIDLE
+	:: flow_to_ses[n]?accept,0 ->
+		skip
+	:: timeout ->
+		ses_to_fsrv[n]!close;
+		ses_to_pres[n]!reject(FATAL);
+		goto endIDLE
+	fi;
+			/* 4. Transmit the data, upto eof */
+	do
+	:: fsrv_to_ses[n]?data ->
+		ses_to_flow[n]!data,0
+	:: fsrv_to_ses[n]?eof ->
+		ses_to_flow[n]!eof,0;
+		status = COMPLETE;
+		break
+	:: pres_to_ses[n]?abort ->	/* local user aborted */
+		ses_to_fsrv[n]!close;
+		ses_to_flow[n]!close,0;
+		status = FATAL;
+		break
+	od;
+			/* 5. Close the connection */
+	do
+	:: pres_to_ses[n]?abort 	/* ignore */
+	:: flow_to_ses[n]?close,0 ->
+		if
+		:: (status == COMPLETE) ->
+			ses_to_pres[n]!accept,0
+		:: (status != COMPLETE) ->
+			ses_to_pres[n]!reject(status)
+		fi;
+		break
+	:: timeout ->
+		ses_to_pres[n]!reject(FATAL);
+		break
+	od;
+	goto endIDLE
+}
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Samples/App.F.user.h	Fri Jun 29 01:14:43 2012 +0900
@@ -0,0 +1,20 @@
+/*
+ * User Layer Validation Model
+ */
+
+proctype userprc(bit n)
+{
+	use_to_pres[n]!transfer;
+	if
+	:: pres_to_use[n]?accept -> goto Done
+	:: pres_to_use[n]?reject -> goto Done
+	:: use_to_pres[n]!abort  -> goto Aborted
+	fi;
+Aborted:
+	if
+	:: pres_to_use[n]?accept -> goto Done
+	:: pres_to_use[n]?reject -> goto Done
+	fi;
+Done:
+	skip
+}
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Samples/README.txt	Fri Jun 29 01:14:43 2012 +0900
@@ -0,0 +1,105 @@
+Contents
+--------
+The files in this set contain the text of examples
+used in the 1991 Design and Validation of Computer
+Protocols book.  The name of each file corresponds to the
+page number in the book where the example appears in its
+most useful version.  The overview below gives a short
+descriptive phrase for each file.
+
+Description       Page Nr = Filename prefix
+-----------       -------------------------
+hello world       p95.1
+tiny examples     p94 p95.2 p96.1 p97.1 p97.2 p101 p102 p104.1
+useful demos      p99 p104.2 p105.2 p116 p248
+mutual exclusion  p96.2 p105.1 p117 p320
+Lynch's protocol  p107 p312
+alternatin bit    p123
+chappe's protocol p319
+
+We have renamed the main promela files with the standard file
+extension .pml, and gave all promela files that are not meant to be
+used standalone, but only as include files, the extension .h.
+This gives 28 files with extension .pml, and 17 more with extensions .h.
+We've also renamed variables named 'in' in the original version of
+each file with 'inp' or 'cnt', to avoid the name-clash with what is
+today a keyword, starting with Spin version 6.0.
+Other minor chances include moving channel declarations to the start
+of a proctype declaration, to satisfy new syntax rules, etc.
+
+Large runs
+----------
+ackerman's fct    p108	# read info at start of the file
+
+Pftp Protocol
+-------------
+upper tester      p325.test	# not runnable
+flow control l.   p329 p330
+session layer     p337.pftp.ses p342.pftp.ses1 p347.pftp.ses5
+all pftp          App.F.pftp - plus 8 include files
+
+See also the single file version of pftp in: Test/pftp.pml
+
+General
+-------
+Use these examples for inspiration, and to get 
+acquainted with the language and the Spin software.
+
+All examples - except p123.pml - can be used with both version
+1 and version 2 of SPIN. (p123.pml was modifed for version 2.0
+to use the new syntax for remote referencing).
+
+If you repeat the runs that are listed in the book for
+these examples, you should not expect to get the same
+numbers in the result - given the algorithmic improvements 
+that have been made since book version of Spin Version 1.0.
+Generally, the numbers of states, memory, and runtime should
+all be lower (sometimes considerably so) than what the first
+book reported.
+
+For instance, for p329.pml, the book (Spin V1.0) says
+on pg. 332, using a BITSTATE run, that there are:
+	90845 + 317134 + 182425 states (stored + linked + matched)
+Spin V6.0 (December 2010) reports lower numbers:
+	56713 +  35321 +  76958 states (stored + atomic + matched)
+
+If you repeat a BITSTATE run, of course, by the nature of the
+machine dependent effect of hashing, you may get different
+coverage and hash-factors for larger runs.  The implementation
+of the hash functions has also been changed to improve their
+performance and quality, so the numbers you see will likely differ.
+
+The last set of files (prefixed App.F) is included for completeness.
+As explained in the book: don't expect to be able to do an
+exhaustive verification for this specification as listed.
+In chapter 14 it is illustrated how the spec can be broken up
+into smaller portions that are more easily verified.
+
+Some Small Experiments
+-----------------------
+Try:
+	spin p95.1.pml     # small simulation run
+
+	spin -s p108.pml   # a bigger simulation run, track send stmnts
+	spin -c p108.pml   # same with different output format
+
+	spin -a p312.pml   # lynch's protocol - generate verifier
+	cc -o pan pan.c    # compile it for exhaustive verification
+	./pan              # prove correctness of assertions etc.
+	spin -t -r -s p312.pml # display the error trace
+
+you can edit p312.pml to change all three channel declarations in init
+to look like:	``chan AtoB = [1] of { mtype byte }''
+and repeat the last four steps for a more legible error trace.
+
+	spin -a p123.pml   # alternating bit protocol - generate verifier
+	cc -o pan pan.c    # compile it for exhaustive verification
+	pan -a             # check violations of the never claim
+	spin -t -r -s p123.pml # display the error trace
+
+for an alternative view of these runs try the new graphical
+interface ispin (the successor to xspin), and repeat the experiments.
+
+============================================
+Updated for Spin Version 6, December 3, 2010
+
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Samples/p101.pml	Fri Jun 29 01:14:43 2012 +0900
@@ -0,0 +1,17 @@
+#define msgtype 33
+
+chan name = [0] of { byte, byte };
+
+/* byte name; 	typo  - this line shouldn't have been here */
+
+proctype A()
+{	name!msgtype(124);
+	name!msgtype(121)
+}
+proctype B()
+{	byte state;
+	name?msgtype(state)
+}
+init
+{	atomic { run A(); run B() }
+}
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Samples/p102.pml	Fri Jun 29 01:14:43 2012 +0900
@@ -0,0 +1,14 @@
+#define a 1
+#define b 2
+
+chan ch = [1] of { byte };
+
+proctype A() { ch!a }
+proctype B() { ch!b }
+proctype C()
+{	if
+	:: ch?a
+	:: ch?b
+	fi
+}
+init { atomic { run A(); run B(); run C() } }
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Samples/p104.1.pml	Fri Jun 29 01:14:43 2012 +0900
@@ -0,0 +1,19 @@
+#define N    128
+#define size  16
+
+chan inp   = [size] of { short };
+chan large = [size] of { short };
+chan small = [size] of { short };
+
+proctype split()
+{	short cargo;
+
+	do
+	:: inp?cargo ->
+		if
+		:: (cargo >= N) -> large!cargo
+		:: (cargo <  N) -> small!cargo
+		fi
+	od
+}
+init {	run split() }
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Samples/p104.2.pml	Fri Jun 29 01:14:43 2012 +0900
@@ -0,0 +1,34 @@
+#define N    128
+#define size  16
+
+chan inp   = [size] of { short };
+chan large = [size] of { short };
+chan small = [size] of { short };
+
+proctype split()
+{	short cargo;
+
+	do
+	:: inp?cargo ->
+		if
+		:: (cargo >= N) -> large!cargo
+		:: (cargo <  N) -> small!cargo
+		fi
+	od
+}
+proctype merge()
+{	short cargo;
+
+	do
+	::	if
+		:: large?cargo
+		:: small?cargo
+		fi;
+		inp!cargo
+	od
+}
+init
+{	inp!345; inp!12; inp!6777; inp!32; inp!0;
+	run split(); run merge()
+}
+
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Samples/p105.1.pml	Fri Jun 29 01:14:43 2012 +0900
@@ -0,0 +1,22 @@
+#define p	0
+#define v	1
+
+chan sema = [0] of { bit };
+
+proctype dijkstra()
+{	do
+	:: sema!p -> sema?v
+	od	
+}
+proctype user()
+{	sema?p;
+	/* critical section */
+	sema!v
+	/* non-critical section */
+}
+init
+{	atomic {
+		run dijkstra();
+		run user(); run user(); run user()
+	}
+}
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Samples/p105.2.pml	Fri Jun 29 01:14:43 2012 +0900
@@ -0,0 +1,20 @@
+proctype fact(int n; chan p)
+{	int result;
+	chan child = [1] of { int };
+
+	if
+	:: (n <= 1) -> p!1
+	:: (n >= 2) ->
+		run fact(n-1, child);
+		child?result;
+		p!n*result
+	fi
+}
+init
+{	int result;
+	chan child = [1] of { int };
+
+	run fact(7, child);
+	child?result;
+	printf("result: %d\n", result)
+}
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Samples/p107.pml	Fri Jun 29 01:14:43 2012 +0900
@@ -0,0 +1,26 @@
+mtype = { ack, nak, err, next, accept }
+
+proctype transfer(chan inp, out, chin, chout)
+{	byte o, i;
+
+	inp?next(o);
+	do
+	:: chin?nak(i) -> out!accept(i); chout!ack(o)
+	:: chin?ack(i) -> out!accept(i); inp?next(o); chout!ack(o)
+	:: chin?err(i) -> chout!nak(o)
+	od
+}
+init
+{	chan AtoB = [1] of { byte, byte };
+	chan BtoA = [1] of { byte, byte };
+	chan Ain  = [2] of { byte, byte };
+	chan Bin  = [2] of { byte, byte };
+	chan Aout = [2] of { byte, byte };
+	chan Bout = [2] of { byte, byte };
+
+	atomic {
+		run transfer(Ain, Aout, AtoB, BtoA);
+		run transfer(Bin, Bout, BtoA, AtoB)
+	};
+	AtoB!err(0)
+}
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Samples/p108.pml	Fri Jun 29 01:14:43 2012 +0900
@@ -0,0 +1,57 @@
+/***** Ackermann's function *****/
+
+/*	a good example where a simulation run is the
+	better choice - and verification is overkill.
+
+	1. simulation
+		-> straight simulation (spin p108) takes
+		-> approx. 6.4 sec on an SGI R3000
+		-> prints the answer: ack(3,3) = 61
+		-> after creating 2433 processes
+
+	note: all process invocations can, at least in one
+	feasible execution scenario, overlap - if each
+	process chooses to hang around indefinitely in
+	its dying state, at the closing curly brace.
+	this means that the maximum state vector `could' grow
+	to hold all 2433 processes or about 2433*12 bytes of data.
+	the assert(0) at the end makes sure though that the run
+	stops the first time we complete an execution sequence
+	that computes the answer, so the following suffices:
+
+	2. verification
+		-> spin -a p108
+		-> cc -DVECTORSZ=2048 -o pan pan.c
+		-> pan -m15000
+		-> which completes in about 5 sec
+ */
+
+proctype ack(short a, b; chan ch1)
+{	chan ch2 = [1] of { short };
+	short ans;
+
+	if
+	:: (a == 0) ->
+		ans = b+1
+	:: (a != 0) ->
+		if
+		:: (b == 0) ->
+			run ack(a-1, 1, ch2)
+		:: (b != 0) ->
+			run ack(a, b-1, ch2);
+			ch2?ans;
+			run ack(a-1, ans, ch2)
+		fi;
+		ch2?ans
+	fi;
+	ch1!ans
+}
+init
+{	chan ch = [1] of { short };
+	short ans;
+
+	run ack(3, 3, ch);
+	ch?ans;
+	printf("ack(3,3) = %d\n", ans);
+	assert(0)	/* a forced stop, (Chapter 6) */
+}
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Samples/p116.pml	Fri Jun 29 01:14:43 2012 +0900
@@ -0,0 +1,11 @@
+byte state = 1;
+
+proctype A()
+{	(state == 1) -> state = state + 1;
+	assert(state == 2)
+}
+proctype B()
+{	(state == 1) -> state = state - 1;
+	assert(state == 0)
+}
+init { run A(); run B() }
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Samples/p117.pml	Fri Jun 29 01:14:43 2012 +0900
@@ -0,0 +1,27 @@
+#define p	0
+#define v	1
+
+chan sema = [0] of { bit };	/* typo in original `=' was missing */
+
+proctype dijkstra()
+{	do
+	:: sema!p -> sema?v
+	od	
+}
+byte count;
+
+proctype user()
+{	sema?p;
+	count = count+1;
+	skip;	/* critical section */
+	count = count-1;
+	sema!v;
+	skip	/* non-critical section */
+}
+proctype monitor() { assert(count == 0 || count == 1) }
+init
+{	atomic {
+		run dijkstra(); run monitor();
+		run user(); run user(); run user()
+	}
+}
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Samples/p123.pml	Fri Jun 29 01:14:43 2012 +0900
@@ -0,0 +1,66 @@
+/* alternating bit - version with message loss */
+
+#define MAX	3
+
+mtype = { msg0, msg1, ack0, ack1 };
+
+chan	sender  =[1] of { byte };
+chan	receiver=[1] of { byte };
+
+proctype Sender()
+{	byte any;
+again:
+	do
+	:: receiver!msg1;
+		if
+		:: sender?ack1 -> break
+		:: sender?any /* lost */
+		:: timeout    /* retransmit */
+		fi
+	od;
+	do
+	:: receiver!msg0;
+		if
+		:: sender?ack0 -> break
+		:: sender?any /* lost */
+		:: timeout    /* retransmit */
+		fi
+	od;
+	goto again
+}
+
+proctype Receiver()
+{	byte any;
+again:
+	do
+	:: receiver?msg1 -> sender!ack1; break
+	:: receiver?msg0 -> sender!ack0
+	:: receiver?any /* lost */
+	od;
+P0:
+	do
+	:: receiver?msg0 -> sender!ack0; break
+	:: receiver?msg1 -> sender!ack1
+	:: receiver?any /* lost */
+	od;
+P1:
+	goto again
+}
+
+init { atomic { run Sender(); run Receiver() } }
+
+never {
+	do
+	:: skip	/* allow any time delay */
+	:: receiver?[msg0] -> goto accept0
+	:: receiver?[msg1] -> goto accept1
+	od;
+accept0:
+	do
+	:: !Receiver[2]@P0	/* n.b. new syntax of remote reference */
+	od;
+accept1:
+	do
+	:: !Receiver[2]@P1
+	od
+}
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Samples/p248.pml	Fri Jun 29 01:14:43 2012 +0900
@@ -0,0 +1,20 @@
+proctype fact(int n; chan p)
+{	int result;
+	chan child = [1] of { int };
+
+	if
+	:: (n <= 1) -> p!1
+	:: (n >= 2) ->
+		run fact(n-1, child);
+		child?result;
+		p!n*result
+	fi
+}
+init
+{	int result;
+	chan child = [1] of { int };
+
+	run fact(12, child);
+	child?result;
+	printf("result: %d\n", result)
+}
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Samples/p312.pml	Fri Jun 29 01:14:43 2012 +0900
@@ -0,0 +1,47 @@
+#define MIN	9	/* first data message to send */
+#define MAX	12	/* last  data message to send */
+#define FILL	99	/* filler message */
+
+mtype = { ack, nak, err }
+
+proctype transfer(chan chin, chout)
+{	byte o, i, last_i=MIN;
+
+	o = MIN+1;
+	do
+	:: chin?nak(i) ->
+		assert(i == last_i+1);
+		chout!ack(o)
+	:: chin?ack(i) ->
+		if
+		:: (o <  MAX) -> o = o+1	/* next */
+		:: (o >= MAX) -> o = FILL	/* done */
+		fi;
+		chout!ack(o)
+	:: chin?err(i) ->
+		chout!nak(o)
+	od
+}
+
+proctype channel(chan inp, out)
+{	byte md, mt;
+	do
+	:: inp?mt,md ->
+		if
+		:: out!mt,md
+		:: out!err,0
+		fi
+	od
+}
+
+init
+{	chan AtoB = [1] of { byte, byte };
+	chan BtoC = [1] of { byte, byte };
+	chan CtoA = [1] of { byte, byte };
+	atomic {
+		run transfer(AtoB, BtoC);
+		run channel(BtoC, CtoA);
+		run transfer(CtoA, AtoB)
+	};
+	AtoB!err,0	/* start */
+}
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Samples/p319.pml	Fri Jun 29 01:14:43 2012 +0900
@@ -0,0 +1,44 @@
+#define true	1
+#define false	0
+
+bool busy[3];
+
+chan   up[3] = [1] of { byte };
+chan down[3] = [1] of { byte };
+
+mtype = { start, attention, data, stop }
+
+proctype station(byte id; chan inp, out)
+{	do
+	:: inp?start ->
+		atomic { !busy[id] -> busy[id] = true };
+		out!attention;
+		do
+		:: inp?data -> out!data
+		:: inp?stop -> break
+		od;
+		out!stop;
+		busy[id] = false
+	:: atomic { !busy[id] -> busy[id] = true };
+		out!start;
+		inp?attention;
+		do
+		:: out!data -> inp?data
+		:: out!stop -> break
+		od;
+		inp?stop;
+		busy[id] = false
+	od
+}
+
+init {
+	atomic {
+		run station(0, up[2], down[2]);
+		run station(1, up[0], down[0]);
+		run station(2, up[1], down[1]);
+
+		run station(0, down[0], up[0]);
+		run station(1, down[1], up[1]);
+		run station(2, down[2], up[2])
+	}
+}
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Samples/p320.pml	Fri Jun 29 01:14:43 2012 +0900
@@ -0,0 +1,31 @@
+#define true	1
+#define false	0
+#define Aturn	false
+#define Bturn	true
+
+bool x, y, t;
+bool ain, bin;
+
+proctype A()
+{	x = true;
+	t = Bturn;
+	(y == false || t == Aturn);
+	ain = true;
+	assert(bin == false);	/* critical section */
+	ain = false;
+	x = false
+}
+
+proctype B()
+{	y = true;
+	t = Aturn;
+	(x == false || t == Bturn);
+	bin = true;
+	assert(ain == false);	/* critical section */
+	bin = false;
+	y = false
+}
+
+init
+{	run A(); run B()
+}
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Samples/p325.test.h	Fri Jun 29 01:14:43 2012 +0900
@@ -0,0 +1,42 @@
+proctype test_sender(bit n)
+{	byte type, toggle;
+
+	ses_to_flow[n]!sync,toggle;
+	do
+	:: flow_to_ses[n]?sync_ack,type ->
+		if
+		:: (type != toggle)
+		:: (type == toggle) -> break
+		fi
+	:: timeout ->
+		ses_to_flow[n]!sync,toggle
+	od;
+	toggle = 1 - toggle;
+
+	do
+	:: ses_to_flow[n]!data,white
+	:: ses_to_flow[n]!data,red -> break
+	od;
+	do
+	:: ses_to_flow[n]!data,white
+	:: ses_to_flow[n]!data,blue -> break
+	od;
+	do
+	:: ses_to_flow[n]!data,white
+	:: break
+	od
+}
+proctype test_receiver(bit n)
+{
+	do
+	:: flow_to_ses[n]?data,white
+	:: flow_to_ses[n]?data,red -> break
+	od;
+	do
+	:: flow_to_ses[n]?data,white
+	:: flow_to_ses[n]?data,blue -> break
+	od;
+end:	do
+	:: flow_to_ses[n]?data,white
+	od
+}
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Samples/p327.upper.h	Fri Jun 29 01:14:43 2012 +0900
@@ -0,0 +1,57 @@
+proctype upper()
+{	byte s_state, r_state;
+	byte type, toggle;
+
+	ses_to_flow[0]!sync,toggle;
+	do
+	:: flow_to_ses[0]?sync_ack,type ->
+		if
+		:: (type != toggle)
+		:: (type == toggle) -> break
+		fi
+	:: timeout ->
+		ses_to_flow[0]!sync,toggle
+	od;
+	toggle = 1 - toggle;
+
+	do
+	/* sender */
+	:: ses_to_flow[0]!white,0
+	:: atomic {
+		(s_state == 0 && len (ses_to_flow[0]) < QSZ) ->
+		ses_to_flow[0]!red,0 ->
+		s_state = 1
+	   }
+	:: atomic {
+		(s_state == 1 && len (ses_to_flow[0]) < QSZ) ->
+		ses_to_flow[0]!blue,0 ->
+		s_state = 2
+	   }
+	/* receiver */
+	:: flow_to_ses[1]?white,0
+	:: atomic {
+		(r_state == 0 && flow_to_ses[1]?[red]) ->
+		flow_to_ses[1]?red,0 ->
+		r_state = 1
+	   }
+	:: atomic {
+		(r_state == 0 && flow_to_ses[1]?[blue]) ->
+		assert(0)
+	   }
+	:: atomic {
+		(r_state == 1 && flow_to_ses[1]?[blue]) ->
+		flow_to_ses[1]?blue,0;
+		break
+	   }
+	:: atomic {
+		(r_state == 1 && flow_to_ses[1]?[red]) ->
+		assert(0)
+	   }
+	od;
+end:
+	do
+	:: flow_to_ses[1]?white,0
+	:: flow_to_ses[1]?red,0 -> assert(0)
+	:: flow_to_ses[1]?blue,0 -> assert(0)
+	od
+}
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Samples/p329.pml	Fri Jun 29 01:14:43 2012 +0900
@@ -0,0 +1,33 @@
+/*
+ * PROMELA Validation Model
+ * FLOW CONTROL LAYER VALIDATION
+ */
+
+#define LOSS		0	/* message loss   */
+#define DUPS		0	/* duplicate msgs */
+#define QSZ		2	/* queue size     */
+
+mtype = {
+	red, white, blue,
+	abort, accept, ack, sync_ack, close, connect,
+	create, data, eof, open, reject, sync, transfer,
+	FATAL, NON_FATAL, COMPLETE
+	}
+
+chan ses_to_flow[2] = [QSZ] of { byte, byte };
+chan flow_to_ses[2] = [QSZ] of { byte, byte };
+chan dll_to_flow[2] = [QSZ] of { byte, byte };
+chan flow_to_dll[2];
+
+#include "App.F.flow_cl.h"
+#include "p327.upper.h"
+
+init
+{
+	atomic {
+	  flow_to_dll[0] = dll_to_flow[1];
+	  flow_to_dll[1] = dll_to_flow[0];
+	  run fc(0); run fc(1);
+	  run upper()
+	}
+}
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Samples/p330.pml	Fri Jun 29 01:14:43 2012 +0900
@@ -0,0 +1,33 @@
+/*
+ * PROMELA Validation Model
+ * FLOW CONTROL LAYER VALIDATION
+ */
+
+#define LOSS		0	/* message loss   */
+#define DUPS		0	/* duplicate msgs */
+#define QSZ		2	/* queue size     */
+
+mtype = {
+	red, white, blue,
+	abort, accept, ack, sync_ack, close, connect,
+	create, data, eof, open, reject, sync, transfer,
+	FATAL, NON_FATAL, COMPLETE
+	}
+
+chan ses_to_flow[2] = [QSZ] of { byte, byte };
+chan flow_to_ses[2] = [QSZ] of { byte, byte };
+chan dll_to_flow[2] = [QSZ] of { byte, byte };
+chan flow_to_dll[2];
+
+#include "App.F.flow_cl.h"
+#include "p327.upper.h"
+
+init
+{
+	atomic {
+	  flow_to_dll[0] = dll_to_flow[1];
+	  flow_to_dll[1] = dll_to_flow[0];
+	  run fc(0); run fc(1);
+	  run upper()
+	}
+}
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Samples/p337.defines2.h	Fri Jun 29 01:14:43 2012 +0900
@@ -0,0 +1,22 @@
+/*
+ * PROMELA Validation Model
+ * global definitions
+ */
+
+#define QSZ		2	/* queue size     */
+
+mtype = {
+	red, white, blue,
+	abort, accept, ack, sync_ack, close, connect,
+	create, data, eof, open, reject, sync, transfer,
+	FATAL, NON_FATAL, COMPLETE
+	}
+
+chan use_to_pres[2] = [QSZ] of { mtype };
+chan pres_to_use[2] = [QSZ] of { mtype };
+chan pres_to_ses[2] = [QSZ] of { mtype };
+chan ses_to_pres[2] = [QSZ] of { mtype, byte };
+chan ses_to_flow[2] = [QSZ] of { mtype, byte };
+chan ses_to_fsrv[2] = [0] of { mtype };
+chan fsrv_to_ses[2] = [0] of { mtype };
+chan flow_to_ses[2];
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Samples/p337.fserver.h	Fri Jun 29 01:14:43 2012 +0900
@@ -0,0 +1,29 @@
+/*
+ * File Server Validation Model
+ */
+
+proctype fserver(bit n)
+{
+end:	do
+	:: ses_to_fsrv[n]?create ->	/* incoming */
+		if
+		:: fsrv_to_ses[n]!reject
+		:: fsrv_to_ses[n]!accept ->
+			do
+			:: ses_to_fsrv[n]?data
+			:: ses_to_fsrv[n]?eof -> break
+			:: ses_to_fsrv[n]?close -> break
+			od
+		fi
+	:: ses_to_fsrv[n]?open ->		/* outgoing */
+		if
+		:: fsrv_to_ses[n]!reject
+		:: fsrv_to_ses[n]!accept ->
+			do
+			:: fsrv_to_ses[n]!data -> progress: skip
+			:: ses_to_fsrv[n]?close -> break
+			:: fsrv_to_ses[n]!eof -> break
+			od
+		fi
+	od
+}
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Samples/p337.pftp.ses.pml	Fri Jun 29 01:14:43 2012 +0900
@@ -0,0 +1,21 @@
+/*
+ * PROMELA Validation Model
+ * Session Layer
+ */
+
+#include "p337.defines2.h"
+#include "p337.user.h"
+#include "App.F.present.h"
+#include "p337.session.h"
+#include "p337.fserver.h"
+
+init
+{	atomic {
+	  run userprc(0); run userprc(1);
+	  run present(0); run present(1);
+	  run session(0); run session(1);
+	  run fserver(0); run fserver(1);
+	  flow_to_ses[0] = ses_to_flow[1];
+	  flow_to_ses[1] = ses_to_flow[0]
+	}
+}
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Samples/p337.session.h	Fri Jun 29 01:14:43 2012 +0900
@@ -0,0 +1,128 @@
+/*
+ * Session Layer Validation Model
+ */
+
+proctype session(bit n)
+{	bit toggle;
+	byte type, status;
+
+endIDLE:
+	do
+	:: pres_to_ses[n]?type ->
+		if
+		:: (type == transfer) ->
+			goto DATA_OUT
+		:: (type != transfer)	/* ignore */
+		fi
+	:: flow_to_ses[n]?type,0 ->
+		if
+		:: (type == connect) ->
+			goto DATA_IN
+		:: (type != connect)	/* ignore */
+		fi
+	od;
+
+DATA_IN:		/* 1. prepare local file fsrver */
+	ses_to_fsrv[n]!create;
+	do
+	:: fsrv_to_ses[n]?reject ->
+		ses_to_flow[n]!reject,0;
+		goto endIDLE
+	:: fsrv_to_ses[n]?accept ->
+		ses_to_flow[n]!accept,0;
+		break
+	od;
+			/* 2. Receive the data, upto eof */
+	do
+	:: flow_to_ses[n]?data,0 ->
+		ses_to_fsrv[n]!data
+	:: flow_to_ses[n]?eof,0 ->
+		ses_to_fsrv[n]!eof;
+		break
+	:: pres_to_ses[n]?transfer ->
+		ses_to_pres[n]!reject(NON_FATAL)
+	:: flow_to_ses[n]?close,0 ->	/* remote user aborted */
+		ses_to_fsrv[n]!close;
+		break
+	:: timeout ->		/* got disconnected */
+		ses_to_fsrv[n]!close;
+		goto endIDLE
+	od;
+			/* 3. Close the connection */
+	ses_to_flow[n]!close,0;
+	goto endIDLE;
+
+DATA_OUT:		/* 1. prepare local file fsrver */
+	ses_to_fsrv[n]!open;
+	if
+	:: fsrv_to_ses[n]?reject ->
+		ses_to_pres[n]!reject(FATAL);
+		goto endIDLE
+	:: fsrv_to_ses[n]?accept ->
+		skip
+	fi;
+			/* 2. initialize flow control *** disabled
+	ses_to_flow[n]!sync,toggle;
+	do
+	:: atomic {
+		flow_to_ses[n]?sync_ack,type ->
+		if
+		:: (type != toggle)
+		:: (type == toggle) -> break
+		fi
+	   }
+	:: timeout ->
+		ses_to_fsrv[n]!close;
+		ses_to_pres[n]!reject(FATAL);
+		goto endIDLE
+	od;
+	toggle = 1 - toggle;
+			/* 3. prepare remote file fsrver */
+	ses_to_flow[n]!connect,0;
+	if
+	:: flow_to_ses[n]?reject,0 ->
+		ses_to_fsrv[n]!close;
+		ses_to_pres[n]!reject(FATAL);
+		goto endIDLE
+	:: flow_to_ses[n]?connect,0 ->
+		ses_to_fsrv[n]!close;
+		ses_to_pres[n]!reject(NON_FATAL);
+		goto endIDLE
+	:: flow_to_ses[n]?accept,0 ->
+		skip
+	:: timeout ->
+		ses_to_fsrv[n]!close;
+		ses_to_pres[n]!reject(FATAL);
+		goto endIDLE
+	fi;
+			/* 4. Transmit the data, upto eof */
+	do
+	:: fsrv_to_ses[n]?data ->
+		ses_to_flow[n]!data,0
+	:: fsrv_to_ses[n]?eof ->
+		ses_to_flow[n]!eof,0;
+		status = COMPLETE;
+		break
+	:: pres_to_ses[n]?abort ->	/* local user aborted */
+		ses_to_fsrv[n]!close;
+		ses_to_flow[n]!close,0;
+		status = FATAL;
+		break
+	od;
+			/* 5. Close the connection */
+	do
+	:: pres_to_ses[n]?abort 	/* ignore */
+	:: flow_to_ses[n]?close,0 ->
+		if
+		:: (status == COMPLETE) ->
+			ses_to_pres[n]!accept,0
+		:: (status != COMPLETE) ->
+			ses_to_pres[n]!reject(status)
+		fi;
+		break
+	:: timeout ->
+		ses_to_pres[n]!reject(FATAL);
+		break
+	od;
+	goto endIDLE
+}
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Samples/p337.user.h	Fri Jun 29 01:14:43 2012 +0900
@@ -0,0 +1,20 @@
+/*
+ * User Layer Validation Model
+ */
+
+proctype userprc(bit n)
+{
+	use_to_pres[n]!transfer;
+	if
+	:: pres_to_use[n]?accept -> goto Done
+	:: pres_to_use[n]?reject -> goto Done
+	:: use_to_pres[n]!abort  -> goto Aborted
+	fi;
+Aborted:
+	if
+	:: pres_to_use[n]?accept -> goto Done
+	:: pres_to_use[n]?reject -> goto Done
+	fi;
+Done:
+	skip
+}
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Samples/p342.pftp.ses1.h	Fri Jun 29 01:14:43 2012 +0900
@@ -0,0 +1,31 @@
+/*
+ * PROMELA Validation Model
+ * Session Layer
+ */
+
+#include "p337.defines2.h"
+#include "p337.user.h"
+#include "App.F.present.h"
+#include "p337.session.h"
+#include "p337.fserver.h"
+
+init
+{
+	atomic {
+	  run userprc(0); run userprc(1);
+	  run present(0); run present(1);
+	  run session(0); run session(1);
+	  run fserver(0); run fserver(1);
+	  flow_to_ses[0] = ses_to_flow[1];
+	  flow_to_ses[1] = ses_to_flow[0]
+	};
+	atomic {
+		byte any;
+		chan foo = [1] of { byte, byte };
+		ses_to_flow[0] = foo;
+		ses_to_flow[1] = foo
+	};
+end:	do
+	:: foo?any,any
+	od
+}
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Samples/p343.claim.h	Fri Jun 29 01:14:43 2012 +0900
@@ -0,0 +1,21 @@
+never {
+	skip;	/* match first step of init (spin version 2.0) */
+	do
+	:: !pres_to_ses[0]?[transfer]
+	&& !flow_to_ses[0]?[connect]
+	:: pres_to_ses[0]?[transfer] ->
+		goto accept0
+	:: flow_to_ses[0]?[connect] ->
+		goto accept1
+	od;
+accept0:
+	do
+	:: !ses_to_pres[0]?[accept]
+	&& !ses_to_pres[0]?[reject]
+	od;
+accept1:
+	do
+	:: !ses_to_pres[1]?[accept]
+	&& !ses_to_pres[1]?[reject]
+	od
+}
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Samples/p347.pftp.ses5.pml	Fri Jun 29 01:14:43 2012 +0900
@@ -0,0 +1,19 @@
+/*
+ * PROMELA Validation Model
+ * Session Layer
+ */
+
+#include "p337.defines2.h"
+#include "p347.pres.sim.h"
+#include "p347.session.prog.h"
+#include "p337.fserver.h"
+
+init
+{	atomic {
+	  run present(0); run present(1);
+	  run session(0); run session(1);
+	  run fserver(0); run fserver(1);
+	  flow_to_ses[0] = ses_to_flow[1];
+	  flow_to_ses[1] = ses_to_flow[0]
+	}
+}
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Samples/p347.pres.sim.h	Fri Jun 29 01:14:43 2012 +0900
@@ -0,0 +1,23 @@
+/*
+ * PROMELA Validation Model
+ * Presentation & User Layer - combined and reduced
+ */
+
+proctype present(bit n)
+{	byte status;
+progress0:
+	pres_to_ses[n]!transfer ->
+	do
+	:: pres_to_ses[n]!abort;
+progress1:	skip
+	:: ses_to_pres[n]?accept,status ->
+			break
+	:: ses_to_pres[n]?reject,status ->
+		if
+		:: (status == NON_FATAL) ->
+			goto progress0
+		:: (status != NON_FATAL) ->
+			break
+		fi
+	od
+}
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Samples/p347.session.prog.h	Fri Jun 29 01:14:43 2012 +0900
@@ -0,0 +1,128 @@
+/*
+ * Session Layer Validation Model
+ */
+
+proctype session(bit n)
+{	bit toggle;
+	byte type, status;
+
+endIDLE:
+	do
+	:: pres_to_ses[n]?type ->
+		if
+		:: (type == transfer) ->
+			goto progressDATA_OUT
+		:: (type != transfer)	/* ignore */
+		fi
+	:: flow_to_ses[n]?type,0 ->
+		if
+		:: (type == connect) ->
+			goto progressDATA_IN
+		:: (type != connect)	/* ignore */
+		fi
+	od;
+
+progressDATA_IN:		/* 1. prepare local file fsrver */
+	ses_to_fsrv[n]!create;
+	do
+	:: fsrv_to_ses[n]?reject ->
+		ses_to_flow[n]!reject,0;
+		goto endIDLE
+	:: fsrv_to_ses[n]?accept ->
+		ses_to_flow[n]!accept,0;
+		break
+	od;
+			/* 2. Receive the data, upto eof */
+	do
+	:: flow_to_ses[n]?data,0 ->
+progress:	ses_to_fsrv[n]!data
+	:: flow_to_ses[n]?eof,0 ->
+		ses_to_fsrv[n]!eof;
+		break
+	:: pres_to_ses[n]?transfer ->
+		ses_to_pres[n]!reject(NON_FATAL)
+	:: flow_to_ses[n]?close,0 ->	/* remote user aborted */
+		ses_to_fsrv[n]!close;
+		break
+	:: timeout ->		/* got disconnected */
+		ses_to_fsrv[n]!close;
+		goto endIDLE
+	od;
+			/* 3. Close the connection */
+	ses_to_flow[n]!close,0;
+	goto endIDLE;
+
+progressDATA_OUT:		/* 1. prepare local file fsrver */
+	ses_to_fsrv[n]!open;
+	if
+	:: fsrv_to_ses[n]?reject ->
+		ses_to_pres[n]!reject(FATAL);
+		goto endIDLE
+	:: fsrv_to_ses[n]?accept ->
+		skip
+	fi;
+			/* 2. initialize flow control *** disabled
+	ses_to_flow[n]!sync,toggle;
+	do
+	:: atomic {
+		flow_to_ses[n]?sync_ack,type ->
+		if
+		:: (type != toggle)
+		:: (type == toggle) -> break
+		fi
+	   }
+	:: timeout ->
+		ses_to_fsrv[n]!close;
+		ses_to_pres[n]!reject(FATAL);
+		goto endIDLE
+	od;
+	toggle = 1 - toggle;
+			/* 3. prepare remote file fsrver */
+	ses_to_flow[n]!connect,0;
+	if
+	:: flow_to_ses[n]?reject,status ->
+		ses_to_fsrv[n]!close;
+		ses_to_pres[n]!reject(FATAL);
+		goto endIDLE
+	:: flow_to_ses[n]?connect,0 ->
+		ses_to_fsrv[n]!close;
+		ses_to_pres[n]!reject(NON_FATAL);
+		goto endIDLE
+	:: flow_to_ses[n]?accept,0 ->
+		skip
+	:: timeout ->
+		ses_to_fsrv[n]!close;
+		ses_to_pres[n]!reject(FATAL);
+		goto endIDLE
+	fi;
+			/* 4. Transmit the data, upto eof */
+	do
+	:: fsrv_to_ses[n]?data ->
+		ses_to_flow[n]!data,0
+	:: fsrv_to_ses[n]?eof ->
+		ses_to_flow[n]!eof,0;
+		status = COMPLETE;
+		break
+	:: pres_to_ses[n]?abort ->	/* local user aborted */
+		ses_to_fsrv[n]!close;
+		ses_to_flow[n]!close,0;
+		status = FATAL;
+		break
+	od;
+			/* 5. Close the connection */
+	do
+	:: pres_to_ses[n]?abort 	/* ignore */
+	:: flow_to_ses[n]?close,0 ->
+		if
+		:: (status == COMPLETE) ->
+			ses_to_pres[n]!accept,0
+		:: (status != COMPLETE) ->
+			ses_to_pres[n]!reject(status)
+		fi;
+		break
+	:: timeout ->
+		ses_to_pres[n]!reject(FATAL);
+		break
+	od;
+	goto endIDLE
+}
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Samples/p94.pml	Fri Jun 29 01:14:43 2012 +0900
@@ -0,0 +1,8 @@
+byte state = 2;
+
+proctype A() { (state == 1) -> state = 3 }
+
+proctype B() { state = state - 1 }
+
+/* added: */
+init { run A(); run B() }
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Samples/p95.1.pml	Fri Jun 29 01:14:43 2012 +0900
@@ -0,0 +1,1 @@
+init { printf("hello world\n") }
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Samples/p95.2.pml	Fri Jun 29 01:14:43 2012 +0900
@@ -0,0 +1,5 @@
+proctype A(byte state; short set)
+{	(state == 1) -> state = set
+}
+
+init { run A(1, 3) }
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Samples/p96.1.pml	Fri Jun 29 01:14:43 2012 +0900
@@ -0,0 +1,7 @@
+byte state = 1;
+
+proctype A() { (state == 1) -> state = state + 1 }
+
+proctype B() { (state == 1) -> state = state - 1 }
+
+init { run A(); run B() }
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Samples/p96.2.pml	Fri Jun 29 01:14:43 2012 +0900
@@ -0,0 +1,22 @@
+#define true	1
+#define false	0
+#define Aturn	1
+#define Bturn	0
+
+bool x, y, t;
+
+proctype A()
+{	x = true;
+	t = Bturn;
+	(y == false || t == Aturn);
+	/* critical section */
+	x = false
+}
+proctype B()
+{	y = true;
+	t = Aturn;
+	(x == false || t == Bturn);
+	/* critical section */
+	y = false
+}
+init { run A(); run B() }
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Samples/p97.1.pml	Fri Jun 29 01:14:43 2012 +0900
@@ -0,0 +1,4 @@
+byte state = 1;
+proctype A() { atomic { (state == 1) -> state = state + 1 } }
+proctype B() { atomic { (state == 1) -> state = state - 1 } }
+init { run A(); run B() }
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Samples/p97.2.pml	Fri Jun 29 01:14:43 2012 +0900
@@ -0,0 +1,8 @@
+proctype nr(short id, a, b)
+{	int res;
+
+atomic	{	res = (a*a+b)/2*a;
+		printf("result %d: %d\n", id, res)
+	}
+}
+init { run nr(1,1,1); run nr(1,2,2); run nr(1,3,2) }
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Samples/p99.pml	Fri Jun 29 01:14:43 2012 +0900
@@ -0,0 +1,23 @@
+proctype A(chan q1)
+{	chan q2;
+
+	q1?q2;
+	q2!123
+}
+
+proctype B(chan qforb)
+{	int x;
+
+	qforb?x;
+	printf("x = %d\n", x)
+}
+
+init
+{	chan qname[2] = [1] of { chan };
+	chan qforb = [1] of { int };
+
+	run A(qname[0]);
+	run B(qforb);
+
+	qname[0]!qforb
+}
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/promela/alt1.pml	Fri Jun 29 01:14:43 2012 +0900
@@ -0,0 +1,20 @@
+// Process to run alternately
+
+mtype = { F, S};
+mtype turn = F;
+
+active proctype Producer()
+{
+  do
+    :: (turn == F) -> printf("Producer\n"); turn = S;
+  od
+}
+
+active proctype Consumer()
+{
+  do
+    :: (turn == S) -> printf("Consumer\n"); turn = F;
+  od
+}
+
+
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/promela/alt2.pml	Fri Jun 29 01:14:43 2012 +0900
@@ -0,0 +1,20 @@
+// Multiple Process to run alternately
+
+mtype = { F, S};
+mtype turn = F;
+
+active [2] proctype Producer()
+{
+  do
+    :: (turn == F) -> printf("Producer-%d\n",_pid); turn = S;
+  od
+}
+
+active [2] proctype Consumer()
+{
+  do
+    :: (turn == S) -> printf("Consumer-%d\n",_pid); turn = F;
+  od
+}
+
+
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/promela/alt3.pml	Fri Jun 29 01:14:43 2012 +0900
@@ -0,0 +1,23 @@
+// Multiple Process to run alternately
+// atomic operation
+
+mtype = { F, S, N };
+mtype turn = F;
+
+active [2] proctype Producer()
+{
+  do
+    :: atomic{ (turn == F ) -> turn = N  };
+       printf("Producer-%d\n",_pid); turn = S;
+  od
+}
+
+active [2] proctype Consumer()
+{
+  do
+    :: atomic{ (turn == S) -> turn = N };
+       printf("Consumer-%d\n",_pid); turn = F;
+  od
+}
+
+
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/promela/alt4.pml	Fri Jun 29 01:14:43 2012 +0900
@@ -0,0 +1,27 @@
+// Multiple Process to run alternately
+// atomic operation
+// assert 
+
+mtype = { F, S };
+mtype turn = F;
+pid who;
+
+active [2] proctype Producer()
+{
+  do
+    :: atomic{ (turn == F ) -> who = _pid };
+       printf("Producer-%d\n",_pid);
+       assert(who == _pid); turn = S;
+  od
+}
+
+active [2] proctype Consumer()
+{
+  do
+    :: atomic{ (turn == S) -> who = _pid };
+       printf("Consumer-%d\n",_pid);
+       assert(who == _pid); turn = F;
+  od
+}
+
+