spin - Promela Spin で char を mtype に戻す

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