NuSMV 返回未定义的操作

Question

我写了以下代码：

MODULE main
VAR
status:{empty, no_empty};
x : 0..3;
ASSIGN
init(status):= empty;
init(x):=0;
next(status):= case
(status = empty): no_empty;
(status = no_empty) & (x=0): empty;
TRUE: status;
esac;
next(x):= case
(status = empty): x+3;
(status = no_empty) & (x>0): x-1;
TRUE: x;
esac;

但是，当我执行命令"flatten_hierarchy"时，出现以下错误："x-1"未定义

我不知道为什么 x-1 是未定义的。

Answer 1

这是一个已知问题。

解析器混淆了标识符x-1，而它应该是一个表达式。

取代

x-1

跟

x - 1