SPINネタで良いのが無いか探していたら。。
「ビートたけしのコマ大数学科」を扱ったweb
http://gascon.cocolog-nifty.com/blog/2009/01/index.html
があり、１１９講：バスケットボールを解いてみることにした。
http://gascon.cocolog-nifty.com/blog/2009/01/index.html
があり、１１９講：バスケットボールを解いてみることにした。
SPINでの解き方は。。
promelaでシュートを打つ過程をプログラムし
１０点にならない事を証明させる。
この時、証明は失敗し”反例”を出してくるの、それを数える。
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)。
scoreに足し込まれる。
次のif文で10点未満なら、再びシュートを打つ(run Shot(score)）。
10点以上なら終了(goto end)。
証明文は、コマンドラインより下記のコードを打ち込み[RET]
→注意。。promela文中のscoreはrun Shot(score)と再帰呼び出しているので、scoreで有ってscore
でない！！名前は同じだが実態は別変数だよ。
従って、グローバル変数byte ssを作ってscore値を逐次代入し証明に使用する。
これが#define p (ss==10)だ。
spin -f '<>p'でコードを出力し
#define p (ss==10)を追加する。
→注意。。promela文中のscoreはrun Shot(score)と再帰呼び出しているので、scoreで有ってscore
でない！！名前は同じだが実態は別変数だよ。
従って、グローバル変数byte ssを作ってscore値を逐次代入し証明に使用する。
これが#define p (ss==10)だ。
結果
$ ./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を付けないときと同じ。。なんで？？
証明文を付けないで実行すると。。
16bit範囲を探索して終了。。
unreached in proctype Shot
(0 of 17 states)
なんて出てきた。。どうやら無限に探索空間があって途中終了となっている見たい。byte score byte ssで状態空間を8+8=16bitに制限したつもりだけど。。
16bit範囲を探索して終了。。
変数は可算無限として扱われる見たい。 変数の幅は探索幅制限で使用されるのか。。
つかれた。。今日はおしまい。
SPIN 回路検証 システム検証
