初SPINネタ ②　オプションの使い方が間違っていました。

SPIN #ソフトウェア
初SPINネタの続きです。

前回は
 ./pan -e
としていましたが。。オプションが足りませんでした。。汗）
 ./pan -e -c0
です。
　-eはファイルに書き出すで-c0が全ての反例を出力-cの後ろに数値を入れると数値分の反例を出力
　　　"0"は全てです。

でもこれで実行するとファイルが答えの274を超えてたくさん出力。。汗）
中身を見ると。。重複している物がいっぱい。
だけど反例を１つ出力なら正しく出してくれる。
例→最短経路の反例を出力
 ./pan -i
で実行すると
$ spin -t -p goal5.p
Starting Shot with pid 0
Starting :never: with pid 1
Never claim moves to line 40    [(1)]
  2:    proc  0 (Shot) line  10 "goal5.p" (state 1)     [score = (score+3)]
  4:    proc  0 (Shot) line  10 "goal5.p" (state 2)     [ss = score]
  6:    proc  0 (Shot) line  15 "goal5.p" (state 9)     [((score<10))]
Starting Shot with pid 2
  8:    proc  0 (Shot) line  15 "goal5.p" (state 10)    [(run Shot(score))]
 10:    proc  1 (Shot) line  10 "goal5.p" (state 1)     [score = (score+3)]
 12:    proc  1 (Shot) line  10 "goal5.p" (state 2)     [ss = score]
 14:    proc  1 (Shot) line  15 "goal5.p" (state 9)     [((score<10))]
Starting Shot with pid 3
 16:    proc  1 (Shot) line  15 "goal5.p" (state 10)    [(run Shot(score))]
 18:    proc  2 (Shot) line  10 "goal5.p" (state 1)     [score = (score+3)]
 20:    proc  2 (Shot) line  10 "goal5.p" (state 2)     [ss = score]
 22:    proc  2 (Shot) line  15 "goal5.p" (state 9)     [((score<10))]
Starting Shot with pid 4
 24:    proc  2 (Shot) line  15 "goal5.p" (state 10)    [(run Shot(score))]
 26:    proc  3 (Shot) line  12 "goal5.p" (state 5)     [score = (score+1)]
 28:    proc  3 (Shot) line  12 "goal5.p" (state 6)     [ss = score]
Never claim moves to line 39    [((ss==10))]
Never claim moves to line 43    [(1)]
spin: trail ends after 30 steps
#processes: 4
                ss = 10
 30:    proc  3 (Shot) line  15 "goal5.p" (state 9)
 30:    proc  2 (Shot) line  28 "goal5.p" (state 11) <valid end state>
 30:    proc  1 (Shot) line  28 "goal5.p" (state 11) <valid end state>
 30:    proc  0 (Shot) line  28 "goal5.p" (state 11) <valid end state>
 30:    proc  - (:never:) line  44 "goal5.p" (state 8) <valid end state>
4 processes created
OKです想定通りです！！

もっとも反例をつぶして無くすのが目的のプログラムですから。。
反例を過不足無く出力にこだわってないのかも。。
それとも問題がspin-LTL向きでないのかも？？
SMV-CTLなら正しく答えを出してくれる？？

今日はつかれた。。おしまい。。CTLも勉強してみます。

spin promela モデル検証