问题标签 [promela]

考虑这个片段：

您希望这可以任意打印漂亮的值 0..3，直到计数器低于 0，此时它可以打印另一个数字，也可以终止。

然而，情况似乎并非如此。

返回的唯一值是 0，然后是 1，然后是 0，然后是 1，然后是 0，然后是 1，...

我是否以某种方式误解了 if/fi 语句的“非确定性”？

（如果重要的话，在 ubuntu 上使用 ispin）。

考虑这个简单的 PROMELA 模型：

我想用这个简单的声明来验证这个模型，它是使用 spin -f 生成的：

但是，使用验证

没有结果。尝试 -a 选项也不会产生结果。任何随机模拟都表明，在某些时候显然 p 是错误的，那么尽管我用自旋生成了它，为什么 never 声明不起作用？

我错过了一些基本的东西吗？

我正在使用 Windows 操作系统并在 Cygwin 中输入：wish -f ispin.tcl打开 ispin 界面。我打开一个文件test.pml，其中包含：

之后，我使用种子 = 123 的随机方式运行它。结果打印在输出中没有问题：

当我尝试验证此模型时出现问题。验证结果为：

我该如何解决这个问题？我在互联网上搜索，但找不到可以帮助我的东西。

注意：我没有更改任何验证属性：

我正在学习 Spin Modal Checker 的 promela 语法。我遇到了这段简单的代码。

据我所知，分号用于定义语句的结尾。我可以;在count++andcount--和 after的末尾使用吗fi？它会改变程序的行为方式吗？我会很感激为我清除这个分号的东西。

我用谷歌搜索了一段时间，发现一些论文提出了 CTL 或 CTL* 模型检查 SPIN。但是，根据 Promela 手册页，没有办法在 Promela 模型中表达 CTL。现在只是提案级别吗？

如何在 PROMELA 中将 LTL 转换为 Automata？我知道使用命令 SPIN -f "ltl x" 可以将 LTL 转换为从不声明，但我想要 LTL 的自动机而不是否定的自动机。如果我之前否定 LTL 以生成从不声明，这是正确的。谁能帮我？

是否可以使用 Spin 获得多个（或全部）违规跟踪？

例如，我在下面创建了 Promela 模型：

它有一个简单的互斥锁实现。可以预期进程 A 和 B 不会一起到达它们的临界区，我编写了一个 LTL 表达式来检查这一点。

跑步

表明该属性无效且正在运行

显示违反该属性的语句序列。

这表明语句序列（由标签指示）'B1' -> 'A1' -> 'B2' -> 'A2' 违反了该属性，但还有其他交错选项导致该属性（例如 'A1' -> ' B1'->'B2'->'A2'）。

我可以要求 Spin 给我多条（或全部）痕迹吗？

以下是我正在编写的 Promela 代码。

但是，如果我尝试模拟代码，则会收到如下错误消息，

锯：'['，预期'：'旋转：osek_sp2.pml：507，错误：期望选择（名称：常量..常量）靠近'选择'

但是，根据语法定义，我找不到任何问题。

语法
select '(' varref ':' expr '..' expr ')'

varref : 名称 [ '[' any_expr ']' ] [ '.' 变量引用]

此错误消息的原因是什么？

我对 SPIN 和 Promela 还很陌生，当我尝试验证模型中的 liveness 属性时遇到了这个错误。

错误代码：

该代码基本上是彼得森算法的实现，我检查了安全性，它似乎是有效的。但是，每当我尝试使用 ltl {[]((wait -> <> (cs)))} 验证 liveness 属性时，都会出现上述错误。我不确定他们的意思，所以我不知道如何继续......

我的代码如下：

似乎 Promela 初始化了每个变量（默认为 0，或声明中给出的值）。

如何声明由未知值初始化的变量？

文档建议if :: p = 0 :: p = 1 fi但我认为它不起作用：Spin 仍然验证此声明

（并伪造p）

那么 的语义究竟是什么init？还有一些“预初始”状态？我怎样才能解决这个问题 - 而不是让我的学生感到困惑？