4

私の設計では、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 は他の変数の存在を認識できないため、どの変数が渡されたかを確認します。

4

1 に答える 1

2

変数を配列に入れてから、配列インデックスを渡します。何かのようなもの:

// A type to identify VARs; we pass these values to simulate 'by reference'
#define var_id byte

// A VAR 
typedef var_struct
{
   bit val;  // The var's value
};

#define VAR_COUNT 3

// allocate the VARs
var_struct var_array [VAR_COUNT];

// Access the value for VAR (based on var_t
#define VAR_VAL(id)   var_array[(id)].val
于 2014-11-20T23:21:49.843 に答える