CODEWITHSUNDEEP
spinpromela
Boris Mocialov
Boris Mocialov

Reputation: 3489

Pass by-reference in Promela

In my design, I have N global variables and a method, that takes as parameter some of the mentioned parameters, depending on the state.

Can I pass global variables as parameters by-reference?

This paper explicitly says in Conclusion part that

"special form of call-by-reference parameter passing that Spin does not support"

Is there another any other way to be able to do this? (i.e. pass variable name)

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)
}

P.S. I am not able to use, for instance:

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

and then check which variable been passed, because AProcess cannot know about existence of other variables

Upvotes: 4

Views: 665

Answers (1)

GoZoner
GoZoner

Reputation: 70135

Put your variables into an array and then pass around 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'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

Upvotes: 2

Related Questions