CPNtools协议建模安全分析---实例(二)

2020/04/22 13:20
阅读数 199

首先,token值是变迁的内部的,当变迁点火触发的时候token才会在网络中移动。在颜色Petri网中token是有区分的。

1、我么现在举一个学生吃饼的例子 ,颜色这样定义。    s表示一个学生类型, p表示一个饼 类型。 在定义弧上的变量 ,定义x 为学生类型,  定义 y为 饼类型。

现在我们假设最初的初始状态是,有五个饼子,有三个学生,每个学生吃一个饼就吃饱了。现在建模分析。见下图

colset s=unit with student;
colset p=unit with pasty;

var x:s;

var y:p;

 

 现在点击快速执行步骤显示每个执行步骤达到的状态,从中我们可以看到,饼与学生之间的转换关系,每个状态执行状态如下图

 

     图 2  一个学生吃了一个饼 ,吃饱了一个学生,还剩4个饼子,2个学生挨饿

 

 图 3 两个学生吃了 两块饼,两个学生吃饱了,还有一个学生挨饿,剩下三块饼

 

 图 4 三个学生吃了三块饼子,三个学生吃饱了,还剩两块饼。  这个状态也是最终状态。(终止)

2、模型的状态空间分析,具体的数据,弧,节点,死变迁,绑定的值得上下限都有说明。

 

 

展开阅读全文
加载中
点击引领话题📣 发布并加入讨论🔥
0 评论
0 收藏
0
分享
返回顶部
顶部