Follow the link in Promela
In my design, I have global variables N and a method that takes as a parameter some of the specified parameters depending on the state.
Can I pass global variables as parameters by reference?
This article explicitly states in the Conclusion part that
"special form of callable parameter passing through Spin does not support"
Is there any other way to do this? (i.e. the name of the transfer variable)
The structure is given below
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 I cannot use for example:
mtype = { A, B, C }
...
proctype AProcess(bit AVar; mtype VAR)
...
run AProcess(varA, A)
and then check which variable was passed as AProcess cannot know about the existence of other variables
+3
source to share
1 answer
Put the variables into an array and then pass the array index. Something like:
// 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 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
+1
source to share