Format verification in SPIN

Question

I learned Promela and Spin, but when I try verifying the model, these lines are returned to me.

What do they mean?

Thanks

Answer 1

That means that you ran a Spin verification and your verification identified an error. Your next step is to determine how the error occurred. You do that by generating and examining the 'trail file'.

If you performed your verification as:

$ spin -a model.pml
$ gcc -o pan pan.c
$ ./pan

then examine the trail using the model.pml file with:

$ spin -p -t model.pml

Answer 2

Probably, you have a deadlock or other error in your model.

If you would post your complete console output, I could probably update this answer to give you more information!