if-statement - Promela 中的分号用法

Question

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

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

据我所知，分号用于定义语句的结尾。我可以;在count++andcount--和 after的末尾使用吗fi？它会改变程序的行为方式吗？我会很感激为我清除这个分号的东西。

Answer 1

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

从参考：

分号和箭头在 Promela中是等效的语句分隔符；它们不是语句终止符，尽管解析器被教导要容忍偶尔的失误。序列中的最后一条语句不需要跟语句分隔符，这与 C 编程语言中的情况不同。

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