NuSMV 返回未定义的操作答案

【问题标题】：NuSMV returns undefined operationNuSMV 返回未定义的操作
【发布时间】：2020-06-19 15:01:29
【问题描述】：

我写了以下代码：

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 是未定义的。

【问题讨论】：

标签： model-checking nusmv modal-logic

【解决方案1】：

这是一个已知问题。

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

替换

x-1

与

x - 1

【讨论】：