问题标签 [nusmv]

我正在尝试使用 NuSMV 作为 java 中的模型检查器。但是，我无法在线找到相关的 JAR 库。

我在这里找到的唯一一个下载链接不再有效。显然，该库存在，但访问链接不起作用。

有谁知道我如何访问 NuSMV java API 库或知道任何替代方式？

AG(~q ∨ Fp)LTL 公式是否满足以下模型？为什么或者为什么不？

模型？

目前我正在尝试将系统原型转换为过渡系统模型。我有一些 LTL 属性，我想使用模型检查工具 NuSMV 验证这些属性。我只是介绍如何通过定义原子属性和其他数学方面来开始建模。

模型的图示

我正在使用 LTL 来定义开放交互协议的规则。然后我想检查一个特定的交互是否遵循规范，或者是否有任何规则被破坏。我的直接方法是使用 NuSMV，但问题是我没有要检查的交互模型，而只有一个特定的有限迹线（所有状态下所有变量的值）。

有什么方法可以在 NuSMV 中指定它吗？我基本上想输入 NuSMV 输出的模型之一作为反例：

并验证它。或者 NuSMV 是不是这个错误的工具？

谢谢！

我正在使用 NuSMV，并且正在尝试编写实时 CTL 属性。
我想知道是否有办法从状态设置步骤，例如：
((s.state = on) ABG (0..5 s.state = off))

读作：if (s.state=on) is true，从此状态和其他 5 个步骤的属性(s.state= off) is true。
我试图写这样的东西，但它不起作用。你能帮助我吗？

否则，是否可以从不是第一个状态开始检查相同的属性？

我想用 nuSMV 对对称分布式四处理器三着色协议进行建模。我的规范——我确信它的正确性——必须是正确的，但是当我对“Finally”属性使用关键字“F”时，nuSMV 在第一步就给了我一个反例并停止处理下一个状态。我应该怎么做才能修复它并检查 LTL 中的 finally 属性？

这是我的 SMV 代码：

这是我从 nuSMV 获得的反例：

谢谢你。

我正在为我的教育学习模型检查和 NuSMV。我可以编辑和运行 NuSMV 代码，并且我对 UART 是什么以及做什么有相当了解。

我的任务是用 NuSMV 对 UART 进行正式建模，但目前我不知道该怎么做。我知道 UART 将一个字节作为八个连续位传输，但我该如何建模呢？

我有一个互斥代码作为起点：

编码

我是 NuSMV 和 CTL 的新手，正在尝试简单的示例。我有 3 个状态 A、B 和 C，并且有一个从 A-> B 的转换

我在 NuSMV 中对其进行建模，并想检查是否存在从 B 到 A 的任何执行路径。尽管我没有定义这种转换，但规范给了我反例。

谁能告诉这有什么问题？

我如何编写“A 是否可以从 B 到达”的规范？- 这应该返回 false，因为没有定义转换

I am writing two modules in NuSMV but I am receiving the error, "Case conditions are not exhaustive" This error points to the last case statement I have in the code. I am not sure how to fix this because the cases that I currently have there are the only cases that the variable requires. The first module "train" is instantiated twice so that two trains can be on one track. The module "controller" acts as a controller which receives input from the two trains and prevents them both from being on a bridge at the same time.

Here is the code:

用于 Eclipse 的 nuseen 更新站点无法正常工作。