如何在spin中定义这样一个宏

Question

我编写了以下模型：

#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.

我该怎么解决？

Answer 1

我也遇到过同样的问题。您可以通过将代码更改为以下代码来解决此问题：

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

我不知道是什么原因导致了这个问题，但我通过上面的方法解决了它。