-- Updated for SPIN Version 3.1 ---

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)

	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 and is executable

	$ spin -V
	Spin Version 3.1.2 -- 14 March 1998

test 1	check that you can run a simulation

	$ spin hello
	passed first test!
	1 processes 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 3.1.2 -- 14 March 1998)

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

test 3	cycle detection check (liveness):

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

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

	$ spin -t -p loops	# guided simulation for the error-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)]
	<<<<<START OF CYCLE>>>>>
	  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   7 "loops" (state 2)       [b = (2*a)]
	 11:    proc  0 (loop) line   7 "loops" (state 3)       [(1)]
	 12:    proc  0 (loop) line  10 "loops" (state 8)       [b = (b-1)]
	 13:    proc  0 (loop) line   5 "loops" (state 1)       [a = ((a+1)%3)]
	 14:    proc  0 (loop) line   8 "loops" (state 4)       [b = (2*a)]
	 15:    proc  0 (loop) line   8 "loops" (state 5)       [(1)]
	spin: trail ends after 15 steps
	#processes: 1
	 15:    proc  0 (loop) line  10 "loops" (state 8)
	1 processes 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 3.1.2 -- 14 March 1998)
	
	Full statespace search for:
	        never-claim             +	# i.e., an implicit claim 
	        assertion violations    +
>	        non-progress cycles     + (fairness disabled)
	        invalid endstates       - (disabled by never-claim)
	
	State-vector 16 byte, depth reached 30, errors: 0
	      30 states, stored (43 visited)
	      35 states, matched
	      78 transitions (= visited+matched)
	       0 atomic steps
	hash conflicts: 0 (resolved)
	(max size 2^18 states)
	
	1.493   memory usage (Mbyte)

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


test 6:	check partial order reduction algorithm

	$ spin -a leader (or snoopy, pftp, sort)
	$ cc -DSAFETY -DNOREDUCE -DNOCLAIM -o pan pan.c	# safety only
	$ pan -c0 -n                # exhaustive, -c0 = ignore errors
	...
	$ cc -DSAFETY -DNOCLAIM -o pan pan.c  # safety only, reduced search
	$ pan -c0 -n                # -n = no dead code listing
	(Spin Version 3.1.2 -- 14 March 1998)
	
	Full statespace search for:
	        never-claim             - (not selected)
	        assertion violations    +
	        cycle checks            - (disabled by -DSAFETY)
	        invalid endstates       +
	
	State-vector 196 byte, depth reached 125, errors: 0
	   41692 states, stored
	  127998 states, matched
	  169690 transitions (= stored+matched)
	      18 atomic steps
	hash conflicts: 17950 (resolved)
	(max size 2^18 states)
	
	Stats on memory usage (in Megabytes):
	8.338   equivalent memory usage for states (stored*(State-vector + overhead))
	7.061   actual memory usage for states (compression: 84.68%)
	        State-vector as stored = 165 byte + 4 byte overhead
	1.049   memory used for hash-table (-w18)
	0.200   memory used for DFS stack (-m10000)
	8.417   total actual memory usage

	If compiled as above, the results should match the results from
	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 it matches depends only on the properties of
	the C-compiler and the speed of the hardware you use to
	run the tests.)
	The first line for each test is for the exhaustive run,
	the second line is for the reduced run.
	The times given are for an SGI system, with a 150 MHz 
	MIPS R4400 Cpu and 1 Gigabyte of main memory.

	States Stored	Transitions	Memory Used	Time (s)
leader
	S=   41692	T=  169690	M= 8.42 Mb	t=  9
	S=     108	T=     108	M= 1.08 Mb	t= <0.1

snoopy
(1)	S=   91920	T=  305460	M= 9.89 Mb	t= 14
	S=   15295	T=   20490	M= 2.90 Mb	t=  1

pftp
	S=  439895	T= 1301620	M= 55.9 Mb	t= 64
	S=   95241	T=  130859	M= 13.5 Mb	t=  6

sort
(2)	S=  659683	T= 3454990	M= 113.6 Mb	t= 170
	S=     182	T=     182	M=   1.1 Mb	t= <0.1

Note:
(1) perform this run as:  pan -m13000 -c0 -n
(2) if you have less than approx 100 Mb of main memory, the
    runtime for this test can increase considerably due to paging.
    (the verifier assumes a statespace that fits in memory)


test 7	check random number generator

	$ spin -p -g priorities		# will not terminate
	....
	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
	....

	Interrupt the run after it executes for a while.
	Note: the numbers in the array 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
	        :: ((p)) -> goto T0_init
	        :: (1) -> goto T0_S28
	        :: ((q)) -> goto accept_S14
	        fi;
	accept_S14:
	        if
	        :: (1) -> goto T0_S28
	        :: (((p) || (q))) -> goto T0_init
	        fi;
	accept_S28:
	        if
	        :: (1) -> goto T0_S28
	        :: ((q)) -> goto T0_init
	        fi;
	T0_S28:
	        if
	        :: ((q)) -> goto accept_S28
	        :: (1) -> goto T0_S28
	        :: ((q)) -> goto accept_S14
	        fi;
	accept_all:
	        skip
	}

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 3.1.2 -- 14 March 1998)
	        + 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 204 byte, depth reached 233, errors: 0
	     202 states, stored (402 visited)
	     281 states, matched
	     683 transitions (= visited+matched)
	      36 atomic steps
	hash conflicts: 0 (resolved)
	(max size 2^18 states)
	
	1.493   memory usage (Mbyte)
	
	unreached in proctype node
	        line 105, state 28, "out!two,nr"
	        (1 of 49 states)
	unreached in proctype :init:
	        (0 of 11 states)

end of tests