问题标签 [spin]

我希望 SPIN 打印出计算的状态空间，以便我可以对其进行可视化，然后手动探索它。那可能吗？

我已经检查了诸如 -DCHECK 和 -DVERBOSE 之类的标志，但我想，这些不是我想要的……

我正在尝试对以下 LTL 属性的简单 Promela 模型进行模型检查：

我得到一个错误，错误线索上的引导模拟产生以下输出：

现在我看不到“M [0]直到M [1]”在这里被违反。M[0] 在初始化过程中被设置为 1，并且一直如此，直到 M[1] 变为 1。并且跟踪结束得这么早，或者我可能完全误解了“stronguntil”的语义。我非常有信心是这种情况......但我做错了什么？在 Promela 文件中指定 LTL 可以吗？

有问题的模型如下（一个简单的 petri 网）：

我阅读了旋转指南，但以下问题没有答案：

我的代码中有一行如下：

其中 Ch 是一个通道，x 是通道类型（接收 MSG） 如果 Ch 为空会发生什么？它会等待味精到达吗？我是否需要先检查 Ch 是否为空？

基本上我想要的是，如果 Ch 是空的，那么等到 MSG 到达，当它到达时继续......

我在 Spin 中编写了一个模型。我想检查模型上的一些 LTL。例如：

在验证窗口中，我选择选项“使用声明”并单击“运行”：

在这一点上，我不知道下一步该做什么......？我试图用谷歌寻找答案，但没有关于如何使用 Spin 的指南......

我是新手。我想检查转换系统是否满足给定的 LTL 属性。但我不知道如何在 promela 中建模过渡系统。例如下图所示的转移系统有两种状态，初始状态为s0。如何检查LTL属性：<>q是否满足。有人知道如何在 promela 中描述这个问题吗？对了，spin中LTL的next算子怎么用？

我似乎太傻了，看不到它。日志显示我的语法错误在哪里（第 12、22 和 25 行），我阅读了一些教程，但找不到错误。

程序很简单，它应该通过一个同步通道计算0和1的数量。

这是我的代码：

还有我的语法错误：

我很乐意给小费..

我想知道是否可以在具有公平约束的程序中验证 LTL 属性，该公平约束表明必须经常无限执行多个语句。

例如：

如果最终no_flip标志变为真并 flag变为真，则该程序是正确的。

但是，同时运行 'pan -a' 和 'pan -a -f' （弱公平）会在no_flip=1语句和接受状态（来自 LTL 公式）之间产生一个循环。

我认为进度标签会强制执行无限频繁地通过它们，但情况似乎并非如此。那么，是否可以添加这种公平约束？

谢谢，努诺

我使用 Spin 创建了一个面包房锁

当我测试它时，我得到一个错误：pan：1：断言违反 - 无效的数组索引（深度 5）

当我跑步时，我得到了这个

谁能告诉我为什么它跳过这一行 (i == n) -> break; ?

我正在尝试在 Promela 中制作 B-Tree，以便我可以证明有关它的内容，但是，Promela 似乎不支持递归数据类型。这不起作用：

如何在 Promela 中制作 B-Tree，如果不能，您会建议使用哪种工具？我考虑过 QuickCheck 和 Prolog。然而，在 Prolog 中制作 B-Tree 也很困难。

是否有全局变量的默认值？或者模型检查器检查所有可能的交错，也就是说，在这种情况下，将所有可能的状态与(x==0)和一起使用(x>0)。