食玩問題その3

前回、誕生日のパラドックスをPRISMで解いたので、
調子に乗って食玩問題もモデル化してみたらできましたので
紹介させて頂きます。

いたって簡単です。

dtmc
const int NUM_BOX; // 購入数
const int OMAKE;   // おまけの種類

module omake

  n : [0..OMAKE] init 0;   // 既に手に入れたおまけの個数
  b : [0..NUM_BOX] init 1; // 購入済みの個数

  [] (n<OMAKE)&(b<NUM_BOX) -> (OMAKE-n)/OMAKE : (n'=n+1)&(b'=b+1) + 1-(OMAKE-n)/OMAKE : (n'=n)&(b'=b+1);
  [] (n=OMAKE)&(b<NUM_BOX) -> (b'=b+1);

endmodule

定数としては、単純に問題のパラメータとして、
購入する予定の数と、おまけがいくつ混入しているか、
というものを与えています。

状態遷移の定義ですが、おまけがまだ全種類集まっていないとき、かつ購入予定数に
到達していないときに、残りの当たっていないおまけが当たるか当たらないか、
に遷移します。
当たり終わったら購入予定数にいくまで買い続けます。


というシンプルなモデルで表現できました。


前回同様、「おまけがすべて揃う確率」をPRISMで求め、
購入数を増やしていったときのおまけの当たる確率を計算してみましょう。

横軸が商品の購入数で、凡例にある4つの数値がおまけの種類です。
おまけの種類が増えるにつれ、やはり揃う確率も減ってきていますね。
15種類だと100個買えばほぼ100%の確率で揃っていたのですが、20個となると
当たる確率の上昇がゆるやかになっていますね。

ただ、前の記事にも書いていましたが当たる確率って均等じゃないですよね。
ものによってはレアなおまけもあるでしょうし。

例えば、おまけが「正規分布」で出現する場合に、
いくつ買えば全種類揃う確率が高いのか、というような感じで、
おまけの出方を変えたりするとまた面白いのかなー。。。

誕生日のパラドックスその2

その2です。
これは、「同じクラスに、同じ誕生日の人がいる確率は？」という問題でした。
直感的には、1年365日なのでとても確率が低そうに見えます。

その1だと、同じ誕生月の人がいるか、という考察しかしていなかったので
今回きちんと解を算出したいと思います。


普通に解いても面白く無いので、今回PRISMというツールを利用して解析したいと思います。
学生時代研究で利用していたのですが、確率モデルを解析するツールです。

参考までに、公式ページです。
http://www.prismmodelchecker.org/


まず確率モデルを設計していきます。
PRISMで書くと下記になります。

＝＝＝＝＝＝＝＝＝＝＝＝＝＝＝＝＝＝＝＝＝＝＝＝＝＝＝＝＝＝＝＝＝
文法を簡単に説明します。
dtmcってのは、モデルの種類を定義していて、今回は
「Discrete-Time Markov Chain（離散時間マルコフ連鎖）」というモデルです。
定数をNで定義し、モデルの変数を8行目～9行目で定義しています。
実際の遷移定義は13行目～16行目です。
例えば、ある状態から、0.3で遷移先状態①に遷移し、
0.7の確率で遷移先状態②に遷移する場合、下記のように記述します。

【ある状態】 -> 0.3 : 【遷移先状態①】 + 0.7 : 【遷移先状態②】
＝＝＝＝＝＝＝＝＝＝＝＝＝＝＝＝＝＝＝＝＝＝＝＝＝＝＝＝＝＝＝＝＝

単純に"N"人分誕生日を同じか確認していく、というモデルです。

今回の問題は、普通に解くと場合分けが必要なのですが、
それを考えなくていいように、"day"という変数を使って、
　誕生日が同じ⇒dayを減らさない
　誕生日が違う⇒dayを減らす
という方法で「任意の誰かが誕生日が同じであるかどうか」
を解くようにしています。

各変数の意味：
　s   : "1"の時、計算終了状態
　n   : 誕生日確認済み人数
  day : 誕生日が違う人がいると-1される
　m   : 誕生日が同じ人の数

13行目が最もメインで、
　誕生日が違う場合は、dayを減らし、残りの確認人数nを減らします。
　誕生日が同じ場合は、誕生日が同じ人の数mを増やし、残りの確認人数nを減らします。
ってな感じです。
14行目は、「すべての誕生日で同じペアが存在した」という状態を想定しており、
確率1で遷移します。で、人数nが0になったら状態s=1に遷移し、計算を終了します。


では、計算してみましょう。

PRISMは、「モデルに対してある性質を満たす確率を計算する」ツールです。
今回は、「s=1かつmが1以上の状態に到達する確率」を求めることで、誕生日のパラドックスを解きたいと思います。

またPRISMでは、定数をある範囲で動かして、各値での計算結果をグラフに
出してくれます。便利ですね。

今回は、クラスにいる人数をNとしていますので、クラス内の人数を
3～100で動かしてみましょう。

40人のクラスだと、ほぼ90%ですね。
（値としては0.891でした）

問題を解くよりは「PRISMの紹介」メインになってしまいましたが、
同じ誕生日がいる確率って結構高いんですね。

私は自分と同じ誕生日の人に出会ったこと無いので、
この結果は信じておりませんがｗ

TVサーバの構築(1)

すっごく久しぶりの更新です。（3年空きました）

最近は仕事でもプライベートでも色々調べたり手を動かすことが
多いので、せっかくなのでそれらについて色々書いていこうとおもいます。

なので、元々「問題の解説」というテーマでしたが、IT関連の情報も発信していきます。


今回のテーマは、「TVサーバ」です。
最近、会社の先輩がnasneを買ったらしく、家の中で色々な端末で見れるだけでなく、
タブレットにダウンロードして、出先でも見れるようにしてるみたいです。

自分もそれしたい！と考えて、色々調べました。

nasneを買うのが早いのかなと思っていましたが、
FAT32というファイルシステムの制約で2GBまでだそうですので、なんか微妙だなと。

調べていると、今の自作PCに取り付けているPIXELA社の「PIX-DT230-PE0」
というキャプチャボードのStation TVというソフトにTVサーバの機能があるみたいです。

早速それを更新してサーバを立てて、試しにローカルでそのTVサーバにアクセスしてみました。
利用したのは、XBMCというDLNA接続ができるクライアントです。

TVサーバ、見つかった！
あれ、でも見れない。。。

どうやら、DLNAだけでなく、DTCP-IPというTVサーバ用の保護された接続方式に対応した
ソフトでないとダメなようです。

今のところ、フリーソフトは無いようで（当然か？）

・Dixim Digital TV plus
・SoftDMA

の２つが主だったツールのようです。
両方ともシェアウェアですが、体験版があったので使ってみました。

今回は「Dixim Digital TV plus」でやってみました。
TVサーバが見つからない！！なんでや！って一人で騒いでいましたが、
しばらく放置していたら見つかりました。（ちょっと読み込みに時間がかかるようです）


しかし、「著作権保護に対応していません」と出ました。
どうやらディスプレイの接続方式が、「HDCP」という映像データの暗号化技術に
対応しているディスプレイでないと再生させないようです。

今のディスプレイは接続方式がアナログのD-sub15ピン（青いやつ）なので、
だめです。厳しいですね。

これを解決するには、ディスプレイごと買えないとなので一旦こっちは保留、
もう一台のノートPCでLAN経由で接続してみましたが、今度は、

「お使いのパソコンのセキュリティ設定やネットワーク環境、
サーバー機器の症状を確認して下さい。」

って出ました。もう疲れました。
また今度トライします。