如何使用 Spin 从命令行检查 Promela 代码 [关闭]答案

【问题标题】：How to use Spin to check Promela code from the command line [closed]如何使用 Spin 从命令行检查 Promela 代码 [关闭]
【发布时间】：2017-10-19 12:31:30
【问题描述】：

我正在研究如何在 Windows 10 命令行中使用 Spin 分析 train.pml 的输出。

任何帮助使文件给出正确的输出将不胜感激。

【问题讨论】：

输出是什么？什么是正确的输出？请查看有关在 SO 上提问的一些项目。 stackoverflow.com/help/asking
@lit 我不知道它应该是什么。除了错误，我似乎无法得到任何输出。我不确定如何正确运行该文件。谢谢。
当您的源代码不工作时，可以使用 SO。 SO 不是介绍性教程的地方。
这对我的问题没有帮助。
你是对的。这无济于事，因为 SO 不适合此类问题。您希望有人在 Google 上搜索 spin 和 train.pml 吗？

标签： logic model-checking promela spin

【解决方案1】：

先决条件：获得一个在 Windows 10 上使用 gcc 的工作环境（例如参见these instructions），或者，获得一个虚拟环境 em> 带有一些 GNU/Linux 发行版。另外，correctly install Spin 在目标系统中。

只有两种可能的方法：

选项A.：

~$ spin -a train.pml
~$ gcc pan.c -o verifier
~$ ./verifier -a -N c1
...
~$ ./verifier -a -N c8
...

选项B.：

~$ spin -search -ltl c1 train.pml
...
~$ spin -search -ltl c8 train.pml
...

目前，属性c1, c5, c7, c8 在您的模型上已验证，而c2, c3, c4, c6 则未验证。还有一些关于未达到的最终状态的投诉。请检查后一种情况是否不违反您的系统规范（可能有问题也可能没有问题），并且验证的结果是否符合您的预期。

作为参考，这是验证属性c1时应获得的正确输出示例：

~$ spin -search -a -ltl c1 trail.pml
...
pan: ltl formula c1

(Spin Version 6.4.6 -- 2 December 2016)
    + Partial Order Reduction

Full statespace search for:
    never claim             + (c1)
    assertion violations    + (if within scope of claim)
    acceptance   cycles     + (fairness disabled)
    invalid end states  - (disabled by never claim)

State-vector 152 byte, depth reached 4508, errors: 0
    67919 states, stored (97586 visited)
   170919 states, matched
   268505 transitions (= visited+matched)
        0 atomic steps
hash conflicts:       184 (resolved)

Stats on memory usage (in Megabytes):
   11.659   equivalent memory usage for states (stored*(State-vector + overhead))
    5.455   actual memory usage for states (compression: 46.78%)
            state-vector as stored = 56 byte + 28 byte overhead
  128.000   memory used for hash table (-w24)
    0.534   memory used for DFS stack (-m10000)
  133.905   total actual memory usage


unreached in proctype train
    trail.pml:31, state 14, "-end-"
    (1 of 14 states)
unreached in proctype gate
    trail.pml:52, state 17, "-end-"
    (1 of 17 states)
unreached in proctype queue
    trail.pml:74, state 17, "-end-"
    (1 of 17 states)
unreached in claim c1
    _spin_nvr.tmp:10, state 13, "-end-"
    (1 of 13 states)

pan: elapsed time 0.12 seconds
pan: rate 813216.67 states/second

【讨论】：

太棒了！非常感谢帕特里克。
@PatrickTrentin “虚拟环境”是什么意思？因为它只是 C 代码，所以 Spin 在 Linux 上不是原生的吗？
@MaxvonHippel 问题是针对 windows 的
我的错，谢谢你的澄清。