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

Question

В моей конструкции у меня есть N глобальные переменные и метод, который принимает в качестве параметра некоторые из указанных параметров в зависимости от состояния.

Могу ли я передавать глобальные переменные в качестве параметров по ссылке?

This paper явно говорит в заключительной части, что

«особая форма вызова по ссылке передачи параметров, что спина делает не поддерживает»

Есть еще какой-нибудь другой способ, чтобы иметь возможность сделать это? (Т.е. передать имя переменной)

Структура приводится ниже

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) 

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

Answer 1

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

// 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