將char轉換回在PROMELA旋M型

Question

比方說，例如，我有以下

mtype = {ONE, TWO, THREE} ; 
mtype array[3] ; 
mtype test ; 
test = array[0] ; 
printf("Test is %e\n", test) ; 

我得到

Test is 1 

我的理解是，因爲潛在變量是char類型。但是，我想獲得該字符的mtype，是否有任何方法來交叉引用一個字符回到它的mtype？

Answer 1

您尚未使用有效值初始化array[3]。以下是我得到：

== foo.pml == 
mtype = {ONE, TWO, THREE}; 
mtype array[3]; 
mtype test; 

init { 
    array[0] = TWO; // initialize! 
    test = array[0]; 
    printf ("Test is '%e'\n", test); 
} 

$ spin foo.pml 
     Test is 'TWO' 
1 process created 

如果我再修改foo.pml刪除的array[0]初始化，那麼輸出是：

$ spin foo.pml 
     Test is '0' 
1 process created