问题标签 [nusmv]

无论如何使用 NuSMV 将属性验证结果分配给变量？

例如： check_ctlspec "AG(lift.pressed -> lif.button)" 模型检查结果为： "AG(lift.pressed -> lif.button)" 为 TRUE

我需要将验证结果TRUE保存在x中，并使用这种方式来比较一些结果。

x:=check_ctlspec "AG(lift.pressed -> lif.button)" 即 x=TRUE

先感谢您

我正在尝试在 NuSMV 中实现基本交换指令，所以我有局部变量 a1,tmp,a2 来执行逻辑

tmp = a1; a1 = a2; a2 = tmp

但是，我不知道如何next()在 NuSMV 中保持这种顺序，任何想法都会受到赞赏。

我是学习 nuXMV 的新手，希望有人能帮助我。我正在尝试从 UPAAL 实现灯示例，只是为了学习如何使用这个工具。

所以我想做的是这个例子：

我知道下面的代码不起作用，但这就是我走了多远。我不知道如何模拟例如用户的按钮按下。

如果有人知道如何对其进行编码 - 有一个示例可以指导它会很好:)

我在以下代码中缺少什么？我正在尝试实施摆渡人解决方案。你会建议如何填写？部分？谢谢！

我正在尝试将状态机（在 中给出scxml）转换为NuSMV2.6 版，我在用户手册中遇到了这一点：

绕过它的最佳方法是什么？在没有进程的 NuSMV 中表示并行状态机的最佳方法是什么？有 flatten 方法，但是当超过 3 个状态时就很复杂了。所以我寻求更好的方法。

谢谢！