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

이 작업은 c_code {} 및/또는 c_expr() 구문을 사용하여 수행 할 수 있습니다. 여기 SPIN 교재 예이다 :

국부 'EX1'의 'X'

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 
} 

사용하여 액세스 할 수있다 '는 Pex1-> X'c_expr 내에서 {}.

Answer 2

"procname [pid] : var"를 사용하여 로컬 변수의 현재 값을 참조 할 수 있습니다.