-- Updated for SPIN Version 4.1.2 ---

Perform tests test0 to test5 in the order listed, and
make sure you get the same results. The next four tests
are to assess the effect of partial order reductions.
In exhaustive mode, they may not all be executable within
the bounds of your system - with reduction turned on,
though, they should all run as specified.
The last test checks the use of execution priorities
during random simulations.
The file called 'pathfinder' illustrates the use of
'provided' clauses (using as inspiration the bug in
the control software of the Mars pathfinder that
spotted an otherwise perfect mission in July 1997).

The wordcount example illustrates slicing (version 3.4).
Some additional test-cases, not explicitly covered here
are included in the four files with the prefix mobile*.

	You can always check valid options of spin
	by typing: spin --

	Similarly, you can check valid options of
	the compiled verifiers by typing: pan --

test 0	check that spin exists, is executable, and is
	the version that you expect

	$ spin -V
	Spin Version 4.1.2 -- 21 February 2004

test 1	check that you can run a simulation

	$ spin hello
		passed first test!
	1 process created

test 2	a basic reachability check (safety)

	$ spin -a loops			# generate c-verifier
	$ cc -DNOREDUCE -o pan pan.c	# no reduction (test)
	$ ./pan				# default run
	hint: this search is more efficient if pan.c is compiled -DSAFETY
	(Spin Version 4.1.2 -- 21 February 2004)

	Full statespace search for:
	        never-claim             - (none specified)
	        assertion violations    +
	        acceptance   cycles     - (not selected)
	        invalid endstates       +
	
	State-vector 16 byte, depth reached 11, errors: 0
	      15 states, stored
	       4 states, matched
	      19 transitions (= stored+matched)
	       0 atomic steps
	hash conflicts: 0 (resolved)
	(max size 2^18 states)
		
	unreached in proctype loop
        	line 12, state 12, "-end-"
        	(1 of 12 states)

	[the precise size for the State-vector in bytes can depend on
	 the quality of your compiler -- it could be slightly smaller or
	 larger, depending on how well the compiler packs the data structure
	 in memory -- the one we used for the tests was Microsoft Visual Studio.
	 in this case, gcc gets the statevector down to 12 byte.]

test 3	cycle detection check (liveness):

	$ ./pan -a		# search for acceptance cycles
	pan: acceptance cycle (at depth 0)
	pan: wrote loops.trail
	(Spin Version 4.1.2 -- 21 February 2004)
	Warning: Search not completed
	
	Full statespace search for:
	        never-claim             - (none specified)
	        assertion violations    +
>	        acceptance   cycles     + (fairness disabled)
	        invalid endstates       +
	
	State-vector 16 byte, depth reached 11, errors: 1
	      12 states, stored (16 visited)
	       2 states, matched
	      17 transitions (= visited+matched)
	       0 atomic steps
	hash conflicts: 0 (resolved)
	(max size 2^18 states)

test 4	guided simulation check (playback the error trail found in test 3)

	$ spin -t -p loops	# guided simulation for the error-cycle
	<<<<<START OF CYCLE>>>>>
	  1:    proc  0 (loop) line   5 "loops" (state 1)       [a = ((a+1)%3)]
	  2:    proc  0 (loop) line   7 "loops" (state 2)       [b = (2*a)]
	  3:    proc  0 (loop) line   7 "loops" (state 3)       [(1)]
	  4:    proc  0 (loop) line  10 "loops" (state 8)       [b = (b-1)]
	  5:    proc  0 (loop) line   5 "loops" (state 1)       [a = ((a+1)%3)]
	  6:    proc  0 (loop) line   7 "loops" (state 2)       [b = (2*a)]
	  7:    proc  0 (loop) line   7 "loops" (state 3)       [(1)]
	  8:    proc  0 (loop) line  10 "loops" (state 8)       [b = (b-1)]
	  9:    proc  0 (loop) line   5 "loops" (state 1)       [a = ((a+1)%3)]
	 10:    proc  0 (loop) line   8 "loops" (state 4)       [b = (2*a)]
	 11:    proc  0 (loop) line   8 "loops" (state 5)       [(1)]
	spin: line  10 "loops", Error: value (-1->255 (8)) truncated in assignment
	 12:    proc  0 (loop) line  10 "loops" (state 8)       [b = (b-1)]
	spin: trail ends after 12 steps
	#processes: 1
	 12:    proc  0 (loop) line   4 "loops" (state 9)
	1 process created

test 5	try to find a cycle that avoids the progress labels
	(there are none)

	$ cc -DNP -DNOREDUCE -o pan pan.c # add support for non-progress
	$ pan -l		# search for non-progress cycles
	(Spin Version 4.1.2 -- 21 February 2004)

	Full statespace search for:
	        never-claim             +
	        assertion violations    + (if within scope of claim)
>	        non-progress cycles     + (fairness disabled)
	        invalid endstates       - (disabled by never-claim)

	State-vector 20 byte, depth reached 23, errors: 0
	      27 states, stored (39 visited)
	      28 states, matched
	      67 transitions (= visited+matched)
	       0 atomic steps
	hash conflicts: 0 (resolved)
	(max size 2^18 states)

	unreached in proctype loop
	        line 12, state 12, "-end-"
	        (1 of 12 states)

test 6:	check partial order reduction algorithm -- first disable it

	$ spin -a leader # (or snoopy, pftp, sort)
	$ cc -DSAFETY -DMEMLIM=50 -DNOREDUCE -o pan pan.c	# safety only
	$ pan -c0 -n                # -n = no dead code listing
	(Spin Version 4.1.2 -- 21 February 2004)
	
	Full statespace search for:
	        never-claim             - (not selected)
	        assertion violations    +
	        cycle checks            - (disabled by -DSAFETY)
	        invalid endstates       +
	
	State-vector 200 byte, depth reached 108, errors: 0
	   15779 states, stored
	   42402 states, matched
	   58181 transitions (= stored+matched)
	      12 atomic steps
	hash conflicts: 709 (resolved)
	(max size 2^18 states)

	Stats on memory usage (in Megabytes):
	3.219   equivalent memory usage for states (stored*(State-vector + overhead))
	2.965   actual memory usage for states (compression: 92.12%)
	        State-vector as stored = 184 byte + 4 byte overhead
	1.049   memory used for hash table (-w18)
	0.280   memory used for DFS stack (-m10000)
	4.196   total actual memory usage

test 6b: now leave p.o. reduction enabled (i.e., do not disable it)

	$ cc -DSAFETY -DMEMLIM=50 -o pan pan.c  # safety only
	$ pan -c0 -n                # -c0 = ignore errors
	(Spin Version 4.1.2 -- 21 February 2004)
	        + Partial Order Reduction
	
	Full statespace search for:
	        never-claim             - (not selected)
	        assertion violations    +
	        cycle checks            - (disabled by -DSAFETY)
	        invalid endstates       +
	
	State-vector 200 byte, depth reached 108, errors: 0
	      97 states, stored
	       0 states, matched
	      97 transitions (= stored+matched)
	      12 atomic steps
	hash conflicts: 0 (resolved)
	(max size 2^18 states)

	If compiled and run as above, the results for the 4 examples
	given should match the results in the table below. 
	The numbers in the first two columns of the table
	should match exactly.  (Note, the leader election algorithm
	that is in the current distribution was extended slightly
	compared to the one that was there before version 2.9.1)
	The numbers in the third column should match approximately.
	How well these match depends only on the properties of
	the C-compiler and the speed of the hardware you use to
	run these tests.
	The first line for each test is for the exhaustive run,
	the second line is for the default reduced run.
	The times given are for a 2.5GHZ Windows PC, with 2 Gb of memory.

	States Stored	Transitions	Memory Used	Time (s)
leader
	S=   15779      T=   58181	M= 4.196 Mb	t= 0.25
	S=      97      T=      97	M= 1.573 Mb	t= 0.03

snoopy
	S=   61619	T=  211398	M= 7.68 Mb	t= 0.5
	S=    9343	T=   12706	M= 2.49 Mb	t= 0.08

pftp
	S=  144813	T=  397948	M= 19.45 Mb	t= 1.16
	S=   47356	T=   64970	M=  7.61 Mb	t= 0.26

sort
	S=  107713	T=  512419	M= 19.56 Mb	t= 1.56
	S=     135	T=     135	M=  1.57 Mb	t= 0.06


test 7	check random number generator

	$ spin -p -g -u3512 priorities		# stops after 3,512 steps
	....
	3510:   proc  3 (A) line   5 "priorities" (state 3)  \
		[printf('%d\\n',_pid)]
	                a[0] = 0
	                a[1] = 116
	                a[2] = 234
	                a[3] = 344
	                a[4] = 474
	....

	The numbers in the array that is printed at the end
	should tend to the ratio 1:2:3:4 if the random number
	generator works properly.
	array index 0 remains unused (it's the pid of the init
	process)

test 8	test the generation of never claims from LTL formulae:

	$ spin -f "[] ( p U ( <> q ))"
	never {    /* [] ( p U ( <> q )) */
	T0_init:
		if
		:: ((q)) -> goto accept_S9
		:: (1) -> goto T0_init
		fi;
	accept_S9:
		if
		:: (1) -> goto T0_init
		fi;
	}


test 9	read a never claim from a file (works only with 3.1.2 and later)

	$ spin -a -N leader.ltl leader	# the claim is in file leader.ltl
	$ cc -o pan pan.c		# the default compilation
	$ pan -a			# search for acceptance cycles
	warning: for p.o. reduction to be valid the never claim must be stutter-closed
	(never claims generated from LTL formulae are stutter-closed)
	(Spin Version 4.1.2 -- 21 February 2004)
	        + Partial Order Reduction
	
	Full statespace search for:
>	        never-claim             +
	        assertion violations    + (if within scope of claim)
	        acceptance   cycles     + (fairness disabled)
	        invalid endstates       - (disabled by never-claim)
	
	State-vector 208 byte, depth reached 205, errors: 0
	     181 states, stored (360 visited)
	     251 states, matched
	     611 transitions (= visited+matched)
	      24 atomic steps
	hash conflicts: 0 (resolved)
	(max size 2^18 states)
	
	unreached in proctype node
	        line 53, state 28, "out!two,nr"
	        (1 of 49 states)
	unreached in proctype :init:
	        (0 of 11 states)

test 10	try the new slicing analysis in version 3.4.0 and later:
	$ spin -V
	Spin Version 4.1.2 -- 21 February 2004
	$ spin -A wordcount
	spin: redundant in proctype :init: (for given property):
	      line  25 "test/wordcount" (state 14)	[(!(inword))]
	      line  26 "test/wordcount" (state 15)	[nw = (nw+1)]
	      line  26 "test/wordcount" (state 16)	[inword = 1]
	      line  21 "test/wordcount" (state 11)	[((((c==32)||(c==9))||(c==10)))]
	      line  22 "test/wordcount" (state 12)	[inword = 0]
	spin: redundant vars (for given property):
		int   	nw	0	<:global:>	<variable>
		bit   	inword	0	<:init:>	<variable>
	spin: consider using predicate abstraction to replace:
		int   	c	0	<:global:>	<variable>

end of tests