Прохождение по ссылке в Promela

В моем дизайне у меня есть 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)
}

P.S. Я не могу использовать, например:

mtype = { A, B, C }
...
proctype AProcess(bit AVar; mtype VAR)
...
run AProcess(varA, A)

а затем проверьте, какая переменная была передана, потому что AProcess не может знать о существовании других переменных


promela spin
person Boris Mocialov    schedule 18.11.2014    source источник

Ответы (1)


arrow_upward
2
arrow_downward

Поместите свои переменные в массив, а затем передайте индекс массива. Что-то типа:

// 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
person GoZoner    schedule 20.11.2014
comment
Я думаю, что у вас есть дополнительная информация в вашем коде. Но у меня есть идея. Спасибо - person Boris Mocialov; 24.11.2014