PRISM概率模型检测器初使用--骰子模型

PRISM—probabilistic model checker概率模型检测器

骰子模型 The dieexample

http://www.prismmodelchecker.org/tutorial/die.php 与马尔科夫链有关

PRISM code：

dtmc

moduledie

//local state

s : [0..7]init0;

//value of the die

d : [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的模拟器在循环进行第二步就停止了。所以可以看作是用来停止该算法的。

代码用法具体网址：http://www.prismmodelchecker.org/manual/ThePRISMLanguage/Commands

http://www.prismmodelchecker.org/manual/ThePRISMLanguage/ModulesAndVariables

操作解释：

Exploring the model in PRISM 用PRISM探索模型

下载模块源代码http://www.prismmodelchecker.org/tutorial/examples/die/die.pm，打开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

下载属性文件http://www.prismmodelchecker.org/tutorial/examples/die/die.pctl，点上排“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就不是正确格式（可以查看原因：http://www.prismmodelchecker.org/manual/FrequentlyAskedQuestions/PRISMProperties#inf_rewards）

PRISM概率模型检测器初使用--骰子模型相关推荐

PRISM概率模型检测器初使用--骰子模型（改进版）
PRISM-probabilistic model checker概率模型检测器骰子模型 The dieexample 与马尔科夫链有关 -目录 PRISM-probabilistic model ...
[DeepSpeed]初代chatGPT模型部署实践
DeepSpeed Chat 部署方式中间遇到很多坑,解决方法都写这里了DeepSpeed 部署中bug以及解决方法环境基于阿里云GPU 云服务器部署实践操作系统版本: Ubuntu 18.0 ...
概率论的学习和整理--番外7：简单的丢骰子和抽黑球白球问题，对比不同概率模型求解的差别。
前言:通过题目去理解概率知识刷题的意义虽然说刷题不好,但是不会做题肯定也不对理论学了一箩筐,但是不会做题,说明不会应用模型,对模型的条件,应用环境,背后的逻辑理解的不深刷题的局限性不要记这个 ...
navicat模型显示注释_RetinaNet模型构建面罩检测器
字幕组双语原文:如何使用RetinaNet模型构建面罩检测器英语原文:How to build a Face Mask Detector using RetinaNet Model! 翻译:雷锋字幕 ...
自然语言处理一大步，应用Word2Vec模型学习单词向量表征
选自TowardsDataScience,作者:Suvro Banerjee,机器之心编译,参与:Pedro.张倩. 在常见的自然语言处理系统中,单词的编码是任意的,因此无法向系统提供各个符号之间可能 ...
机器学习——HMM(隐马尔可夫模型的基本概念)(一)
[开始之前]由于隐马尔可夫模型属于机器学习中比较难也比较重要的知识,所以此算法笔者将分段讲解,本文主要讲的是隐马尔可夫模型的定义以及相关例子,在后续的文章中会讲到概率计算方法如前向算法.后向算法.学习 ...
隐马尔科夫模型（HMM）等文章记录
[link] 如何用简单易懂的例子解释隐马尔可夫模型? - 知乎 --骰子举例举的不错: 一站式解决:隐马尔可夫模型(HMM)全过程推导及实现 - 知乎 --略微有点长,看看能不能看完马尔科夫模型 ...
一站式解决：隐马尔可夫模型（HMM）全过程推导及实现
作者 | 永远在你身后转载自知乎用户永远在你身后 [导读]隐马尔可夫模型(Hidden Markov Model,HMM)是关于时许的概率模型,是一个生成模型,描述由一个隐藏的马尔科夫链随机生成不可 ...
小样，加张图你就不认识我了？“补丁”模型骗你没商量！| 技术头条
作者 | Simen Thys, Wiebe Van Ranst(共同一作) 译者 | 刘畅编辑 | Rachel.Jane 出品 | AI科技大本营(id:agznai100) [导语]本文介绍了 ...
Nat. Commun.｜概率蛋白质序列模型的生成能力
本文介绍了由坦普尔大学Vincenzo Carnevale和Allan Haldane共同通讯发表在Nature Communications的研究成果:本文提出了一个新的标准来度量蛋白质序列生成模型 ...

PRISM概率模型检测器初使用--骰子模型

PRISM概率模型检测器初使用--骰子模型相关推荐

最新文章

热门文章