问题标签 [model-checking]

我只是想出了这个问题。正如在 Logic in Computer Science 一书中所写，LTL 的重要等价之一是：Fp=TUp。T 表示没有约束。

但是，如果我将 T 替换为（而不是 p）呢？Fp=(not p)Up 成立吗？因为在这种情况下，我实际上在公式中加入了一些约束（不是 p），但同时不可能有任何状态可以同时满足（不是 p）和 p。我尝试使用不同的 LTL 公式作为 p，只要 p 是可满足的，那么对于每条带有 p 的路径，它也必须满足 Fp 和（而不是 p）Up。这是否意味着我可以用这种方式重写 F 或者有一些反例？

CBMC 在以下行中检测到可能的无符号加法溢出：

我同意第一行有溢出的可能性，但我正在处理 CBMC 无法查看的下一行中的进位。如果出现溢出，我将设置进位 1。因此，由于我知道这一点，这就是我希望我的代码工作的方式，我想继续验证过程。那么，我是如何告诉 CBMC 忽略这个错误并继续前进的呢？

我在 ispin 中建模了一个系统，当尝试使用 LTL 公式验证系统时，我发现了无法访问的错误，例如

我的 ltl 公式是

在最后一段，用户手册 2.5 的第 23 页（我使用的是 2.5.4）：

“类型说明符可以由两个用 .. (<TWO DOTS>) 分隔的表达式给出。这两个表达式都必须计算为常量整数，并且可以包含定义名称和模块形式参数。例如，-1 - P1 .. 5 + D1，其中 P1 指的是模块形式参数，而 D1 指的是定义。P1 和 D1 都必须可以静态评估为整数常量。”

我已经测试了许多不同的示例来运行类似的东西，但我最终不能。这是其中之一：

或类似的东西：

错误是“无效的子范围 1 .. n”

有谁能够帮我？你能给我例子，类型说明符包含定义和模块形式参数的名称并正确运行吗？

事实上，这段代码是 fiat-shamir 协议的一部分，我正在对不同的 n 值（n 不能是常量整数）测试 ctl，并寻找一个反例。

我正在做 CTL 练习，我正在尝试检查以下公式是否等效。但我不确定我是否做得对。

第一个公式：等效

第二个公式：等价

第三个公式：等价

这样对吗？如果错了，你能给我一个 Kripke 模型中可能的反例吗？

提前致谢。

在下面的代码中有一个调用约定错误（可能导致一个永恒的循环），我无法检测到它。我尝试使用“Satabs”验证代码。什么样的模型可以使错误浮出水面。使用以下模型，我得到一个段错误。通过改变 VLEN 和 TMAX 你可以玩一点。

• Q1。什么是调用约定错误？
• Q2。哪种模型最适合用于查找错误？

如何比较两个 LTL 以查看其中一个是否相互矛盾？我问这个是因为我有一个分层状态机和描述每个状态行为的 LTL。我需要知道本地 LTL 是否可以与全局 LTL 相矛盾。我在文章“特征规范和自动冲突检测”中看到，如果 L(f) 交集 L(g) 为空，则两个 LTL 属性 f 和 g 不一致。这正是以 f 作为程序和 ¬g 作为属性的模型检查问题。谁能帮我这个？如何将 LTL f 转换为 SPIN/Promela 中的程序？

谢谢。

iSpin (v. 1.1.4) 中的“自动机视图”显示......究竟是什么？它似乎只是一个进程的控制流图。

我将如何获得系统的完整状态空间？

例如，在 Ben-Ari：自旋模型检查器的原理中，我想要图 4.1。或在Overview中，我想要图 1。

目前我正在使用基于pairsR 中命令的脚本来查找给定模型的残差与剩余变量之间的关系。这种关系对于模型诊断可能很重要。您可以在下面查看我的代码，以了解我当前如何绘制关系的一个小示例。

如果我的模型中有很多变量（比如~10），那么pairs图就会变得非常大。我只看pairs图的底行与残差的关系，因此可以大大简化图。任何人都可以推荐一个命令来仅绘制配对图的底行或类似的东西吗？

如果新的绘图方法可以使用网格进行残差分析而不是非常宽的绘图，那就太好了。

来自 dput(gpa) 的输出

我正在尝试在 NuSMV 中将简单的冒泡排序编程为 FSM，但我面临一个主要问题，当我尝试在数组的 2 个元素之间进行交换时，我无法在数组中进行交换，程序停止。任何人都可以帮助解决这个问题吗？非常感谢。