问题标签 [nusmv]

我不知道如何在 NuSMV 中声明全局常量，方式类似于

在C.

我怎样才能在 NuSMV 中做到这一点？

at token "X": syntax error- 为什么语法错误？

我尝试使用关键字X，但从未成功。

在 NuSMV 中确实没有像 NULL、nil、None 这样的值吗？

而且我们不应该为流程制作模型，因为模型应该代表电子电路？

我的场景是我有一个 UART 连接器、一个主存储器和一个进程，后者在该进程中读取和写入主存储器并读取和写入 UART。在主存储器中有命名的数据K应该保持不变。我们想证明如果进程不写入K' then the value ofK` 等于它的下一个值。

我想知道我的模型是否足够细粒度或者是否过于抽象。另外，如果我使用了正确的数据类型。

在 nusmv 中运行规范期间，需要几个小时并最终给出“killed 9”的结果。如何加快执行速度？是否有选项可以增加 NuSMV 在规范运行期间可以使用的内存量？

我用这段代码验证了一个 8 位加法器。当我打印时，如果主模块为空，则可达状态数为 1，如果包含整个主模块，则为 2^32。是什么导致了报告的可达状态数量的差异？对于 4 位加法器，报告的可达状态数为 2^16。如果 n 是位数，则输入状态为 2^n 似乎是合乎逻辑的。所有其他州来自哪里？我注意到当我添加a : adder (in1, in2);状态增加的行时，但这只是通过实验验证，这是增加状态数量而不是加法器模块本身的原因。为什么？

我是 NuSMV 和 UPPAAL 的新手，正在解决这个问题。任何人都可以提供以下问题的解决方案吗？

对您自己设计的电梯系统的控制系统进行建模和分析，该电梯系统
服务于多个楼层（例如 4 或 5 个）并具有
多个 liX（例如 2 或 3 个），并且多个用户位于
各个楼层并具有个人希望凝胶到不同的
楼层。系统可以：
• 允许用户可以指示在某个楼层需要 liX，
和/或需要上或下和/或被要求去
某个楼层
• 或者用户可以 -- 一旦进入liX -- 请求实际楼层。
• 为了移动门必须关闭。• 不能跳过楼层。• 所有liX 的初始位置是1 楼。 a 电梯
仅由一个按钮控制，通过该按钮可以命令电梯到您所在的楼层。

我无法在 Windows 10 操作系统上安装 NuSMV-2.6.0-win64。我已成功下载此文件，但无法从已解压缩的“bin”文件夹安装。

当我尝试在SMV中检查“EG（！s11included＆！s10included）”时，它被报告为错误并给出了一个反例如下，我认为相反它支持这个CTL规范。我的 CTL 规范有问题吗？

我正在尝试对我创建的 NuSMV 模型运行“随机”或非确定性模拟。然而，在后续运行之间，产生的跟踪是完全相同的。

这是模型：

我在交互式 shell 中使用以下命令运行它：

也许我的模型有错误？或者我没有在 shell 中运行正确的命令。

提前致谢！

如何从 Java 访问NuSMV作为模型检查器？
我想使用库来调用 NuSMV 并读取 .smv 文件，检查LTLSPEC并返回满意消息或反例作为结果。
我找到了 nusmv-tools，它是一个基于 Eclipse 的 API。由于我与 IntelliJ 合作，我无法得到答案。我更喜欢一个不依赖于任何 IDE 的库。

谢谢你。