食玩問題その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個となると
当たる確率の上昇がゆるやかになっていますね。

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

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