初SPINネタ �� 補集合ですか。。汗）
|
SPINを業務へ使用してみたくなったので、SPIN初ネタを見直した。 |
SPIN
[ リスト | 詳細 ]
全1ページ
[1]
コメント（0）
初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 モデル検証
|
初SPINネタ
|
SPINネタで良いのが無いか探していたら。。 「ビートたけしのコマ大数学科」を扱ったweb http://gascon.cocolog-nifty.com/blog/2009/01/index.html があり、１１９講：バスケットボールを解いてみることにした。 問題：バスケットボールの得点は、フリースローが1点、スリーポイントラインの内側からだと2点、外側からだと3点入る。ちょうど得点が10点になるまでの得点経過は何通りあるか？ （上記webより引用） SPINでの解き方は。。 promelaでシュートを打つ過程をプログラムし １０点にならない事を証明させる。 この時、証明は失敗し”反例”を出してくるの、それを数える。 promelaのコードはこれだ byte ss = 0 ;
init {run Shot(0);}
proctype Shot(byte score)
{
if
:: score = score +1 -> ss = score
:: score = score +2 -> ss = score
:: score = score +3 -> ss = score
fi;
if
::(score < 10) -> run Shot(score)
:: else goto end
fi;
end:
printf("score_total = %d", ss) -> skip
}
#define p (ss==10)
never { /* <>p */
T0_init:
if
:: ((p)) -> goto accept_all
:: (1) -> goto T0_init
fi;
accept_all:
skip
}
最初のif文でシュートが入ったときの得点(1-3)が非決定的に選択され scoreに足し込まれる。 次のif文で10点未満なら、再びシュートを打つ(run Shot(score)）。 10点以上なら終了(goto end)。 証明文は、コマンドラインより下記のコードを打ち込み[RET] spin -f '<>p'でコードを出力し #define p (ss==10)を追加する。 →注意。。promela文中のscoreはrun Shot(score)と再帰呼び出しているので、scoreで有ってscore でない！！名前は同じだが実態は別変数だよ。 従って、グローバル変数byte ssを作ってscore値を逐次代入し証明に使用する。 これが#define p (ss==10)だ。 作ったpromela文をshot.pとしてセーブ。。コンパイル。。実行。 spin -a shot.p gcc -o pan pan.c ./pan 結果 $ ./pan
warning: never claim + accept labels requires -a flag to fully verify
hint: this search is more efficient if pan.c is compiled -DSAFETY
warning: for p.o. reduction to be valid the never claim must be stutter-invariant
(never claims generated from LTL formulae are stutter-invariant)
pan: claim violated! (at depth 81)
pan: wrote Shot.p.trail
(Spin Version 5.1.6 -- 9 May 2008)
Warning: Search not completed
+ Partial Order Reduction
Full statespace search for:
never claim +
assertion violations + (if within scope of claim)
acceptance cycles - (not selected)
invalid end states - (disabled by never claim)
State-vector 60 byte, depth reached 81, errors: 1
41 states, stored
0 states, matched
41 transitions (= stored+matched)
0 atomic steps
hash conflicts: 0 (resolved)
2.501 memory usage (Mbyte)
pan: elapsed time 0.046 seconds
pan: rate 891.30435 states/second
State-vector 60 byte, depth reached 81, errors: 1と反例が出てきたので spin -t -p shot.pとして反例を見てみる。 ---- 略 ----
78: proc 10 (Shot) line 10 "Shot.p" (state 2) [ss = score]
Never claim moves to line 33 [((ss==10))]
80: proc 10 (Shot) line 17 "Shot.p" (state 11) [else]
Never claim moves to line 37 [(1)]
spin: trail ends after 81 steps
#processes: 11
ss = 10
---- 略 ------
ss=10が出てきた。次にpanへオプション-eを付けて実行。 →オプション”-e”は全ての不具合をtrailファイルに出力する。 ./pan -e結果は State-vector 60 byte, depth reached 81, errors: 1オプション -eを付けないときと同じ。。なんで？？ 証明文を付けないで実行すると。。 unreached in proctype Shot
(0 of 17 states)
なんて出てきた。。どうやら無限に探索空間があって途中終了となっている見たい。byte score byte ssで状態空間を8+8=16bitに制限したつもりだけど。。 16bit範囲を探索して終了。。 変数は可算無限として扱われる見たい。 変数の幅は探索幅制限で使用されるのか。。 つかれた。。今日はおしまい。 SPIN 回路検証 システム検証
|
全1ページ
[1]
