確率モデル検査器PRISMを使ってみる（DTMC）

dtmc

module die

// local state

s : [0..8] init 0;

// value of the die

d : [0..6] init 0;

[] s=0 -> 0.5 : (s'=1) + 0.5 : (s'=2);

[] s=1 -> 0.5 : (s'=3) + 0.5 : (s'=4);

[] s=2 -> 0.5 : (s'=5) + 0.5 : (s'=6);

[] s=3 -> 0.5 : (s'=1) + 0.5 : (s'=7) & (d'=1);

[] s=4 -> 0.5 : (s'=7) & (d'=2) + 0.5 : (s'=7) & (d'=3);

[] s=5 -> 0.5 : (s'=7) & (d'=4) + 0.5 : (s'=7) & (d'=5);

[] s=6 -> 0.5 : (s'=2) + 0.5 : (s'=7) & (d'=6);

[] s=7 -> (s'=8);

[] s=8 -> (s'=8);

endmodule

下のタブから Properties のタブを選択し画面を切り替えます．

Properties の白いボックスで右クリックをして「Add」を選択します．

そうするとダイアログが出るので Property にモデルでチェックしたいことを書きます．

P=?[F s=8&d=x ]

これは将来的（F）にs=8かつd=xになる確率は？というような意味です．

Okeyを押すと何やらエラーが出ますが，xが定義されていないよという意味なので．

とりあえずそのダイアログを Yes で閉じた後に

Properties の白いボックスのしたの Constats というところで設定します．

Constatsの枠の中で右クリックをして「Add constants」を選択します．

そうしたら，Name の場所が「C0」となっていると思うので「x」に書き換えてください．

Value は空欄のままにしておいてください．

これで準備は整ったので

右の Experiments のボックスの中で右クリックをして「New Experiment」を選択します．

すると，xの範囲を指定する画面が開きます．

ラジオボタンをRangeの方に切り替えて End を 6 に設定してOkayを押します．

グラフの書き方を聞いてきますがとりあえずそのまま Okey にします．

すると，d=0で0となり，残りで0.1666...ぐらいとなっているグラフが描かれると思います(下図)．

これがdの値がそれぞれの値になる確率になります．

dが1~6をとるサイコロの目のような振る舞いをすることがわかると思います．

次に，サイコロの目の期待値の計算をこのモデルを用いて行なってみます．

サイコロの目の期待値は1×1/6+2×1/6+3×1/6+4×1/6+5×1/6+6×1/6となり，7/2となるのが正しい値です．

下のタブを Model に戻して以下の式を追加します．

rewards "steps"

[] (s=7): d;

endrewards

R=?[F s=8 ]