NuSMV中嵌套的NEXT运算符存在语法错误
NuSMV中嵌套的NEXT运算符存在语法错误
提问于 2018-10-07 22:04:23
我尝试使用NuSMV来检查我的模型，下面是代码。
但是，当我在外壳程序中输入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模型检查器的新手，所以我不能修复这个语法错误。请帮帮忙，谢谢！
回答 1
Stack Overflow用户
回答已采纳
发布于 2018-10-08 00:26:17
我能够从你的图像中创建一个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 6next()运算符在其内部有一个双重嵌套，这是不受支持的，因为它需要将执行范围增加到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页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持
原文链接：
https://stackoverflow.com/questions/52689245
复制相关文章
相似问题
腾讯云开发者
