问题标签 [promela]

我想知道如何编写代表 proctype 的所有实例的 never 声明。例如，如果我有以下命题：

现在，如果我实例化 5 个实例，camera_node我如何创建一个原子命题检查start_publishing所有这 5 个实例是否等于零？

我正在尝试习惯 iSpin/Promela。我在用：

Spin 版本 6.4.3——2014 年 12 月 16 日，iSpin 版本 1.1.4——2014 年 11 月 27 日，TclTk 版本 8.6/8.6，Windows 8.1。

这是我尝试使用 LTL 的示例。如果 for 循环中的两个步骤不是原子的，则 LTL 属性的验证会产生错误：

在验证点击中，我只想测试 LTL 属性，所以我禁用所有安全属性并激活“使用声明”。声明名称为“alwaysten”。

但是，如果我激活“断言违规”，似乎只是评估了 LTL 属性。为什么？一位同事正在使用 iSpin v1.1.0，他不需要激活它？我究竟做错了什么？我想独立地证明断言和 LTL 属性......

这是跟踪：

我正在尝试修复我的代码，我已经解决了死锁和互斥问题，但我不知道如何避免饥饿，因为在 promela (PML) 中没有监视器。有人能帮我吗？提前致谢

如何比较两个 LTL 以查看其中一个是否相互矛盾？我问这个是因为我有一个分层状态机和描述每个状态行为的 LTL。我需要知道本地 LTL 是否可以与全局 LTL 相矛盾。我在文章“特征规范和自动冲突检测”中看到，如果 L(f) 交集 L(g) 为空，则两个 LTL 属性 f 和 g 不一致。这正是以 f 作为程序和 ¬g 作为属性的模型检查问题。谁能帮我这个？如何将 LTL f 转换为 SPIN/Promela 中的程序？

谢谢。

iSpin (v. 1.1.4) 中的“自动机视图”显示......究竟是什么？它似乎只是一个进程的控制流图。

我将如何获得系统的完整状态空间？

例如，在 Ben-Ari：自旋模型检查器的原理中，我想要图 4.1。或在Overview中，我想要图 1。

当我尝试运行我的 promela 代码时，我收到一个语法错误，错误显示 Error: syntax error saw 'token: ::'

这是指这行代码（第 10-13 行）：

我试图在 if 和 fi 之后添加一个分号，但错误似乎并没有消失。

有人有想法么？

如何以非原子方式在 Promela 中对布尔 AND 评估进行建模？

我想为语句建模while (flag[j] == true && victim == i)应该以非原子方式进行 AND 评估的语句进行建模。

这怎么可能？

我编写了 Promela 代码来使用 SPIN 验证 Needham-Schroeder 协议。运行代码的随机模拟后，我收到以下输出：

我可以看到为发起者、响应者和入侵者创建的进程。即使我了解其背后的理论，我也很难确切地看出这如何证明 Needham-Schroeder 协议可以被破坏。

任何人都可以理解这个输出并可能将我引导到我应该寻找的地方吗？ 如果您想查看我的 Promela 代码，请告诉我！ 任何反馈表示赞赏！

uppaal 和 spin/promela 对嵌入式系统建模的优缺点是什么？

我有点困惑-谢谢

在尝试比较我的结构的一个属性（不是第一个属性）时，我遇到了 promela 语言的问题。

这是一个例子：

问题很简单：我只想比较content属性。不是前一个（header）。我尝试了一些语法，看看语法（http://spinroot.com/spin/Man/grammar.html#recv_args ...顺便说一句，我不是专家）。但我仍然坚持这个问题。

我使用 ispin 来模拟和测试。

任何帮助都会很棒。

谢谢！