Spin Modal Checker の promela 構文を学習しています。この単純なコードに遭遇しました。
int count;
active proctype count(){
if
:: count++
:: count--
fi
}
私が知っているように、セミコロンはステートメントの終わりを定義するために使用されます。andと after;
の両方の最後で使用できますか; プログラムの動作は変わりますか? このセミコロンをクリアしてくれてありがとう。count++
count--
fi