文章/答案/技术大牛

发布

社区首页 >问答首页 >使用SPIN tool验证LTL的步骤是什么？

问使用SPIN tool验证LTL的步骤是什么？
EN

Stack Overflow用户

提问于 2013-06-20 15:03:24

回答 2查看 3.7K关注 0票数 4

我用Spin写了一个模型。我想检查一下模型上的LTL。例如：

ltl L1 {<>[]Working}

在验证窗口中，我选择"use claim“选项，然后单击"Run"：

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

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

spin

promela

回答 2

Stack Overflow用户

发布于 2013-06-20 17:01:07

在foo.pml
spin -a foo.pml
gcc -o foo.exe pan.c (Windows)
foo.exe -a

中保存模型，包括ltl-block

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

票数 3

Stack Overflow用户

发布于 2013-06-21 00:37:37

在单击“运行”之后的“验证”窗口中，应该会有一个验证结果。它看起来像这样(例如)：

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?

你什么都没看到吗？或者你看到了什么，但无法解释它？

票数 1

页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持

原文链接：

https://stackoverflow.com/questions/17207250

复制

相似问题

问使用SPIN tool验证LTL的步骤是什么？
EN

回答 2

Stack Overflow用户

Stack Overflow用户

社区

活动

圈层

关于

腾讯云开发者

热门产品

热门推荐

更多推荐

问使用SPIN tool验证LTL的步骤是什么？EN

回答 2

Stack Overflow用户

Stack Overflow用户

社区

活动

圈层

关于

腾讯云开发者

热门产品

热门推荐

更多推荐

问使用SPIN tool验证LTL的步骤是什么？
EN