问题标签 [promela]

我试图通过使用 -DMEMLIMIT 标志来限制 PROMELA 使用的最大内存，就像这样。

但是，内存仍在不断增加。任何想法，为什么会这样？

我正在寻找为多核处理器建模缓存，包括缓存一致性。这样的 PROMELA 实现是否已经存在。我试图搜索它，但找不到任何东西。其次，如果我必须自己实现它，在 PROMELA 中声明非常大的数组来表示缓存结构是否可行？

所以我想要的是进程 A 广播一条消息，说进程 B 到 D。这怎么做？这样做的正确方法似乎是在 A 和进程 B 到 D 之间建立通道，然后将相同的消息发送到从 B 到 D 的每个进程，如下所示。

这是在 PROMELA 中模仿广播的正确方法，还是有合适的操作员这样做？

以下是导致此问题的代码。

如果我在第一个条件下删除了nempty调用，错误就消失了。根据我的阅读，如果在条件中使用接收或发送语句，则不能使用 else 语句，但据我所知，nempty不是发送或接收语句，而只是检查通道是否不是空的。那么，我在做什么错误，我该如何解决这个问题。

下面的算法试图在两个进程 P1 和 P2 之间强制互斥，每个进程都运行下面的代码。您可以假设最初 sema = 0。

如何在 promela/SPIN 中建模此代码？

谢谢你。

对不起我的英语，我来自乌克兰）才开始研究旋转系统验证。我们问了以下问题：“用LTL表达式下面的形式呈现：如果我爱玛莎，我就不能爱达莎”。我不明白该怎么做。下面是我得到的： p - 就像玛莎得到的 Gp，用 [] p 代码的形式表示（虽然我不知道怎么写）：

我知道这是胡说八道，但我请求您的帮助。

我是尝试使用 Promela 和 SPIN 的初学者。在开发一些简单的 Promela 规范时，我想使用 printf() 检查程序中变量的值。我已阅读此手册页并尝试运行一个简单的 hello world 程序，但我没有看到任何输出文本。这是示例 hello world 文件：

我用来编译和运行的步骤是

运行的输出是

那么，我在哪里可以找到 printf 语句的输出？我也在更复杂的 promela 文件中尝试了 printf 语句，但显然我想让它首先适用于简单的情况。任何见解将不胜感激。谢谢！

我学习了 Promela 和 Spin，但是当我尝试验证模型时，这些行会返回给我。

他们的意思是什么？

谢谢

如果数组的所有值都相等，您如何检查 Promela？

如果它们是，我希望这段代码是原子的和可执行的（忙于等待，直到所有都相等）。

有没有办法使用 for 循环？（数组的长度作为参数给出）

所以我在我的 Promela 代码中使用了以下行。

但是，它正在引起状态爆炸。我用以下if语句替换它，突然状态爆炸问题消失了。我上面显示的语句不select应该等同于if下面的语句吗？这里发生了什么？