spin - 使用 SPIN 工具验证 LTL 的步骤是什么？

Question

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

ltl L1 {<>[]Working}

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

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

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

Answer 1

保存您的模型，包括 ltl -阻止 foo.pml

spin -a foo.pml

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

foo.exe -a

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