Promela 中分号的使用

Question

我正在学习 Spin Modal Checker 的 promela 语法。我遇到了这段简单的代码。

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

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

Answer 1

Promela 中的分号是所谓的分隔符。

来自the reference：

The semicolon and the arrow are equivalent statement separators in Promela; they are not statement terminators, although the parser has been taught to be forgiving for occasional lapses. The last statement in a sequence need not be followed by a statement separator, unlike, for instance, in the C programming language.

所以您的问题的答案是：您不需要在 count++、count-- 或 fi 之后放置分号，因为它们是最后一个语句。如果你把它们放在那里，解析器将忽略。