问题标签 [nusmv]

我是 NUSMV 的新手，我正在尝试为 reconize 41708 建模一个数字代码，但用户不能再犯 3 个错误。如果您输入更多 3 错误，当您输入要解锁的特殊代码时，系统会进入阻塞状态等待。如果您不能帮助我提出想法并建议完成代码，这是我的代码。

模型图像

我有一个异步对称环形协议，它有 5 个满足给定属性的进程。我想证明（或获得反例）该属性对于具有 6 个或更多进程的协议是正确的；那是

∀n.φ(n)

我决定使用假设保证，并nuSMV用于模型检查。

我知道以前版本的SMV可以Cadence支持此功能，但是有什么方法可以实现假设保证nuSMV吗？
如果没有，我可以使用其他模型检查器SPIN吗？

谢谢你。

模块 主要

IVAR v1 ：布尔值；

VAR v2：布尔值；

规格名称 p1 := AG (v1&v2);

文件 ltlerror.smv：第 8 行：属性包含输入变量：

IVAR我知道 . 中（输入变量）和VAR（状态变量）之间的区别NuSMV。但是，我能够理解使用时的反例VAR，但我不是在其他情况下。

让我用一个例子来展示它。

NuSMV 给出的反例（足够清楚）是：

现在，将 v1 和 v2 更改为 IVAR。

反例是：

有人可以解释为什么这个反例如此奇怪吗？它有几个嵌套循环。输出是什么意思？

最近我尝试将一些模型转换为 Nusmv 模型，但我想尝试更改“TRUE：”关键字的功能。众所周知，“case ... esac;”中的“TRUE：” 当案例条件没有特定条件时，可以定义一些您想要的操作，但是，我要求天气“真”可以执行最后一次操作，例如：

换句话说，当'a'=0时，如果上次'a'被赋值-10，那么这次也将被赋值-10；如果上次'a'被分配了10，这次它也将被分配10。

那么，现在的问题是，是否可以通过更改 NuSMV 的源代码来做到这一点，你能告诉我哪个是在“case”中实现“TRUE”函数的 c 语言文件吗？

感谢您的帮助！

我正在使用 nuXmv 1.1.1 对以下有限状态机进行模型检查。

使用以下 CTL 规范

nuXmv 产生规范是真实的。

具有以下 LTL 规格

nuXmv 产生以下警告

******** 警告 ******** 有限状态机的初始状态集是空的。这可能会使模型检查的结果不可信。********结束警告********

我理解警告，但我不明白为什么会出现。在我看来，它应该与两种规格一起出现，或者根本不出现。

有人有解释吗？

我在 NuSMV 中有以下代码。

所以 x 是一个变量，可以取整数值 0,1,2,3,4,5。接下来，我初始化它并制定它的转换规则。

上面应该说的是 x 最初是 1。然后如果 y=1 且 z=23，x 变为 4，否则 x 可以假设其域中的任何随机值。逻辑的这个“否则”部分是我怀疑的。我是否正确编码？y 和 z 是变量，其代码未在此处显示。为 y 和 z 假设一些东西。

或者我应该写：

因为我从本文档的第 4 页确定以上内容是正确的。

但这对于非常大的域是不可行的。假设 x 可以取 0 到 293 之间的任何值。

我在 NuSMV 中有一段代码出现了错误。代码是： -

所以当我在 NuSMV 中编译它时，它给出了一个错误：recursively defined: x1

现在我可以通过删除与 x2 关联的下一个语句来处理 x1 的转换规则，这意味着我替换x1=d & next(x2)=c : a;为x1=d : a;orx1=d & x2=d : a;

我想了解导致错误的 NuSMV 软件的机制以及上述修复解决错误的原因。我认为这与我不明白的同步实现有关。有人可以给出精确的详细技术解释吗？

并解释为什么 variable 没有错误x2。它的转换规则也使用 next 运算符定义。

假设我在 NuSMV 中编写了一个从状态 S1 开始的模型。我想在这个模型检查器中检查我是否最终在所有情况下都达到状态 S70。现在可视化我编码的 NuSMV 模型，如下所示：

从上面很明显，最终会达到 S70，但可能需要超过 70 个时间步长。为什么？因为您可能会先进入 S2，然后再进入 S3，而不是再进入 S4，然后再回到 S2，这种模式会重复，比如 100 次。NuSMV 软件也考虑了这种可能性，以确认肯定会达到 S70。

问题是 NuSMV 表示无法到达 S70 并生成了一个反例，这正是：-

所以反例就是这4个步骤。但令我惊讶的是，NuSMV 无法弄清楚这种僵局最终会随着时间的推移而得到解决。为什么我得到一个非直观的结果？

我在图中显示的自动机可能是我希望我的 NuSMV 代码表示的，但我错误地编码了一两行，但我不这么认为。否则 NuSMV 怎么会认为它可以从 S2 转到 S3。如果它可以计算出可以从 S2 转到 S3，那么为什么要在 S2 处终止上面的反例呢？

有人可以解释吗？

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

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

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