Promela中分号的使用

Question

我正在学习自旋模式检查器的promela语法。我遇到了一段简单的代码。

int count;
active proctype count(){
if
::   count++
::   count--
fi
}

如我所知，分号用于定义语句的结尾。我可以在count++和count--的末尾以及fi之后使用fi吗?它会改变程序的行为方式吗？我很感激能帮我清理掉这个分号。

Answer 1

在Promela中分号是所谓的分隔符.

来自参考文献

分号和箭头在Promela中是等价的语句分隔符；它们不是语句终止符，尽管解析器被教导要原谅偶尔出现的错误。序列中的最后一条语句不需要后面跟着语句分隔符，例如，在C编程语言中。

因此，您的问题的答案是:您不需要在count++、count--或fi之后加上分号，因为它们是最后的语句。如果您将它们放在那里，解析器将忽略它们。