Accessing local variable of one process from another in Promela

Question

Is it possible to access value of local variable of one process from another process . For example in program below, I want to read value of my_id from manager.

proctype user (byte id){
    byte my_id = id;
}

proctype manager (){
     printf ("my_id : %d \n" , user:my_id);

}


init {
    run user (5);
    run manager();

}

Answer 1

You can accomplish this using c_code{} and/or c_expr() syntax. Here is an example from the SPIN manual:

active proctype ex1()
{   int x;

    do
    :: c_expr { Pex1->x < 10 } ->
        c_code { Pex1->x++; }
    :: x < 10 -> x++
    :: c_expr { fct() } -> x--
    :: else -> break
    od
}

The local 'x' of 'ex1' can be accessed using 'Pex1->x' from within c_expr{}.

Answer 2

You can refer to the current value of local variable by using "procname[pid]:var".