Promela: ошибки с параметрами в проктипах и использованием метки «конец» - PullRequest
Новая
       68

Promela: ошибки с параметрами в проктипах и использованием метки «конец»

1 голос
/ 04 марта 2020

Я новичок в 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, что прокт типа лягушки может быть считается законченным без необходимости быть в конце своего кода. Но у меня проблема в том, что я не могу использовать «do» рядом с «end». Я также не знаю, в чем проблема с параметром int.

1 Ответ

1 голос
/ 04 марта 2020

Эта ошибка 

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

вызвана тем, что разделитель списка аргументов для объявления proctype равен ;, а не ,.

Вы можете устранить ошибку go, изменив 

proctype frogJump(int frogNum, int frogDirection)

на этот 

proctype frogJump(int frogNum; int frogDirection)

В случае встроенных функций , правильный список аргументов разделитель действительно ,, например 

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'

, вероятно, является лишь побочным эффектом неправильного дерева синтаксического анализа в результате первой синтаксической ошибки, и должны соответственно исчезать при ее исправлении.

...