當前位置：首頁 >

PRISM概率模型检测器初使用--骰子模型（改进版）

發布時間：2024/6/21 40 豆豆

生活随笔收集整理的這篇文章主要介紹了 PRISM概率模型检测器初使用--骰子模型（改进版）小編覺得挺不錯的,現在分享給大家,幫大家做個參考.

PRISM-probabilistic model checker概率模型檢測器

骰子模型 The dieexample 與馬爾科夫鏈有關

-目錄

PRISM-probabilistic model checker概率模型檢測器
- PRISM code
- 代碼解釋
- 操作解釋
  - - Exploring the model in PRISM 用PRISM探索模型
  - - Model checking with PRISM 用PRISM模型檢測
  - - Statistical Model checking withPRISM 用統計模型驗證結果
  - - Expected termination time預估終止次數

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一個骰子模塊
兩個變量，設s來指定算法當前要執行哪個步驟，d則為骰子的值（為0時表示還沒開始選）
s : [0..7]init0; s 是骰子模塊里的一個整數變量，范圍是0到7，初始值（initial）設為0
[]s=0 -> 0.5: (s'=1)+0.5 : (s'=2); s=0時，有0.5的可能性s跳到1并接著執行s=1后的動作，即（s’=1），有0.5的可能性s跳到2并執行s=2，即（s’=2）。注意當可能性的和不為1時，會報錯。
[]s=7 -> (s'=7); s=7時，繼續執行s=7。看起來像循環，但是PRISM的模擬器在循環進行第二步就停止了。所以可以看作是用來停止該算法的。

代碼用法具體網址：
-PRISM Language-Commands

-PRISM Language-Modules And Variables

操作解釋：

- Exploring the model in PRISM 用PRISM探索模型

導入代碼： 下載模塊源代碼，打開PRISM，點擊上排按鈕 “Model”，選“Open model”，導入下好的代碼。

使用模擬器（Simulator）：點擊下排的“Simulator”來到模擬器，在中部任意處雙擊（或右鍵），選擇“Newpath”建立一個新測試路徑。點擊在左上方“Automatic exploration”中的“Simulate”來生成算法的一個樣本。再次點擊執行樣本下一步驟。可多次點擊直到算法執行結束（這里是s=7）。

手動選擇路徑（s值）：右擊并選“Reset path”可重新創建一個樣本路徑（path）。也可點擊“Manual exploration”中的下一執行路徑來手動選擇樣本的路徑。

設置步驟大小：把“Steps”（在“Simulate”下方）中的值改1為20，再重建個path，算法會由一次走一步變成走20步，但是這里的骰子算法一般6到8步，列在“Path”框中。

- Model checking with PRISM 用PRISM模型檢測

下載屬性文件，點上排“Properties”選“Open propertieslist”導入。

const int x; P=? [ F s=7 & d=x ]

解釋：

const int x；即在“Properties”框左中的“Constants”中加入整數變量x（可用操作代替代碼）
P=? [ F s=7 & d=x ]；格式為 P=? [ F phi ]，意思是“從原始狀態到令phi能為true時的狀態時可能性（P）為多少？”。這里phi是s=7，d為新變量x的狀態。

計算不同x值對應的屬性式的可能性值：右擊“Properties”選“Verify”，選一個1到6之間的數并“OK”，PRISM會給出x為該值時同時s=7的可能性，如x=1時同時s=7，可能性為P=0.16666650772094727 。也可以點擊下排“Log”來獲得計算過程和結果的更多細節。

設置不同的參數，觀察P值的變化：打開上排的“Options”選“Options”，把“Terminationepsilon”中的參數 1.0e-6 改成 1.0e-10 ，然后重新“Verify”。

如上一情況，結果變成了 0.1666666666569654。

把參數改回 1.0e-6 。

做實驗（experiments）生成概率圖：右擊“Properties”選“New experiment”，對變量x進行設置：Range下方點選后者“End”填入范圍0和7，Step填入步驟為1，注意左下方“Create Graph”要勾選才能生成圖，“Use Simulation”先不勾。OK后，點選“New Graph”，點OK。即生成x為范圍內值時的概率曲線分布圖。

- Statistical Model checking withPRISM 用統計模型驗證結果

PRISM也可以用離散事件模擬工具來生成近似驗證結（即用給定數量的樣本（samples）來模擬計算概率，樣本數量越大，模擬計算的結果也就越接近上面屬性公式計算的值，以此來驗證可能性值的正確性）

模擬測試一定數量樣本下，可能性值的變化：在Properties中重開一個experiment，在“DefineConstants”對話框內的左下方要勾選“Use Simulation”，在“NewGraph Series”對話框中選“Existing Graph”以在原圖上生成新曲線（利于比較），接著，在右邊的“NumberOf samples”中把1000改為10， OK。得到的曲線與之前的曲線有很大的不同（因為樣本數量小）。另外，可通過改變Graph的設置（x軸，y軸等）來使曲線走向更清晰：如右擊概率圖，選擇“Graph Options”，在“Axes”選項下找“scale type”，把“Normal”改選成“Logarithmic”，曲線變化幅度小的圖的變化幅度就能被放大（放成對數曲線）。

再重開一個experiment，把sample為10，100，1000的概率曲線放在一個圖上，觀察曲線。結果當然是樣本數量越大，曲線越接近之前模擬器的計算結果。右擊選“Export Graph”可導出圖（選png格式）。

圖中（1）為1000，（2）為100，（3）為10.

- Expected termination time預估終止次數

用PRISM計算預期的步驟次數

骰子模型的次數很小，操作之前可先自己手算一下。

加一些東西進模型：在“Model”中代碼的最后加上這幾句：

rewards "steps" true : 1; endrewards

回到模擬器simulator，生成一個新path，在彈出框中的“Rewardvisibility”中點右邊的
1：’steps’(cumulative) 并點中間的朝左箭頭，然后OK。接著simulate運行，你會看到窗口右邊的reward在累積。（Reward下的“Steps”是每次結果的執行步數，“Steps”（+）才是次數的累加）

當然，以上也可以用一個form來完成： R=? [ F phi ]

解釋：從初始狀態到滿足phi狀態時，所有reward累加所得的預期值是多少？

為了滿足上面的運算，phi應該設成什么？

到Properties里，加入新property（右擊選“add”）,測試自己的phi，正確結果應該是11/3。如果你得到的結果是無窮大（infinity），你的phi就不是正確格式（可以查看原因）

轉載于:https://www.cnblogs.com/sriting/p/6031983.html

總結

以上是生活随笔為你收集整理的PRISM概率模型检测器初使用--骰子模型（改进版）的全部內容，希望文章能夠幫你解決所遇到的問題。

如果覺得生活随笔網站內容還不錯，歡迎將生活随笔推薦給好友。