4

Spin でモデルを書きました。モデルの LTL を確認したい。例えば：

ltl L1 {<>[]Working}

[検証] ウィンドウで、[クレームを使用] オプションを選択し、[実行] をクリックします。

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

この時点で、私は次に何をすべきかわかりません...？Google で答えを探してみましたが、Spin の使用方法に関するガイドはありません....

4

2 に答える 2

3

  1. ltl-blockを含むモデルを保存しますfoo.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 に答える