问题标签 [nusmv]

我想知道是否有一种方法可以为 NuSMV 中的给定 LTL 公式生成不同的可能反例。如果我们需要为 LTL 公式生成反例，它会为我们生成一个。但是由 NuSMV 生成的那个可能不是最令人兴奋或最有见地的，因为对于相同的 LTL 公式可能还有其他反例。

你能建议一些一般的方法来让 NuSMV 产生一些与其产生的反例不同的反例吗？

一种方法是修改 LTL 公式本身，以便 NuSMV 一次性生成的反例对我们来说很有趣。但我相信系统的操纵过多，无法获得您想要的结果。

另外，您需要事先知道有趣的结果。但如果我已经知道有趣的反例，我为什么要让 NuSMV 再次向我确认呢？那么为什么还要麻烦设计一个 LTL 表达式来给出所需的反例呢？我希望 NuSMV 生成其他我没有想到的有趣的反例，从而增加价值。

如果在 NuSMV 中不可能，您能否建议任何其他可能的 LTL 模型检查器？

我想在特定条件下排除可能的下一个案例。例如，我有：

所有值 1..6 相同。否则，我必须做很多组合才能只返回空闲的位置。

有人知道这是否可能吗？

我想在 NuSMV 中实现一个转换系统，该系统在一个 .txt 文件中指定，我希望该工具读取该文件，然后从中构建 TS。文件格式为：

6

1 2

2 3

3 4

4 5

5 6

这是一个特定示例，其中 6 是顶点/节点的总数，后面是指定它们之间的边的元组。我查看了 NuSMV 中的一些示例，但没有得到任何相关示例来读取描述转换系统的文件。有人可以帮忙吗？

我徒劳地搜索了如何在 ubuntu 16.04 上运行 NuSMV。我已经安装了 NuSMV 二进制文件，我在 bin 文件夹中有一个可执行的 NuSMV，但它不会运行。我输入NuSMV -help但 cmd 报告NuSMV:command not found。关于如何运行 NuSMV/ 的任何想法还是我缺少类似安装的东西？

给定一个 NuSMV 模型，如何找到它的运行时以及它消耗了多少内存？

因此可以在系统提示符下使用此命令找到运行时：/usr/bin/time -f "time %es" NuSMV filename.smv

以上给出了挂钟时间。有没有更好的方法从 NuSMV 本身获取运行时统计信息？

另外如何找出程序在处理文件期间使用了多少 RAM 内存？

是否有可能在 NuSMV 中有一个没有转换到任何其他状态的状态？例如，在我的代码中 l3 没有任何转换是否有效？当我运行这个 NuSMV 时，我给出了“案例条件并不详尽”的错误。谢谢！

我正在尝试在 Mac 上运行 NuSMV，我可以正常运行它，但是当我需要使用交互模式时，-int 选项会出错 - 命令行选项“–int”是未知的。

有没有其他人有这个问题？

是否有任何工具或代码可以将 BPEL 转换为 NuSMV 代码？我找到了BPEL 业务流程的建模和验证论文，但没有提供工具或代码。

我有一个简单的 kripke 结构，其中有 3 个状态，具有以下转换：

s1 是唯一的初始状态。我不希望循环 s1 到 s2 重复超过一定数量（比如两次）。在其他过渡系统中，我可以在过渡中添加一个守卫。

Q1：Kripke 结构可以在转换时设置守卫吗？

Q2：如果是，我如何在 NuSmv 中建模？

谢谢

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

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

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

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