Will check into this for the next release.
Thanks for reporting that!
Unfortunately, I may not post the promela file, and a simplified version does not lead to these errors but to a successful non-progress cycle check.
What causes these errors? With a hint, I might be able to avoid these errors or write a simplified version that still exposes these errors.
------------------------------------
Here is the output from the problematic promela file:
Checking syntax and generating the pan.c verifier ...
/opt/local/bin/spin -a sSDPV1.pml
...
the model contains 12 never claims: ...
only one claim is used in a verification run
choose which one with ./pan -a -N name (defaults to -N REQ0)
or use e.g.: spin -search -ltl REQ0 sSDPV1.pml
No Syntax Error.
Starting verification...
gcc -DMEMLIM=1024 -DNP -DNOFAIR -DNOCLAIM -DXUSAFE -O2 -w -o pan pan.c
pan.c:7485:26: error: expected expression
if (stopstate[((Pclaim *)pptr(0))->_t][((Pclaim *)pptr(0))->_p])
^
pan.c:7485:18: error: use of undeclared identifier 'Pclaim'
if (stopstate[((Pclaim *)pptr(0))->_t][((Pclaim *)pptr(0))->_p])
^
pan.c:7485:51: error: expected expression
if (stopstate[((Pclaim *)pptr(0))->_t][((Pclaim *)pptr(0))->_p])
^
pan.c:7485:43: error: use of undeclared identifier 'Pclaim'
if (stopstate[((Pclaim *)pptr(0))->_t][((Pclaim *)pptr(0))->_p])
^
pan.c:8796:39: error: expected expression
printf(" (%s)\n", procname[((Pclaim *)pptr(0))->_t]);
^
pan.c:8796:31: error: use of undeclared identifier 'Pclaim'
printf(" (%s)\n", procname[((Pclaim *)pptr(0))->_t]);
^
6 errors generated.
Verification: Compile-Time Error - Process ExitValue: 1