论文部分内容阅读
摘 要 首先介绍自动售货机的工作原理和基本功能，并根据工作原理对其进行Petri网模型的构建。而后Petri网模型的建立与化简技术的结合使用，使得复杂的Petri网模型能够得以简单化，系统的活性、有界性和合理性等都能直观地表现出来。
关键词 Petri网；自动售货机；系统建模
中图分类号 TP 文献标识码 A 文章编号 1673-9671-(2010)121-0155-01
基于Petri网的自动售货机的建模就是根据系统功能抽象自动售货机的工作信息，得出系统的状态（库所）和操作（转换），并利用HPSIM软件对系统的Petri网模型进行测试，同时通过Petri网的化简规则验证模型的合理性。
1 自动售货机动态模型的建立
自动售货机的功能要求是：首先，用户准备，系统服务器启动；其次，用户用按键选择商品，在数码管上显示商品的编号和单价；然后用户准备投币，投币时，按一次键模仿投入1元硬币。投入硬币的数量够买入商品时，点亮一个指示灯，表示商品已经买出。如果输入的硬币不够数，按退款键可以退出硬币，清除投币的显示数据。如果在硬币数量足够的情况下，系统中的货物总量不足时，系统通过网络向远程服务器发送缺货信息。
根据自动售货机的功能如顺序Petri网模型、选择Petri网模型和并行Petri网模型等对自动售货机进行动态模型的建立。
通过对自动售货机交易流程状态表的分析，利用HPSIM工具能够实现自动售货机交易流程的Petri网建模。
2 模型合理性验证
Petri网模型的合理性是指：对应于起始库所的每一个标记，最终会有且仅有一个标记出现在终止库所中，当终止库所中出现标记时，其它所有库所都为空，对每个转换，从初始状态都能够到达该转换的就绪状态。通常对于复杂的、大型的Petri网模型的合理性验证通过上述定义较难实现，为更好地分析模型的合理性在此引入Petri网模型化简技术。Petri网的化简是指在某种性质不变的基础上，采用等效变换，以达到缩小状态空间、简化系统分析的目的。
2.1 Petri网的化简规则
Petri网模型化简规则包括以下4条：（矩形表示Petri网模型中的转换，圆形表示Petri网模型中的库所）。
1）合并库所：如果库所P1和P2有相同的输入输出转换，则可以将库所P1和P2合并；再者，如果在Petri网中输入输出弧都唯一的库所P12的输入转换T1和输出转换T2不为空且唯一，那么库所P12可被化简。2）合并转换：如果Petri网模型中转换T1和T2有相同的输入输出库所，那么可以将转换T1和T2合并为一个转换T12。3）消除库所：如果在Petri网中输入输出弧都唯一的转换T1的输入库所P1和输出库所P2不为空且唯一，那么转换T1的输入输出库所可被化简。4）复杂变换：复杂变换是在前面所述三条化简规则的基础上产生的一种新的化简方式，实际上它只是前三条化简规则的一种应用。
2.2 自动售货机Petri网模型的合理性分析
利用Petri网模型的4条化简规则对自动售货机模型进行化简，并对其合理性进行验证。过程如下：
1）应用化简规则1和规则3，消除库所P3、P4、P5、P6、P7，并将其合并为Q1；消除库所P10、P11，将其合并为Q2；消除库所P15、P18，将其合并为Q3；消除库所P14、P16，将其合并为Q4；消除库所P17、P19，将其合并为Q5；同理，消除库所P12、P13，将其合并为Q6。库所Q1、Q2、Q3、Q4、Q5和Q6产生后，经过HPSIM工具执行过后，模型的执行流程没有改变，说明化简过程不影响系统的执行，只是复杂的系统模型被简化了。2）应用化简规则4，消除库所M1、转换T13；消除库所Q5、转换T15；消除库所Q6、转换T12；消除库所P20，库所Q4，转换T6；消除库所Q1，转换K1；消除库所P1，转换T1；消除库所Q3；消除库所P2，转换T19。
荷兰学者Aalst证明了Petri网模型的充分必要条件是其具有有界性和活性，从而将合理性问题转化为Petri网动态性质的分析和验证。综上所述自动售货机的Petri网模型具有合理性，是活的、有界的。
参考文献
[1]杨雪,蒋昌俊.Petri网的化简规则在系统中的实现[J].计算机工程与应用,2003,2.
[2]袁崇义.Petri网原理[M].电子工业出版社,1998.
[3]张亮.基于Petri网化简技术的工作流模型正确性研究[J].计算机工程,2007,5.
作者简介
魏培李（1982－），女，汉族，华侨大学计算机科学与技术学院2007级在读工程硕士，研究方向：软件工程。
关键词 Petri网；自动售货机；系统建模
中图分类号 TP 文献标识码 A 文章编号 1673-9671-(2010)121-0155-01
基于Petri网的自动售货机的建模就是根据系统功能抽象自动售货机的工作信息，得出系统的状态（库所）和操作（转换），并利用HPSIM软件对系统的Petri网模型进行测试，同时通过Petri网的化简规则验证模型的合理性。
1 自动售货机动态模型的建立
自动售货机的功能要求是：首先，用户准备，系统服务器启动；其次，用户用按键选择商品，在数码管上显示商品的编号和单价；然后用户准备投币，投币时，按一次键模仿投入1元硬币。投入硬币的数量够买入商品时，点亮一个指示灯，表示商品已经买出。如果输入的硬币不够数，按退款键可以退出硬币，清除投币的显示数据。如果在硬币数量足够的情况下，系统中的货物总量不足时，系统通过网络向远程服务器发送缺货信息。
根据自动售货机的功能如顺序Petri网模型、选择Petri网模型和并行Petri网模型等对自动售货机进行动态模型的建立。
通过对自动售货机交易流程状态表的分析，利用HPSIM工具能够实现自动售货机交易流程的Petri网建模。
2 模型合理性验证
Petri网模型的合理性是指：对应于起始库所的每一个标记，最终会有且仅有一个标记出现在终止库所中，当终止库所中出现标记时，其它所有库所都为空，对每个转换，从初始状态都能够到达该转换的就绪状态。通常对于复杂的、大型的Petri网模型的合理性验证通过上述定义较难实现，为更好地分析模型的合理性在此引入Petri网模型化简技术。Petri网的化简是指在某种性质不变的基础上，采用等效变换，以达到缩小状态空间、简化系统分析的目的。
2.1 Petri网的化简规则
Petri网模型化简规则包括以下4条：（矩形表示Petri网模型中的转换，圆形表示Petri网模型中的库所）。
1）合并库所：如果库所P1和P2有相同的输入输出转换，则可以将库所P1和P2合并；再者，如果在Petri网中输入输出弧都唯一的库所P12的输入转换T1和输出转换T2不为空且唯一，那么库所P12可被化简。2）合并转换：如果Petri网模型中转换T1和T2有相同的输入输出库所，那么可以将转换T1和T2合并为一个转换T12。3）消除库所：如果在Petri网中输入输出弧都唯一的转换T1的输入库所P1和输出库所P2不为空且唯一，那么转换T1的输入输出库所可被化简。4）复杂变换：复杂变换是在前面所述三条化简规则的基础上产生的一种新的化简方式，实际上它只是前三条化简规则的一种应用。
2.2 自动售货机Petri网模型的合理性分析
利用Petri网模型的4条化简规则对自动售货机模型进行化简，并对其合理性进行验证。过程如下：
1）应用化简规则1和规则3，消除库所P3、P4、P5、P6、P7，并将其合并为Q1；消除库所P10、P11，将其合并为Q2；消除库所P15、P18，将其合并为Q3；消除库所P14、P16，将其合并为Q4；消除库所P17、P19，将其合并为Q5；同理，消除库所P12、P13，将其合并为Q6。库所Q1、Q2、Q3、Q4、Q5和Q6产生后，经过HPSIM工具执行过后，模型的执行流程没有改变，说明化简过程不影响系统的执行，只是复杂的系统模型被简化了。2）应用化简规则4，消除库所M1、转换T13；消除库所Q5、转换T15；消除库所Q6、转换T12；消除库所P20，库所Q4，转换T6；消除库所Q1，转换K1；消除库所P1，转换T1；消除库所Q3；消除库所P2，转换T19。
荷兰学者Aalst证明了Petri网模型的充分必要条件是其具有有界性和活性，从而将合理性问题转化为Petri网动态性质的分析和验证。综上所述自动售货机的Petri网模型具有合理性，是活的、有界的。
参考文献
[1]杨雪,蒋昌俊.Petri网的化简规则在系统中的实现[J].计算机工程与应用,2003,2.
[2]袁崇义.Petri网原理[M].电子工业出版社,1998.
[3]张亮.基于Petri网化简技术的工作流模型正确性研究[J].计算机工程,2007,5.
作者简介
魏培李（1982－），女，汉族，华侨大学计算机科学与技术学院2007级在读工程硕士，研究方向：软件工程。