问题标签 [spin]

有没有人接触过这个工具SPIN的模型检查，更任何模型检查的信息（并发程序）

我正在为 Spin 中的算法建模。我有一个有多个渠道的流程，并且在某些时候，我知道一条消息将会到来，但不知道来自哪个渠道。因此，希望等待（阻止）该过程，直到消息来自任何通道。我怎样才能做到这一点？

我正在尝试使用 Spin Model Checker 对两个对象（A 和 B）之间的游戏进行模型检查。对象在板上移动，每个位置由其 (x,y) 坐标定义。这两个物体应该不会碰撞。我有三个进程：init，A Model，B Model。我正在检查一个 ltl 属性的模型：（用于检查两个对象是否曾经占据相同位置的 liveness 属性）

我得到的错误线索是：init -> A Model -> B Model -> init

但是，根据显示的数据，我不应该得到错误线索（反例）：x_a=2，x_b=1，y_a=1，y_b=1。

同样，第一个 init 确实经过了 init 进程的所有行，但第二个只显示到它的最后一行。

此外，我的 A 模型和 B 模型仅由“do”块中的警卫和动作组成，如下所示。但是它们更复杂，并且在“->”右侧有 if 块

我需要在原子块中放入任何东西吗？我问的原因是错误跟踪显示的行甚至没有进入“do”块，它只是两个模型的第一行。

编辑： LTL 属性是错误的。我将其更改为：

但是，我仍然得到完全相同的错误线索。

是否可以从另一个进程访问一个进程的局部变量的值。例如在下面的程序中，我想从经理那里读取 my_id 的值。

我有以下 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 中设置包含路径？