问题标签 [promela]

我有以下 promela 代码：

我期望将级别（0-9）信息发送到通道中，并根据该级别使传感器输出低|正常|高。它很简单。但是为什么 SPIN 一直说超时呢？

它似乎只做 1 次循环，为什么？

我希望能够使用 for 循环来遍历 typedef 值的数组，如下所示：

自旋给出以下错误：

是否可以使用这种形式的 for 循环来遍历数组，而不必使用带有索引指针的 for 循环？

我正在尝试重现 Dijkstra 在题为“协作顺序进程”的论文中编写的 ALGOL 60 代码，该代码是解决互斥锁问题的第一次尝试，语法如下：

所以我试图在 Promela 中重现上面的代码，这是我的代码：

我要做的是，验证公平属性永远不会成立，因为标签 L1 无限运行。

这里的问题是我的 never claim 块没有产生任何错误，我得到的输出只是说我的语句从未到达..

这是 iSpin 的实际输出

我已经阅读了有关never{..}块旋转的所有文档，但找不到我的答案（这里是链接），我也尝试过使用ltl{..}块（链接）但这只是给了我语法错误，即使它明确在文档中提到它可以在initand之外proctypes，有人可以帮我更正这段代码吗？

谢谢

当我尝试使用 ispin 验证模型时，我收到“long long long is too long for gcc”的错误消息。我的 gcc 有问题吗？

如果有人可以向我解释为什么我会使用以下代码超时，那就太好了。我理解，或者至少我认为我理解，超时的想法，但是使用 do 循环我认为这会阻止这种情况。任何建议表示赞赏。

我正在使用 jspin 并尝试在 c_code 表达式中包含 stdio.h 库：

但是，我收到以下错误：

我检查了安装 mingw 的目录，里面有 stdio.h。因此，我想，这都是关于错误的道路。如何在 jspin 中设置包含路径？

我希望 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 的指南......