人類は推論しました

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 ]

comctl32.lib;Advapi32.lib;user32.lib;Gdi32.lib;

libjasperd.lib;opencv_gpu230d.lib;libjpegd.lib;

opencv_haartraining_engined.lib;libpngd.lib;opencv_highgui230d.lib;

libtiffd.lib;opencv_imgproc230d.lib;opencv_calib3d230d.lib;

opencv_legacy230d.lib;opencv_contrib230d.lib;opencv_ml230d.lib;

opencv_core230d.lib;opencv_objdetect230d.lib;opencv_features2d230d.lib;

opencv_video230d.lib;opencv_flann230d.lib;zlibd.lib

以前から気にはなっていたけど使わなっかったDoxygenを使う気になったので メモメモ

まず、自分はコメントとして///（スラッシュ３つ）使うのが好きなのでこれを採用
この場合、一行のみのコメントだとbriefになって、複数行続くと勝手にdetailになるようです。便利！

doxygenのはまりどころとしては、
VisualC++(2010以前で確認)ではソースファイルはデフォルトでShift-JISになります。
ソースコードのエンコーディングをDoxygenに教えるにはINPUT_ENCODINGのオプションを使います。
また、Doxygenが出力するファイルのエンコーディングはDOXYFILE_ENCODINGオプションを使います。
しかし、DoxygenのINPUT_ENCODINGをShift-JISに、DOXYFILE_ENCODINGをUTF-8にして、Doxygenのコマンドに使うと円マークとバックスラッシュの変換が都合よく行かず、
結果として、Doxygenコマンドを認識できないという問題があります。
（参考：http://blogs.yahoo.co.jp/onion_developer/5791986.html）

JavaDocスタイルのコマンドでは@マークを使うため、このような問題は起こりません。
しかし、texを入れてtexコマンドを使おうとしたときに同様の問題にぶつかります。
（自分はこちらに引っかかった）

そこで、回避策としてはINPUT_ENCODINGはCP932 を指定しましょう。
こうすると、Doxygenの中で円マークをうまくバックスラッシュとして読んでくれて、コマンドが通るようになります。