Promela语法错误

Question

当我试图运行我的promela代码时，我收到了一个语法错误，错误上写着错误:语法错误看到了'token：‘

它指的是这一行代码(第10-13行)：

#define IniRunning(x,y) if
                    :: ((x==A) && (y==B)) -> IniRunningAB = 1
                    :: else skip
                    fi

我试着在if之后加上一个分号，也在fi之后添加一个分号，但是错误似乎并没有消失。

有人有什么想法吗？

Answer 1

将\放在宏定义的每一行中断之前。

您可以使用spin -I check.pml检查中间文本(宏展开后)。