Как я могу определить такой макрос в спине?

Я написал следующую модель:

#define inc(sn)if :: sn < 255 -> sn = sn + 1; ::else -> sn = 1; fi;
#define inc_twice(sn) if :: sn+2 >255 -> sn= sn-253; ::else -> sn=sn+2; fi;

active proctype monitor()
{
    byte sn = 255;
    assert (inc(sn) ==1);
}

Но компилятор терпит неудачу следующим образом:

spin: test2.pml:9, Error: syntax error  saw 'keyword: if' near 'if'
spin: test2.pml:9, Error: syntax error  saw 'token: ::'
spin: test2.pml:9, Error: syntax error  saw 'keyword: fi' near 'fi'
spin: test2.pml:11, Error: aborting (ana_stmnt)
child process exited abnormally.

Как я могу это решить?


promela spin
person sword    schedule 16.10.2020    source источник
comment
я должен изменить его на встроенный модуль?   -  person sword    schedule 16.10.2020
comment
Есть ли способ определить функцию для получения возвращаемого значения?   -  person sword    schedule 16.10.2020
comment
Проблема скорее всего не в том, что Promela не поддерживает макросы (см.: макросы ), но что вы встраиваете команды в утверждение, для которого требуется выражение. Вы пытались увеличить sn и только после проверки того, что значение sn равно 1?   -  person Patrick Trentin    schedule 24.10.2020

Ответы (1)


arrow_upward
0
arrow_downward

Я встретил ту же проблему. И вы можете решить эту проблему, изменив свой код на это:

#define inc(sn)if \\

:: sn < 255 -> sn = sn + 1 \\

::else -> sn = 1 \\

fi;

#define inc_twice(sn) if \\

:: sn+2 >255 -> sn= sn-253 \\

::else -> sn=sn+2 \\

 fi;

Я не знаю, что вызывает эту проблему, но я решаю ее вышеуказанным методом.

person rookie    schedule 10.02.2021