问题标签 [spin]

我在 ispin 中建模了一个系统，当尝试使用 LTL 公式验证系统时，我发现了无法访问的错误，例如

我的 ltl 公式是

我在活动中间有一个图像视图，我将如何使它无休止地旋转 360 度？

如何比较两个 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 代码来使用 SPIN 验证 Needham-Schroeder 协议。运行代码的随机模拟后，我收到以下输出：

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

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

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

我有点困惑-谢谢

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

这是一个例子：

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

我使用 ispin 来模拟和测试。

任何帮助都会很棒。

谢谢！

考虑这个片段：

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

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

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

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

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

考虑这个简单的 PROMELA 模型：

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

但是，使用验证

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

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