Promela：proctypes 中的参数错误，以及使用 'end' 标签

Question

我是 Promela 的新手，我不确定我的代码有什么问题：

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
}

出现以下错误：

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

第 25 行是

proctype frogJump(int frogNum, int frogDirection)

第 30 行是

end:  do

据我所知，我应该使用 'end' 标签向 SPIN 发出信号，表明 frog proctype 可以被视为已结束，而不必位于其代码的末尾。但我遇到的问题是我似乎无法在 'end' 标签旁边使用 'do'。我也不知道参数 'int' 有什么问题。

Answer 1

这个错误

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

是由于 proctype declaration 的参数列表分隔符是 ; 而不是 ,。

您可以通过更改

来消除错误

proctype frogJump(int frogNum, int frogDirection)

进入这个

proctype frogJump(int frogNum; int frogDirection)

在inline functions的情况下，正确的参数列表分隔符确实是,，例如

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;
}

第二条错误信息

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

可能只是第一个语法错误导致的不正确解析树的副作用，在修复它时应该会相应地消失。

Promela：proctypes 中的参数错误，以及使用 'end' 标签

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

spin

promela