When you run a SPIN verification there is no printed output; only an indication of whether or not errors were found (and other performance information). Note, since you are a beginner, you 'run a SPIN verification' when you invoke spin with 'spin -a …' and then run the compiled code.
There are two ways to see output. First, use SPIN in simulation mode by using spin hello.pml
. For example:
$ cat >hello.pml <<EOF
> init { printf ("hello world\n"); }
> EOF
$ spin hello.pml
hello world
1 process created
Second, use SPIN in verification mode but inject an error into your program. After the error occurs, examine the trail file. For example:
$ cat >hello.pml <<EOF
> init { printf ("hello world\n"); assert (0); }
> EOF
$ spin -a hello.pml
$ gcc -o hello pan.c
$ ./hello
hint: this search is more efficient if pan.c is compiled -DSAFETY
pan:1: assertion violated 0 (at depth 0)
pan: wrote hello.pml.trail
...
State-vector 12 byte, depth reached 0, errors: 1
...
pan: elapsed time 0 seconds
$ spin -p -t hello.pml
using statement merging
hello world
1: proc 0 (:init:) hello.pml:1 (state 1) [printf('hello world\\n')]
spin: hello.pml:1, Error: assertion violated
spin: text of failed assertion: assert(0)
1: proc 0 (:init:) hello.pml:1 (state 2) [assert(0)]
spin: trail ends after 1 steps
#processes: 1
1: proc 0 (:init:) hello.pml:1 (state 3) <valid end state>
1 process created
You can find 'hello world' in the above after spin -p -t hello.pml