在 Promela Spin 中将 char 转换回 mtype

【问题标题】：Convert char back to mtype in Promela Spin在 Promela Spin 中将 char 转换回 mtype
【发布时间】：2014-06-27 09:39:07
【问题描述】：

假设，例如，我有以下内容

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？

【问题讨论】：

标签： spin promela

【解决方案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

【讨论】：