4

我在 Spin 中编写了一个模型。我想检查模型上的一些 LTL。例如：

ltl L1 {<>[]Working}

在验证窗口中，我选择选项“使用声明”并单击“运行”：

ltl L1: <> ([] (Working))
gcc -DMEMLIM=1024 -O2 -DXUSAFE -w -o pan pan.c

在这一点上，我不知道下一步该做什么......？我试图用谷歌寻找答案，但没有关于如何使用 Spin 的指南......

4

2 回答 2

3

  1. 保存您的模型，包括ltl-blockfoo.pml

  2. spin -a foo.pml

  3. gcc -o foo.exe pan.c（视窗）

  4. foo.exe -a

运行可执行文件-a是关键，否则将不会检查 LTL 属性。

于 2013-06-20T09:01:06.690 回答
1

在您点击“运行”后的“验证”窗口中应该有一个验证结果。它看起来像这样（例如）：

verification result:
spin -a  foo.pml
ltl ltl_0: [] (foo)
gcc -DMEMLIM=1024 -O2 -DXUSAFE -o pan pan.c
./pan -m10000  -a -c1
Pid: 21462

(Spin Version 6.2.4 -- 21 November 2012)
    + Partial Order Reduction
...

pan: elapsed time 0 seconds
No errors found -- did you verify all claims?

你没有看到这些吗？还是您看到了什么但无法解释？

于 2013-06-20T16:37:37.160 回答