问题标签 [spin]

我需要在Promela中将一个数组从父进程传递给子进程，但它不允许我这样做。另外，我在使这个数组全局化方面有一些限制，所以也不能这样做。如何才能做到这一点？

例如：

我正在寻找如何在 Windows 10 命令行上使用Spin分析train.pml的输出。

任何帮助使文件提供正确的输出将不胜感激。

我正在尝试在 promela 中为我的项目之一建模以进行模型检查。在那，我在网络中有 N 个节点。因此，对于每个节点，我都在制作一个流程。像这样的东西：

所以，基本上，这里的每个“节点”都是模拟我网络中每个节点的过程。现在，节点进程有 3 个线程，它们在我的原始实现中并行运行，并且在这三个线程中，我在某个部分有锁定，因此三个线程不会同时访问关键部分。所以，在promela中，我做了这样的事情：

所以这里的recv_A、send_B和do_C是在网络中每个节点并行运行的三个线程。现在，问题是，如果我使用 atomic 将锁放入 recv_A、send_B、do_C 中，那么它将对所有 3*N 个进程进行锁定，而我想要一个锁，以便将锁应用于三个一组。也就是说，如果process1的（运行recv_A的主节点进程）recv_A在它的CS中，那么只有process1的send_B和do_C应该被禁止进入CS，而不是process2的recv_A、send_B、do_C。有没有办法做到这一点？

根据手册页，

进度标签用于定义正确性声明。进度标签规定了在任何无限系统执行中必须经常无限访问标记的全局状态的要求。验证者可以将任何违反此要求的行为报告为非进度循环。

和

Spin 有一个特殊的模式来证明不存在非进度循环。它使用预定义的 LTL 公式执行此操作：

它将非进度正式化为标准的 Buchi 接受属性。

但是让我们看一下非常原始的promela规范

据我了解，assert应该保持但验证失败，因为initialised++只执行一次，而progress标签声称应该可以任意频繁地执行它。

然而，即使使用上面的 LTL 公式，这在 ispin 中也可以很好地验证（见下文）。

如何正确测试是否可以经常任意执行语句（例​​如锁定方案）？

（Spin 版本 6.4.7——2017 年 8 月 19 日）

完整的状态空间搜索：

状态向量 28 字节，深度达到 7，错误：0

哈希冲突：0（已解决）

内存使用统计（以兆字节为单位）：

在初始化中未达到

pan：经过时间 0.001 秒

未发现错误——您是否验证了所有声明？

更新

仍然不知道如何使用这个......

让我们为非进展周期选择测试。然后 ispin 将其运行为

验证无误。

因此，让我们尝试使用 ltl 属性...

现在，首先，

好吧，我不在乎，我只想让它最终运行，所以让我们继续progress_writer1担心以后如何将它们拼接在一起：

ispin 运行这个

这不会产生错误，而是报告

是的？灿烂！我完全不知道该怎么做。

我如何让它运行？

好的，所以我试图在 Promela 中模拟一个CLH-RW 锁。

锁的工作方式很简单，真的：

队列由 . 组成，tail读取者和写入者都将一个包含单个节点的节点排入队列，bool succ_must_wait他们通过创建一个新节点并使用tail.

尾部因此成为节点的前任，pred。

然后他们旋转等待pred.succ_must_wait直到它是false。

读者首先增加一个读者计数器ncritR，然后将自己的标志设置为false，允许多个读者同时在临界区。释放一个读锁仅仅意味着ncritR再次递减。

作家等到ncritR达到零，然后进入临界区。false在释放锁之前，它们不会将其标志设置为。

不过，我有点努力在 promela 中建模。

我当前的尝试（见下文）尝试使用数组，其中每个节点基本上由许多数组条目组成。

这失败了，因为让我们说A自己入队，然后B自己入队。然后队列将如下所示：

S哨兵节点在哪里。

现在的问题是，当A运行到完整性并重新入队时，队列看起来像

在实际执行中，这绝对没问题，因为A和A'是不同的节点对象。并且由于A.succ_must_wait将已设置为首次释放false时A的锁，B最终会取得进展，因此A'最终也会取得进展。

但是，在下面的基于数组的 promela 模型中发生的情况是A和A'占据相同的数组位置，导致错过已释放锁B的事实，从而在（错误地）等待而不是等待（正确）对于。ABA'AA'B

对此的一个可能的“解决方案”可能是A等到B确认发布。但这并不适用于锁的工作方式。

另一个“解决方案”是等待一个 CHANGE in pred.succ_must_wait，其中一个 release 会增加succ_must_wait，而不是重置它到0.

但是我打算对锁的一个版本进行建模，其中pred可能会发生变化（即，一个节点可能被允许忽略它的一些前辈），而且我并不完全相信像增加版本这样的东西不会引起问题有了这个变化。

那么在 promela 中对像这样的隐式队列进行建模的“最智能”方法是什么？

我是新手Jspin和Promela。我试图实现以下系统：

家庭警报系统可以使用个人 ID 密钥或密码来激活和停用，激活后系统进入大约 30 秒的等待期，该时间允许用户撤离安全区域，之后警报被布防，即使是在入侵时检测到警报有一个内置的等待时间或延迟 15 秒，以允许入侵者输入密码或刷卡钥匙从而识别自己，如果在分配的 15 秒内未进行识别，警报将响起并将一直打开，直到使用身份证或密码将其停用。

这是代码：

当我运行代码时，Jspin我收到以下消息：

但我在标题中声明了这一点。

我该如何解决这个问题？

根据我必须使用jSpin和promela语言实现的问题，我需要一些帮助。

家庭警报系统可以使用个人 ID 密钥或密码来激活和停用，激活后系统进入大约 30 秒的等待期，该时间允许用户撤离安全区域，之后警报被布防，即使是在入侵时检测到警报有一个内置的等待时间或延迟 15 秒，以允许入侵者输入密码或刷卡钥匙从而识别自己，如果在分配的 15 秒内未进行识别，警报将响起并将一直打开，直到使用身份证或密码将其停用。

这是我尝试过的：

在user proctype中我发送密码

如何验证密码是否1234正确，如何根据验证使其适应自己的情况（on、、、off）pending？

我正在构建一个 Promela 模型，其中一个进程向 N 个其他进程发送请求，等待回复，然后计算一个值。基本上是典型的 map-reduce 风格的执行流程。目前我的模型以固定的顺序发送请求。我想将其概括为发送不确定的订单。我已经查看了该select声明，但这似乎不确定地选择了单个元素。

有没有一个很好的模式来实现这一点？这是我正在使用的基本结构：

msgtype这是一个对象进程，它用它计算的一些值来响应消息。

这是客户端。它按顺序向每个对象发送请求0, 1, 2, ...，并收集所有响应并减少值。

我像这样启动系统

在 Promela 中设计模型时，当发送许多不同类型的消息时，通道的设计权衡是什么？

文档中的许多示例都使用类似这样的简单案例

然而，在实践中，一些模型可能具有处理各种不同消息类型的进程，每个消息类型都有一组独特的参数。

所以通道之间似乎有一个设计决策，可以表示各种消息类型的参数：

以及特定于每种消息类型的通道

我有兴趣了解一种设计相对于另一种设计的任何性能优势，以及什么被认为是最佳实践。

我刚接触 Promela，尤其是 SPIN。我有一个模型，我正在尝试验证，但无法理解 SPIN 的输出来解决问题。

这是我所做的：

输出如下：

然后我再次运行 SPIN 以尝试通过检查跟踪文件来确定问题的原因。我使用了这个命令：

结果是这样的：

根据此输出（据我了解），在“init”过程中验证失败。untitled.pml 中的相关代码是这样的：

在这一点上，我不知道是什么导致了问题，因为对我来说，“do”语句应该执行得很好。

谁能帮助我理解 SPIN 输出，以便我可以在验证过程中消除此错误？该模型确实产生了正确的输出以供参考。