问题标签 [promela]

我正在研究一个相当简单的 promela 模型。使用两个不同的模块，它充当人行横道/交通灯。第一个模块是输出当前信号（绿色、红色、黄色、待定）的交通灯。该模块还接收一个称为“行人”的信号作为输入，该信号用作指示有行人想要穿过的信号。第二个模块充当人行横道。它接收来自交通灯模块的输出信号（绿色、黄色、绿色）。它将行人信号输出到交通灯模块。该模块仅定义行人是否正在过马路、等待或不存在。我的问题是，一旦计数值达到 60，就会发生超时。我相信声明“SigG_out！1”会导致错误，但我不知道为什么。我附上了从命令行收到的跟踪图像。我对 Spin 和 Promela 完全陌生，所以我不确定如何使用跟踪中的信息在代码中找到我的问题。任何帮助是极大的赞赏。

这是完整模型的代码：

对于使用永不声明的验证（使用 ispin），我得到depth reached的输出大于状态数和转换数，例如：

我觉得这有点不直观。某处是否有“深度达到”语义的精确描述（比pan 的输出格式描述更彻底）？或许的意义

最长的深度优先搜索路径包含 87 个转换

不是指 51 个转移，而是指由永不主张组成的系统自动机的转移？

我试图弄清楚 SPIN 如何在以下示例中选择执行和终止进程的顺序。我意识到 SPIN 的主要焦点是分析并发进程，但出于我的目的，我只对简单的线性执行感兴趣。在下面的示例中，我只希望 step1() 然后 step2() 以该顺序执行。

但是，即使使用原子 {} 声明，进程在执行时也会交错。使用命令spin -p my_pml_code.pml我只得到以下 3 个输出（我运行了很多次，这些是唯一的输出）。

运行 1：

顺序是 proc 0 -> 0 -> 0 -> 0 ->2 -> 1 -> 2 -> 1 -> 0

运行 2：

顺序是 proc 0 -> 0 -> 0 -> 0 -> 1 -> 2 -> 2 -> 1 -> 0

运行 3：

顺序是 proc 0 -> 0 -> 0 -> 0 ->2 -> 2 -> 1 -> 1 -> 0

我试图简单地得到它的输出： proc 0 -> 0 -> 0 -> 0 ->1 -> 1 -> 2 -> 2 -> 0

我意识到 proc 0 在 1 和 2 终止之前无法终止，但是为什么 2 和 1 的终止是不确定的交错的？当 init 函数是原子的并且因此应该按顺序执行时，为什么 SPIN 在执行 proc 1 和 proc 2 之间随机选择？为什么我可以让 proc 2 在 proc 1 之前启动和终止（在 Run 3 中），而不是相反？

注意：我也使用dstep代替测试了这个atomic，我得到了相同的结果。

我正在尝试定义一个在 SPIN 中使用 ne(X)t 运算符的 ltl 公式。我的问题与这个问题非常相似。我有一个状态机，我想验证如果某个语句p在 state0 中为真，那么某个语句q在下一个状态 state1 中为真。ltl 公式如下所示：

ltl p0 {p X q}

当我尝试使用生成验证程序时spin -a test.pml，出现以下错误：

spin: test.pml:20, Error: syntax error saw 'X'

我用 -DNXT 标志编译了 SPIN（正如这个建议的那样）。我知道 ne(X)t 运算符无法在启用部分降阶的情况下进行测试。我发现禁用部分降阶的唯一方法是在编译验证器时使用 -DNOREDUCE 标志。但是，我什至无法首先生成验证程序（pan.c）。

我在看 SPIN 软件。我想用它来寻找 LTL 理论的模型。所有的手册和教程都在讨论验证算法的属性，但我对此一点也不感兴趣。我只是想找到 LTL 公式的模型（我想是相应的 Büchi 自动机），就像 mace4 或悖论模型检查器可以找到 FOL 公式的模型一样。我相信 SPIN 应该能够做到这一点，但我无法在文档中找到如何做到这一点。有人可以指出任何有用的资源吗？

我会在spinroot 错误报告中发布此内容，但 spinroot 论坛目前不接受新用户...如果负责该内容的人正在阅读此内容，请让我进来 :)

当我尝试使用 select 语句时，发生了一些非常奇怪的事情。Promela 不允许select()在结构的字段上调用，所以我必须像这样创建一个临时变量：

这运行良好。我对其进行了测试，并struct.someField正确设置为 -1、0 或 1。但是，当我尝试将内联代码直接放入init()进程时，出现语法错误。代码如下所示：

错误信息是：

spin: select_test.pml:9, Error: syntax error saw ''-' = 45'

我有许多 LTL 公式，我试图在同一个 .pml 文件上进行测试。我的问题是，当在任何单个 ltl 公式中发现错误时，跟踪文件将被写入（或覆盖）相同的跟踪文件名。我一直无法找到写入我选择的跟踪文件名的方法。有谁知道这个选项是否存在？

如果不是，我可以使用什么策略同时测试来自同一个 .pml 文件的多个 ltl 公式，而不会每次都覆盖同一个跟踪文件？

我知道 SPIN 运行时 -x 选项，但这只是防止跟踪文件被覆盖。它不会生成具有不同名称的跟踪文件。

我试图了解如何在 ltl 公式中正确使用直到运算符。我发现这个定义（如下）很清楚：

直到_

A U B：如果存在 i 则为真：

• B 在 [s _i , s _i+1 , s _i+2 , ... ]中为真

• 对于所有满足 0 ≤ j < i 的 j，公式 A 在 [s _j , s _j+1 , s _j+2 , ... ]中为真

意义：

• B 在时间 i 为真

• 对于 0 和 i-1 之间的时间，公式 A 为真

仍然使用“在时间 i 时为真”的形式化

带有示例 ltl 公式的示例代码：

根据我给出的 until 运算符的定义，我不明白上述 ltl 公式如何没有产生任何错误。state == Reverse直到所有时间都不需要是真的state != Reverse吗？最初state == Regular.

下面是运行测试后的 SPIN 输出：

首先，我总是遇到这个深度问题：0。我尝试了每一种可能性。其次，我想达到 ltl 公式中提到的那些状态。那么这种语法是否正确？

我开始使用 Promela，但在表达一些 LTL 公式时遇到了麻烦。

一个例子是sequence我想断言的以下值是单调递增的。直观地说，我想在下一个状态中写下， sequence >= its previous value，但是查看文档，我看不到表达这一点的方法。有没有表达这种公式的方法？

假设可以表达sequence上面的单调递增属性，我想知道是否有通配符数组索引的语法。与上面的示例类似，我直观地想引用所有以前的索引条目。

非常感谢你的帮助。Promela 看起来真的很棒:)