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

Question

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

但是，当我在shell中输入NuSMV kernel.smv时，出现错误

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 + chosen_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

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

syntax error nested NEXT operator in NuSMV

model-checking

nusmv

nuxmv