-- Updated for SPIN Version 5.0 --- October 2007 ---

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 (at command prompt $):
		$ 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 5.0 -- 26 October 2007

test 1	check that you can run a simulation

	$ spin hello
		passed first test!
	1 process created

	or without the default indenting of output:

	$ spin -T 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 5.0 -- 26 October 2007)

	Full statespace search for:
	        never-claim             - (none specified)
	        assertion violations    +
	        acceptance   cycles     - (not selected)
	        invalid endstates       +
	
	State-vector 12 byte, depth reached 11, errors: 0
	      15 states, stored
	       4 states, matched
	      19 transitions (= stored+matched)
	       0 atomic steps
	hash conflicts: 0 (resolved)
	
	2.501     memory usage (Mbyte)

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

	pan: elapsed time 0 seconds

test 3	cycle detection check (liveness):

	$ ./pan -a		# search for acceptance cycles
	pan: acceptance cycle (at depth 0)
	pan: wrote loops.trail
	(Spin Version 5.0 -- 26 October 2007)
	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 11, errors: 1
	      13 states, stored (15 visited)
	       2 states, matched
	      17 transitions (= visited+matched)
	       0 atomic steps
	hash conflicts: 0 (resolved)
	
	2.501     memory usage (Mbyte)

	pan: elapsed time 0.015 seconds
	pan: rate      1000 states/second

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

	$ spin -t -p loops	# guided simulation for the error-cycle
	Starting loop with pid 0
	  <<<<<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 5.0 -- 26 October 2007)
	
	Full statespace search for:
	        never claim             +
	        assertion violations    + (if within scope of claim)
	        non-progress cycles     + (fairness disabled)
	        invalid end states      - (disabled by never claim)
	
	State-vector 16 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)
	
	2.501           memory usage (Mbyte)
	
	unreached in proctype loop
	        line 12, state 12, "-end-"
	        (1 of 12 states)
	
	pan: elapsed time 0 seconds

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

	$ spin -a leader (or snoopy, pftp, sort)
	$ cc -DSAFETY -DNOREDUCE -DNOCLAIM -o pan pan.c	# safety only
	$ ./pan -c0 -n                # exhaustive, -c0 = ignore errors
	(Spin Version 5.0 -- 26 October 2007)

	Full statespace search for:
	        never claim             - (not selected)
	        assertion violations    +
	        cycle checks            - (disabled by -DSAFETY)
	        invalid end states      +
	
	State-vector 196 byte, depth reached 108, errors: 0
	    15779 states, stored
	    42402 states, matched
	    58181 transitions (= stored+matched)
	       12 atomic steps
	hash conflicts:       440 (resolved)
	
	Stats on memory usage (in Megabytes):
	3.010           equivalent memory usage for states (stored*(State-vector + overhead))
	2.731           actual memory usage for states (compression: 90.73%)
	                state-vector as stored = 177 byte + 4 byte overhead
	2.000           memory used for hash table (-w19)
	0.267           memory used for DFS stack (-m10000)
	0.094           memory lost to fragmentation
	4.904           total actual memory usage
	
	pan: elapsed time 0.125 seconds
	pan: rate    126232 states/second

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

	$ cc -DSAFETY -DNOCLAIM -o pan pan.c  # safety only, reduced search
	$ ./pan -c0 -n                # -n = no dead code listing

	(Spin Version 5.0 -- 26 October 2007)
	        + Partial Order Reduction
	
	Full statespace search for:
	        never claim             - (not selected)
	        assertion violations    +
	        cycle checks            - (disabled by -DSAFETY)
	        invalid end states      +
	
	State-vector 196 byte, depth reached 108, errors: 0
	       97 states, stored
	        0 states, matched
	       97 transitions (= stored+matched)
	       12 atomic steps
	hash conflicts:         0 (resolved)
	
	2.501           memory usage (Mbyte)
	
	pan: elapsed time 0 seconds

	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 precisely.  
	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 default run using partial order reduction.
	The times given are for a 2.4GHz dual-core Intel PC, with 2 GB of memory.

	States Stored	Transitions	Memory Used	Time (s)
leader
	S=   15779      T=   58181	M= 4.904 Mb	t= 0.125
	S=      97      T=      97	M= 2.501 Mb	t= <0.1

snoopy
	S=   61619	T=  211398	M= 8.03 Mb	t= 0.328
	S=    9343	T=   12706	M= 3.38 Mb	t= 0.03

pftp
	S=  144813	T=  397948	M= 18.97 Mb	t= 0.79
	S=   47356	T=   64970	M=  8.07 Mb	t= 0.14

sort
	S=  107713	T=  512419	M= 18.87 Mb	t= 1.08
	S=     135	T=     135	M=  2.50 Mb	t= <0.1


test 7	check random number generator

	$ spin -p -g -u10000 priorities		# runs 10000 steps
	....
	depth-limit (-u10000 steps) reached
	#processes: 5
	                a[0] = 0
	                a[1] = 334
	                a[2] = 677
	                a[3] = 994
	                a[4] = 1327
	10000:  proc  4 (A) line  11 "priorities" (state 3)
	10000:  proc  3 (A) line  12 "priorities" (state 2)
	10000:  proc  2 (A) line  14 "priorities" (state 4)
	10000:  proc  1 (A) line  11 "priorities" (state 3)
	10000:  proc  0 (:init:) line  22 "priorities" (state 6) <valid end state>
	5 processes created

	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
	        :: ((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

	$ 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-invariant
	(never claims generated from LTL formulae are stutter-invariant)
	
	(Spin Version 5.0 -- 26 October 2007)
	        + Partial Order Reduction
	
	Full statespace search for:
	        never claim             +
	        assertion violations    + (if within scope of claim)
	        acceptance   cycles     + (fairness disabled)
	        invalid end states      - (disabled by never claim)
	
	State-vector 204 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)
	
	2.501           memory usage (Mbyte)
	
	unreached in proctype node
	        line 53, state 28, "out!two,nr"
	        (1 of 49 states)
	unreached in proctype :init:
	        (0 of 11 states)
	
	pan: elapsed time 0 seconds

end of tests