spin - 用自旋工具验证LTL的步骤?

  显示原文与译文双语对照的内容
0 0

我在旋转中写了个模型。 我想看看模型上的LTL 。 例如:


ltl L1 {<>[]Working}

在验证窗口中,选择选项"使用声明",然后单击"跑步":


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

现在我不知道下一步该做什么。 我试图用谷歌寻找答案,但没有指南如何使用旋转。

时间: 原作者:

0 0
  1. 保存你的模型,包括 foo.pml 中的ltl -block

  2. spin -a foo.pml

  3. gcc -o foo.exe pan.c ( Windows )

  4. foo.exe -a

使用 -a 运行可执行文件是密钥,否则将不检查ltl属性。

原作者:
0 0

在'验证'窗口中单击'跑步'之后,应该有一个验证结果。 它看起来像这个( 例如):


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?

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

原作者:
...