问题标签 [nuxmv]

与固定长度位数组相比，为什么将 16 位有符号整数变量表示为区间（-32768..32767）时性能会显着下降？

检查预处理的 NuSMV/NuXMV 模型可以观察到区间类型转换为枚举。

然而，BDD 的统计数据并未显示任何相关信息。

我在我正在开发的作品上使用nuXmv，但我在使用 Reals 时遇到了麻烦。

假设我有程序：

我试图证明的这个例子的属性是 r 总是小于或等于 600。请注意，这只是一个说明性的例子，没有具体含义。

现在在命令行上我输入

为了运行程序并检查属性是否实现，但出现此消息

“在这个版本的 nuXmv 中，批处理模式不适用于包含无限域变量的模型。”

所以我发现的问题是使用Realon variable t。有没有办法像我在变量上使用的那样指定一系列实数值r（它是整数类型）？我知道如果这存在可以解决问题，如果没有，我如何在我的程序中使用 Reals？

提前感谢您的宝贵时间。

我有一个关于 nuXmv 解决方案的问题。我有一个简单的图表，其中初始状态是 s1，并且从 s1 有两条弧线，一条通往 s2，另一条通往 s3。从 s2 和 s3 有一条弧线通向 s1。这是 nuXmv 中描述情况的程序。

我不明白已经处于初始状态 s1 的 nuXmv 如何知道公式是错误的。它没有给出基于循环的反例，只是在 s1 中立即说基于 s1 的公式是错误的。我的解释是，如果没有正义假设，nuXmv 会立即假设其中一条路径永远不会被执行。但它不应该以循环为例吗？如果我只留下“CTLSPEC AF p;” nuXmv 返回一个循环作为反例。那么为什么对于“AF p & AF w”它只显示状态 s1 作为反例呢？

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

使用以下 CTL 规范

nuXmv 产生规范是真实的。

具有以下 LTL 规格

nuXmv 产生以下警告

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

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

有人有解释吗？

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

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

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

我正在使用 NuXMV 在相当大的模型上使用 msat_check_ltlspec_bmc 命令检查 LTL 属性。结果显示在给定范围内没有找到反例。我是否将其解释为该属性为 True。或者它也可能意味着分析不完整。

这是因为，通过改变属性命题为真或假，结果总是没有反例。大多数结果是违反直觉的。

从基于实变量的属性开始，但由于无法理解结果，使用相同的命令转移到同一模型上基于布尔的属性。

check_property我创建了一个通用 SMV 程序并使用和检查了一对 LTL 属性msat_check_ltlspec_bmc。发现true两个命令都有一个属性。相反，另一个属性给出了第一个命令的14个状态的反例和后一个命令的单状态反例。

问：为什么第二个反例只包含一个状态，应该如何解释？

通过标准 LTL 模型检查，我得到以下输出：

相反，通过msat_基于 - 的 LTL 模型检查，我得到以下输出：

以下属性对于 check_property 是正确的，但 msat_check_ltlspec_bmc 给出了反例。后一个的结果似乎是正确的。“G (((tt >= 7) -> G ((FlagLO = FALSE)))) IN 模块”。我们如何解释这一点？

我用稍微改变的 smv 文件尝试了这个。试图检查基于 LTL 属性的存在模式。Check_fsm 结果未早先运行。这造成了僵局。在这种情况下 msat_check.... 结果似乎不正确。现在哪一个是正确的？验证模型的正确方法应该是什么？需要使用实数，因此尝试 msat 命令。

这是的输出msat_check_ltlspec_bmc：

这是正常 LTLcheck_property调用的输出：

这是的输出check_fsm：

“check_fsm”命令在 nuxmv shell 中用于检查包含有限域变量的模型中的死锁条件。但是如果模型包含无限域变量，例如没有范围的整数或实变量，则无法使用“go”命令构建模型。我们如何使用“go_msat”命令检查死锁以构建模型和进一步分析。

我刚刚安装了 nuXmv 并想从示例文件夹中尝试示例增长计数器整数。当我尝试运行 command:build_model时，我收到错误消息：

文件 grow-counter-integer.smv：第 30 行：不可能构建具有无限精度变量的 BDD FSM

有人知道如何解决这个错误吗？提前致谢。

增长计数器整数.smv 文件：