问题标签 [promela]

我似乎太傻了，看不到它。日志显示我的语法错误在哪里（第 12、22 和 25 行），我阅读了一些教程，但找不到错误。

程序很简单，它应该通过一个同步通道计算0和1的数量。

这是我的代码：

还有我的语法错误：

我很乐意给小费..

我想知道是否可以在具有公平约束的程序中验证 LTL 属性，该公平约束表明必须经常无限执行多个语句。

例如：

如果最终no_flip标志变为真并 flag变为真，则该程序是正确的。

但是，同时运行 'pan -a' 和 'pan -a -f' （弱公平）会在no_flip=1语句和接受状态（来自 LTL 公式）之间产生一个循环。

我认为进度标签会强制执行无限频繁地通过它们，但情况似乎并非如此。那么，是否可以添加这种公平约束？

谢谢，努诺

我使用 Spin 创建了一个面包房锁

当我测试它时，我得到一个错误：pan：1：断言违反 - 无效的数组索引（深度 5）

当我跑步时，我得到了这个

谁能告诉我为什么它跳过这一行 (i == n) -> break; ?

上面的代码发送错误“语法错误在'筷子'附近看到'一个标识符'”我如何将数组定义和初始化为原型P（）之外的全局变量感谢您的帮助

有谁知道您是否可以使用（或转换）带有 Sublime Text 的 vim 语法高亮定义文件？

我正在寻找 promela 的荧光笔，只为 vim 找到了一个，但我使用 sublime-text 作为我的默认编辑器

我找到的定义https://github.com/vim-scripts/promela.vim/blob/master/syntax/promela.vim

在这个 promela 模型中，never 声明验证最初并且然后在每个第二时间步 p 成立。为什么？谢谢！

我正在尝试在 Promela 中制作 B-Tree，以便我可以证明有关它的内容，但是，Promela 似乎不支持递归数据类型。这不起作用：

如何在 Promela 中制作 B-Tree，如果不能，您会建议使用哪种工具？我考虑过 QuickCheck 和 Prolog。然而，在 Prolog 中制作 B-Tree 也很困难。

我是 promela 的新手。我有一个用 promela 编写的程序：

有人知道如何为这个程序绘制过渡系统吗？

是否有全局变量的默认值？或者模型检查器检查所有可能的交错，也就是说，在这种情况下，将所有可能的状态与(x==0)和一起使用(x>0)。

对于以下代码，

我收到以下错误，

为什么呢？Promela 不应该为 cond1 的每个值执行（cond1 == 0 和 cond1 != 0）。至少这是这里写的。

在验证期间，不会进行此类调用，因为在此模式下将有效地探索所有行为选项，一次一个。