PRISM概率模型检测器初使用--骰子模型（改进版）
PRISM-probabilistic model checker概率模型檢測(cè)器
骰子模型 The dieexample 與馬爾科夫鏈有關(guān)
-目錄
- PRISM-probabilistic model checker概率模型檢測(cè)器
- PRISM code
- 代碼解釋
- 操作解釋
- - Exploring the model in PRISM 用PRISM探索模型
- - Model checking with PRISM 用PRISM模型檢測(cè)
- - Statistical Model checking withPRISM 用統(tǒng)計(jì)模型驗(yàn)證結(jié)果
- - Expected termination time預(yù)估終止次數(shù)
PRISM code：
dtmcmoduledie//local states : [0..7]init0;//value of the died : [0..6]init0;[]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'=7);endmodule代碼解釋：
module die … endmodule一個(gè)骰子模塊
兩個(gè)變量，設(shè)s來(lái)指定算法當(dāng)前要執(zhí)行哪個(gè)步驟，d則為骰子的值（為0時(shí)表示還沒(méi)開(kāi)始選）
s : [0..7]init0; s 是骰子模塊里的一個(gè)整數(shù)變量，范圍是0到7，初始值（initial）設(shè)為0
[]s=0 -> 0.5: (s'=1)+0.5 : (s'=2); s=0時(shí)，有0.5的可能性s跳到1并接著執(zhí)行s=1后的動(dòng)作，即（s’=1），有0.5的可能性s跳到2并執(zhí)行s=2，即（s’=2）。注意當(dāng)可能性的和不為1時(shí)，會(huì)報(bào)錯(cuò)。
[]s=7 -> (s'=7); s=7時(shí)，繼續(xù)執(zhí)行s=7。看起來(lái)像循環(huán)，但是PRISM的模擬器在循環(huán)進(jìn)行第二步就停止了。所以可以看作是用來(lái)停止該算法的。
代碼用法具體網(wǎng)址：
-PRISM Language-Commands
-PRISM Language-Modules And Variables
操作解釋：
- Exploring the model in PRISM 用PRISM探索模型
導(dǎo)入代碼： 下載模塊源代碼，打開(kāi)PRISM，點(diǎn)擊上排按鈕 “Model”，選“Open model”，導(dǎo)入下好的代碼。
使用模擬器（Simulator）：點(diǎn)擊下排的“Simulator”來(lái)到模擬器，在中部任意處雙擊（或右鍵），選擇“Newpath”建立一個(gè)新測(cè)試路徑。點(diǎn)擊在左上方“Automatic exploration”中的“Simulate”來(lái)生成算法的一個(gè)樣本。再次點(diǎn)擊執(zhí)行樣本下一步驟。可多次點(diǎn)擊直到算法執(zhí)行結(jié)束（這里是s=7）。
手動(dòng)選擇路徑（s值）：右擊并選“Reset path”可重新創(chuàng)建一個(gè)樣本路徑（path）。也可點(diǎn)擊“Manual exploration”中的下一執(zhí)行路徑來(lái)手動(dòng)選擇樣本的路徑。
設(shè)置步驟大小：把“Steps”（在“Simulate”下方）中的值改1為20，再重建個(gè)path，算法會(huì)由一次走一步變成走20步，但是這里的骰子算法一般6到8步，列在“Path”框中。
- Model checking with PRISM 用PRISM模型檢測(cè)
下載屬性文件，點(diǎn)上排“Properties”選“Open propertieslist”導(dǎo)入。
const int x; P=? [ F s=7 & d=x ]解釋：
const int x； 即在“Properties”框左中的“Constants”中加入整數(shù)變量x（可用操作代替代碼）
P=? [ F s=7 & d=x ]；格式為 P=? [ F phi ]，意思是“從原始狀態(tài)到令phi能為true時(shí)的狀態(tài)時(shí)可能性（P）為多少？”。這里phi是s=7，d為新變量x的狀態(tài)。
計(jì)算不同x值對(duì)應(yīng)的屬性式的可能性值：右擊“Properties”選“Verify”，選一個(gè)1到6之間的數(shù)并“OK”，PRISM會(huì)給出x為該值時(shí)同時(shí)s=7的可能性，如x=1時(shí)同時(shí)s=7，可能性為P=0.16666650772094727 。也可以點(diǎn)擊下排“Log”來(lái)獲得計(jì)算過(guò)程和結(jié)果的更多細(xì)節(jié)。
設(shè)置不同的參數(shù)，觀察P值的變化：打開(kāi)上排的“Options”選“Options”，把“Terminationepsilon”中的參數(shù) 1.0e-6 改成 1.0e-10 ，然后重新“Verify”。
如上一情況，結(jié)果變成了 0.1666666666569654。
把參數(shù)改回 1.0e-6 。
做實(shí)驗(yàn)（experiments）生成概率圖：右擊“Properties”選“New experiment”，對(duì)變量x進(jìn)行設(shè)置：Range下方點(diǎn)選后者“End”填入范圍0和7，Step填入步驟為1，注意左下方“Create Graph”要勾選才能生成圖，“Use Simulation”先不勾。OK后，點(diǎn)選“New Graph”，點(diǎn)OK。即生成x為范圍內(nèi)值時(shí)的概率曲線分布圖。
- Statistical Model checking withPRISM 用統(tǒng)計(jì)模型驗(yàn)證結(jié)果
PRISM也可以用離散事件模擬工具來(lái)生成近似驗(yàn)證結(jié)（即用給定數(shù)量的樣本（samples）來(lái)模擬計(jì)算概率，樣本數(shù)量越大，模擬計(jì)算的結(jié)果也就越接近上面屬性公式計(jì)算的值，以此來(lái)驗(yàn)證可能性值的正確性）
模擬測(cè)試一定數(shù)量樣本下，可能性值的變化：在Properties中重開(kāi)一個(gè)experiment，在“DefineConstants”對(duì)話(huà)框內(nèi)的左下方要勾選“Use Simulation”，在“NewGraph Series”對(duì)話(huà)框中選“Existing Graph”以在原圖上生成新曲線（利于比較），接著，在右邊的“NumberOf samples”中把1000改為10， OK。得到的曲線與之前的曲線有很大的不同（因?yàn)闃颖緮?shù)量小）。另外，可通過(guò)改變Graph的設(shè)置（x軸，y軸等）來(lái)使曲線走向更清晰：如右擊概率圖，選擇“Graph Options”，在“Axes”選項(xiàng)下找“scale type”，把“Normal”改選成“Logarithmic”，曲線變化幅度小的圖的變化幅度就能被放大（放成對(duì)數(shù)曲線）。
再重開(kāi)一個(gè)experiment，把sample為10，100，1000的概率曲線放在一個(gè)圖上，觀察曲線。結(jié)果當(dāng)然是樣本數(shù)量越大，曲線越接近之前模擬器的計(jì)算結(jié)果。右擊選“Export Graph”可導(dǎo)出圖（選png格式）。
圖中（1）為1000，（2）為100，（3）為10.
- Expected termination time預(yù)估終止次數(shù)
用PRISM計(jì)算預(yù)期的步驟次數(shù)
骰子模型的次數(shù)很小，操作之前可先自己手算一下。
加一些東西進(jìn)模型：在“Model”中代碼的最后加上這幾句：
rewards "steps" true : 1; endrewards回到模擬器simulator，生成一個(gè)新path，在彈出框中的“Rewardvisibility”中點(diǎn)右邊的
1：’steps’(cumulative) 并點(diǎn)中間的朝左箭頭，然后OK。接著simulate運(yùn)行，你會(huì)看到窗口右邊的reward在累積。（Reward下的“Steps”是每次結(jié)果的執(zhí)行步數(shù)，“Steps”（+）才是次數(shù)的累加）
當(dāng)然，以上也可以用一個(gè)form來(lái)完成： R=? [ F phi ]
解釋：從初始狀態(tài)到滿(mǎn)足phi狀態(tài)時(shí)，所有reward累加所得的預(yù)期值是多少？
為了滿(mǎn)足上面的運(yùn)算，phi應(yīng)該設(shè)成什么？
到Properties里，加入新property（右擊選“add”）,測(cè)試自己的phi，正確結(jié)果應(yīng)該是11/3。如果你得到的結(jié)果是無(wú)窮大（infinity），你的phi就不是正確格式（可以查看原因）
轉(zhuǎn)載于:https://www.cnblogs.com/sriting/p/6031983.html
總結(jié)
以上是生活随笔為你收集整理的PRISM概率模型检测器初使用--骰子模型（改进版）的全部?jī)?nèi)容，希望文章能夠幫你解決所遇到的問(wèn)題。
