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 类型。但是，我想获得那个 char 的 mtype，有没有办法将一个 char 交叉引用回它的 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