Search code examples
spinpromela

Format verification in SPIN

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

enter image description here

What do they mean?

Thanks

Solution

  • 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