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 回答