model-checking - NuSMV 中嵌套 NEXT 运算符的语法错误

Question

我尝试使用 NuSMV 来检查我的模型，这是代码。

但是，当我NuSMV kernel.smv在 shell 中输入时，会发生错误

file kernel.smv: line 16: nested NEXT operators: next(_b)
in definition of next(_cond)
in definition of next(tx.fired) at line 16

我是 NuSMV 模型检查器的新手，所以我无法修复这个语法错误。请帮忙，谢谢！

Answer 1

我能够从您的图像中创建一个MVCE：

MODULE trans(cond)
VAR
    fired : boolean;
ASSIGN
    init(fired) := FALSE;
    next(fired) := case
        !next(cond) : TRUE;
        TRUE        : FALSE;
    esac;

MODULE main
VAR
    _b : boolean;
    t  : trans(_cond);
DEFINE
    _cond := (_b != next(_b));

这里的设计问题正是模型检查器在错误消息中告诉您的内容：

NuSMV > reset; read_model -i t.smv ; go

file t.smv: line 6: nested NEXT operators: next(_b)
in definition of next(_cond)
in definition of next(t.fired) at line 6

运算符自身内部存在双重嵌套，但next()不支持此操作，因为它需要将执行范围扩大到current_state + selected_transition对之外，并且知道哪个转换来自仍在构建中的未来状态。

---

解决方法。

让我们采用以下模型，它与您的问题相同：

MODULE main()
VAR
    frst : 0 .. 1;
    scnd : boolean;

ASSIGN
    init(frst) := 0;
    init(scnd) := FALSE;

    next(scnd) := case
        next(middle) : TRUE;
        TRUE         : FALSE;
    esac;

DEFINE
    middle := (frst != next(frst));

我们想要scnd当true且仅当 的值将在状态和状态frst中发生变化。next()next(next())

为此，我们可以延迟执行跟踪的开始，这样我们就可以以足够的优势预测未来的价值。frst

让我们看一个例子：

MODULE main()
VAR
    hidden : 0 .. 1;
    frst   : 0 .. 1;
    scnd   : boolean;

ASSIGN
    init(hidden) := 0;
    init(frst)   := 0;
    init(scnd)   := FALSE;

    next(frst) := hidden; -- frst does not start "changing" arbitrarily
                          -- in the second state, but in the third state

    next(scnd) := case
        predicted : TRUE; -- true iff frst changes value 2 states from now
        TRUE      : FALSE;
    esac;

DEFINE
    middle    := (frst != next(frst));     -- true iff frst changes value
                                           -- from the current state to the
                                           -- next() state
    predicted := (hidden != next(hidden)); -- true iff frst changes value
                                           -- from the next state to the
                                           -- next(next()) state