私の設計では、N 個のグローバル変数と、状態に応じて、前述のパラメーターのいくつかをパラメーターとして受け取るメソッドがあります。
グローバル変数を参照渡しのパラメーターとして渡すことはできますか?
この論文は、結論の部分で明示的に次のように述べています。
「Spin がサポートしていない参照渡しパラメータの特別な形式」
これを行うことができる他の方法はありますか?(つまり、変数名を渡す)
構造を以下に示します
bit varA = 1;
bit varB = 1;
bit varC = 1;
proctype AProcess(bit AVar){
/* enter_crit_section */
/* change global varN */
/* exit_crit_section */
}
init {
run AProcess(varA)
run AProcess(varB)
run AProcess(varC)
}
PS たとえば、使用できません:
mtype = { A, B, C }
...
proctype AProcess(bit AVar; mtype VAR)
...
run AProcess(varA, A)
AProcess は他の変数の存在を認識できないため、どの変数が渡されたかを確認します。