Readme
------
The files in this collection contain the text of examples
that were used in the 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
-----------             ------------------
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 excl.	=	p96.2 p105.1 p117 p320
Lynch's prot.	=	p107 p312
alternatin bit	=	p123
chappe's prot.	=	p319

Large runs
----------
ackerman's fct	=	p108

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

Other
-----
leader election	=	leader
sorting example	=	sort
snooping cache	=	snoopy
single file pftp =	pftp	

General
-------
Use these examples for inspiration, and to get quickly
acquainted with the language and the Spin software.

 The language has changed somewhat since the book was
 published, so it is possible that some of the examples
 will need to be tweaked a little to work with the latest
 version of Spin.

If you repeat the runs that are listed in the book for
these examples, you should expect to get roughly the same
numbers in the result - although in some cases there may
be small differences that are due to changes in bookkeeping.

For instance, for p329, the book (Spin V1.0) says
on pg. 332 that there are:
	90845 + 317134 + 182425 states stored + linked + matched.
Spin V1.6 reports the numbers for p329 (more accurately) as:
	90840 + 317136 + 182425 states stored + linked + 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 numbers, though,
should be expected to be in the same range as those reported in
the book.

The last set of file (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		# small simulation run

	spin -s p108		# bigger simulation run, track send stmnts

	spin -a p312		# lynch's protocol - generate verifier
	gcc -o pan pan.c		# compile it for exhaustive verification
	./pan			# prove correctness of assertions etc.
	spin -t -r -s p312	# display the error trace

now edit p312 to change all three channel declarations in init
to look like:	``chan AtoB = [1] of { mtype byte }''
and repeat the above four steps.
note the improvement in the backtrace.

	spin -a p123		# alternating bit protocol - generate verifier
	gcc -o pan pan.c		# compile it for exhaustive verification
	./pan -a		# check violations of the never claim
	spin -t -r -s p123	# display the error trace


Questions, feedback: gerard@spinroot.com
