トップ «前の日記(2007-07-09) 最新 次の日記(2007-07-11)» 月表示 編集

日々の流転


2007-07-10 [長年日記]

λ. ヘッダにしかない関数

mkmf.rb を濫用して調べてみる([ruby-dev:31176])。 ささださんが「他にも、いろいろあるようですね」と言っていたが、本当に色々あるなw

Tags: ruby

λ. 油売り算

キミならどう書く 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を使って遷移関係を直接記述する方法もあり、その場合にはこういった問題は無い。

本日のツッコミ(全2件) [ツッコミを入れる]
ψ ささだ (2007-07-11 10:42)

調べた結果をかいてくれよ!

ψ さかい (2007-07-11 21:14)

じゃ、結果もruby-devに送りますね。