Доступ к локальной переменной одного процесса из другого в Promela

Можно ли получить доступ к значению локальной переменной одного процесса из другого процесса. Например, в программе ниже я хочу прочитать значение my_id из менеджера.

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

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

}


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

}

spin
person Community    schedule 25.12.2012    source источник

Ответы (2)


arrow_upward
1
arrow_downward

Вы можете сделать это, используя синтаксис c_code{} и/или c_expr(). Вот пример из руководства SPIN:

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
}

Доступ к локальному «x» для «ex1» можно получить, используя «Pex1->x» из c_expr{}.

person GoZoner    schedule 06.03.2013

arrow_upward
2
arrow_downward

Вы можете обратиться к текущему значению локальной переменной, используя "procname[pid]:var".

person Mass    schedule 30.10.2014