问题标签 [promela]

我的老师让我们在 Promela 中编写 Dijkstra 的令牌终止算法。这是算法：

“每个节点都维护一个计数器 c。发送消息将 c 加一；收到消息将 c 减一。因此，所有计数器的总和等于网络中未决消息的数量。当节点 0 启动检测探测时，它向节点 N-1 发送一个值为 0 的令牌。每个节点 i 保留令牌直到它变为被动；然后它将令牌转发给节点 i-1，将令牌值增加 c。每个节点和令牌都有一个颜色（最初全白）。当节点收到消息时，节点变为黑色。当节点转发令牌时，节点变为白色。如果黑色机器转发令牌，则令牌变为黑色；否则令牌保持其颜色. 当节点 0 再次收到令牌时，可以结束，如果节点 0 是被动白色，则令牌是白色的，令牌值与 c 之和为 0。否则，节点 0 可能会启动新的探测。”

我有点明白这个想法，但我很难真正理解发生了什么。如果有人可以帮助准确地解释算法正在逐步执行的操作，那就太好了。此外，虽然我不希望任何人为我编写代码，但有关如何开始的任何提示都会有所帮助。

我有一个可以用 Spin 验证的测试 Promela 程序（UI 模型）：

然后我创建了一个相应的 C 程序（第一步，在主窗口中没有循环）：

我想尝试在 Frama-C 和 WP 插件中使用 Aoraï LTL（不想手动创建 .ya）。首先，我创建了一个 .ltl 文件

并且可以获得2个未知目标：

我也试过

结果相同。这个

可以证明，但我相信那个不应该是正确的：

但它是正确的（所有目标都被证明了）。此外，我尝试在 Promela 中测试我的 LTL 公式（没有 CALL/RETURN/X）：

我有很多未经证实的目标，甚至是为了测试

内部错误

我使用命令行

Frama-C 版本是 Phosphorus-20170501。

我应该如何使用这个插件来验证我的 LTL 测试程序？

这将是正确的做法：

在普罗米拉？

我努力了 ：

和

我需要在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？