spin - 在 Promela 中从另一个进程访问一个进程的局部变量

Question

是否可以从另一个进程访问一个进程的局部变量的值。例如在下面的程序中，我想从经理那里读取 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();

}

Answer 1

您可以使用“procname[pid]:var”来引用局部变量的当前值。

Answer 2

您可以使用 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
}

可以使用 c_expr{} 中的 'Pex1->x' 访问“ex1”的本地“x”。