2007-07-10 [長年日記]
λ. ヘッダにしかない関数
mkmf.rb を濫用して調べてみる([ruby-dev:31176])。 ささださんが「他にも、いろいろあるようですね」と言っていたが、本当に色々あるなw
λ. 油売り算
キミならどう書く 2.0 - 2007 - その 1。 どうせHaskellプログラムとかは誰か書くだろうから、モデル検査で解を探してみる。「プログラムを書け」という問題の回答にはならないけど、プログラムなんか書かずに済むのなら書かないほうが良いだろう。
モデル検査ツールにも色々あるのだけど、いつも使っているNuSMVだと変数別に規則を書かなくてはならないのが面倒だったので、今回はよりプログラミング言語っぽい記述が可能なSpinに初挑戦してみた。
Spin(Promela)でモデルを記述すると以下のような感じになる。 aburaというプロセスが非決定的に油を移している。
#define A 10
#define B 7
#define C 3
int a = 10
int b = 0
int c = 0
inline move(from, to, cap)
{
atomic{
if
:: from > 0 && to < cap ->
if
::from+to<cap -> to = from+to; from = 0
::else -> from = from+to-cap; to = cap
fi
:: else -> skip
fi
}
}
active proctype abura()
{
do
:: true -> move(a, b, B)
:: true -> move(a, c, C)
:: true -> move(b, a, A)
:: true -> move(b, c, C)
:: true -> move(c, a, A)
:: true -> move(c, b, B)
od
}
で、ここで何を検証するかというと、「任意有限ステップ後に a=5 かつ b=5 の状態に到達しない」こと。これをSpinにかけてやると、本当に到達しないなら検証に成功し、もし到達する可能性があるなら「反例」として「到達するパス」を教えてくれる。
というわけで、XSpinで「!<>(p && q)」を検査。 ただし、ここで p と q は以下のような定義。
#define p (a==5) #define q (b==5)
そうすると、「Verification Result: not valid」とか言われるので、「Run Guided Simulation」で「Run」を選んで反例のトレース見てみる。
preparing trail, please wait...done Starting abura with pid 0 spin: couldn't find claim (ignored) 2: proc 0 (abura) line 26 "pan_in" (state 1) [(1)] 4: proc 0 (abura) line 13 "pan_in" (state 2) [(((a>0)&&(b<7)))] 5: proc 0 (abura) line 16 "pan_in" (state 6) [else] 6: proc 0 (abura) line 16 "pan_in" (state 7) [a = ((a+b)-7)] < 6: proc 0 (abura) line 16 "pan_in" (state 8) [b = 7] < 8: proc 0 (abura) line 27 "pan_in" (state 17) [(1)] 10: proc 0 (abura) line 13 "pan_in" (state 18) [(((a>0)&&(c<3)))] 11: proc 0 (abura) line 16 "pan_in" (state 22) [else] 12: proc 0 (abura) line 16 "pan_in" (state 23) [a = ((a+c)-3)] < 12: proc 0 (abura) line 16 "pan_in" (state 24) [c = 3] < 14: proc 0 (abura) line 28 "pan_in" (state 33) [(1)] 16: proc 0 (abura) line 13 "pan_in" (state 34) [(((b>0)&&(a<10)))] 17: proc 0 (abura) line 15 "pan_in" (state 35) [(((b+a)<10))] < 17: proc 0 (abura) line 15 "pan_in" (state 36) [a = (b+a)] < 17: proc 0 (abura) line 15 "pan_in" (state 37) [b = 0] < 19: proc 0 (abura) line 31 "pan_in" (state 81) [(1)] 21: proc 0 (abura) line 13 "pan_in" (state 82) [(((c>0)&&(b<7)))] 22: proc 0 (abura) line 15 "pan_in" (state 83) [(((c+b)<7))] < 22: proc 0 (abura) line 15 "pan_in" (state 84) [b = (c+b)] < 22: proc 0 (abura) line 15 "pan_in" (state 85) [c = 0] < 24: proc 0 (abura) line 27 "pan_in" (state 17) [(1)] 26: proc 0 (abura) line 13 "pan_in" (state 18) [(((a>0)&&(c<3)))] 27: proc 0 (abura) line 16 "pan_in" (state 22) [else] 28: proc 0 (abura) line 16 "pan_in" (state 23) [a = ((a+c)-3)] < 28: proc 0 (abura) line 16 "pan_in" (state 24) [c = 3] < 30: proc 0 (abura) line 31 "pan_in" (state 81) [(1)] 32: proc 0 (abura) line 13 "pan_in" (state 82) [(((c>0)&&(b<7)))] 33: proc 0 (abura) line 15 "pan_in" (state 83) [(((c+b)<7))] < 33: proc 0 (abura) line 15 "pan_in" (state 84) [b = (c+b)] < 33: proc 0 (abura) line 15 "pan_in" (state 85) [c = 0] < 35: proc 0 (abura) line 27 "pan_in" (state 17) [(1)] 37: proc 0 (abura) line 13 "pan_in" (state 18) [(((a>0)&&(c<3)))] 38: proc 0 (abura) line 16 "pan_in" (state 22) [else] 39: proc 0 (abura) line 16 "pan_in" (state 23) [a = ((a+c)-3)] < 39: proc 0 (abura) line 16 "pan_in" (state 24) [c = 3] < 41: proc 0 (abura) line 31 "pan_in" (state 81) [(1)] 43: proc 0 (abura) line 13 "pan_in" (state 82) [(((c>0)&&(b<7)))] 44: proc 0 (abura) line 16 "pan_in" (state 86) [else] 45: proc 0 (abura) line 16 "pan_in" (state 87) [c = ((c+b)-7)] < 45: proc 0 (abura) line 16 "pan_in" (state 88) [b = 7] < 47: proc 0 (abura) line 28 "pan_in" (state 33) [(1)] 49: proc 0 (abura) line 13 "pan_in" (state 34) [(((b>0)&&(a<10)))] 50: proc 0 (abura) line 15 "pan_in" (state 35) [(((b+a)<10))] < 50: proc 0 (abura) line 15 "pan_in" (state 36) [a = (b+a)] < 50: proc 0 (abura) line 15 "pan_in" (state 37) [b = 0] < 52: proc 0 (abura) line 31 "pan_in" (state 81) [(1)] 54: proc 0 (abura) line 13 "pan_in" (state 82) [(((c>0)&&(b<7)))] 55: proc 0 (abura) line 15 "pan_in" (state 83) [(((c+b)<7))] < 55: proc 0 (abura) line 15 "pan_in" (state 84) [b = (c+b)] < 55: proc 0 (abura) line 15 "pan_in" (state 85) [c = 0] < 57: proc 0 (abura) line 27 "pan_in" (state 17) [(1)] 59: proc 0 (abura) line 13 "pan_in" (state 18) [(((a>0)&&(c<3)))] 60: proc 0 (abura) line 16 "pan_in" (state 22) [else] 61: proc 0 (abura) line 16 "pan_in" (state 23) [a = ((a+c)-3)] < 61: proc 0 (abura) line 16 "pan_in" (state 24) [c = 3] < 63: proc 0 (abura) line 31 "pan_in" (state 81) [(1)] 65: proc 0 (abura) line 13 "pan_in" (state 82) [(((c>0)&&(b<7)))] 66: proc 0 (abura) line 15 "pan_in" (state 83) [(((c+b)<7))] < 66: proc 0 (abura) line 15 "pan_in" (state 84) [b = (c+b)] < 66: proc 0 (abura) line 15 "pan_in" (state 85) [c = 0] < 68: proc 0 (abura) line 26 "pan_in" (state 1) [(1)] spin: trail ends after 69 steps #processes: 1 69: proc 0 (abura) line 21 "pan_in" (state 16) 1 processes created
思ったよりもだいぶ長いトレースが出てきたけど、 代入文を追いかけてみると、こんな感じになっている。
a から b に 7 升移す ((10,0,0) → (3,7,0)) a から c に 3 升移す ((3,7,0) → (0,7,3)) b から a に 7 升移す ((0,7,3) → (7,0,3)) c から b に 3 升移す ((7,0,3) → (7,3,0)) a から c に 3 升移す ((7,3,0) → (4,3,3)) c から b に 3 升移す ((4,3,3) → (4,6,0)) a から c に 3 升移す ((4,6,0) → (1,6,3)) c から b に 1 升移す ((1,6,3) → (1,7,2)) b から a に 7 升移す ((1,7,2) → (8,0,2)) c から b に 2 升移す ((8,0,2) → (8,2,0)) a から c に 3 升移す ((8,2,0) → (5,2,3)) c から b に 3 升移す ((5,2,3) → (5,5,0))
というわけで、探索をプログラムせずとも答えを得れたと。 これくらい単純な例だと探索を自分でプログラムしても大したことはないけど、扱う状態遷移系が複雑になると、自分で探索を行うプログラムを書くのは結構しんどいことになる。 そんな時にはモデル検査は非常に便利。
詳しくは4日で学ぶモデル検査 (初級編) (CVS教程 (1))(産業技術総合研究所システム検証研究センター)でもどうぞ(読書記録)。
ところで、ところで使ってみて知ったのだけど、Spinでモデル検査するときって、一回C言語のコードを出力してコンパイルして、それを使って検査しているんだな。 なんというか、それだけやっても十分割りにあうということか。
追記
masateruさんという方のmixi日記にて、別の回答が紹介されている。 assertを使う方法など、初心者の私には大変勉強になりました。
2008-07-05追記
「NuSMVだと変数別に規則を書かなくてはならない」と書いたが、これは間違い。これを書いた時点では ASSIGN で init(x) と next(x) に対する代入という形で書く方法しか知らず、その場合には変数別に規則を書く必要があるが、実際にはTRANSを使って遷移関係を直接記述する方法もあり、その場合にはこういった問題は無い。
調べた結果をかいてくれよ！
じゃ、結果もruby-devに送りますね。