Promela: Errors with parameters in proctypes, and using 'end' label

Question

I'm new to Promela, and I'm not sure what the issue with my code is:

proctype frogJump(int frogNum, int frogDirection)
{  
printf("FROG%d STARTS AT %d", frogNum, frogs[frogNum]);
int temp;

end:  do
      :: lock(mutex) ->
          if
          ::(frog[0] == frogs[frogNum]+frogDirection || frog[0] == frogs[frogNum]+frogDirection+frogDirection]) ->
              temp = frog[frogNum];
              frog[frogNum] = frog[0];
              frog[0] = temp;
              printCurrentLayout();
              printf("FROG%d FROM %d TO %d", frogNum, temp, frog[frogNum]);
          :: else -> unlock(mutex);
          fi;
    :: skip;
    od
}

Getting the following errors:

spin: frogs.pml:25, Error: syntax error saw 'data typename' near 'int'
spin: frogs.pml:30, Error: syntax error saw 'an identifier' near 'end'

With line 25 being

proctype frogJump(int frogNum, int frogDirection)

and line 30 being

end:  do

As far as I understand, I'm supposed to use the 'end' label to signal to SPIN that the frog proctype can be considered ended without having to be at the end of it's code. But I'm having the issue that I can't seem to use 'do' beside the 'end' label. I also don't know what the issue with the parameter 'int' is.

Answer 1

This error

spin: frogs.pml:25, Error: syntax error saw 'data typename' near 'int'

is caused by the fact that the argument list separator for a proctype declaration is ; and not ,.

You can make the error go away by changing

proctype frogJump(int frogNum, int frogDirection)

into this

proctype frogJump(int frogNum; int frogDirection)

In the case of inline functions, the correct argument list separator is indeed ,, e.g.

inline recv(cur_msg, cur_ack, lst_msg, lst_ack)
{
    do
    :: receiver?cur_msg ->
        sender!cur_ack; break /* accept */
    :: receiver?lst_msg ->
        sender!lst_ack
    od;
}

---

The second error message

spin: frogs.pml:30, Error: syntax error saw 'an identifier' near 'end'

is probably just a side effect of the incorrect parsing tree resulting from the first syntax error, and should fade away accordingly when fixing it.