本文提出一个基于层次型着色 Petri网CPN的购物系统建模方案。记录一个曾经做过的大作业当时任课老师讲的很有意思所以有认真学这个作业也有在认真的做课程比较小众希望给有在刚刚学习的同学作为参考。建模架构本Colored Petri Nets用于为购物系统建模架构为层次型着色Petri网共分3层。顶层Page为Main Page包含LoginRegisterQuery InfoShoppingChargingExit六个SubPage分别实现登录、注册、查询个人物品余额信息、购物功能、充值功能、退出功能。用户输入用户ID和密码在初始页面main等待检查是否已经注册比对用户ID数据库后若已经存在在数据库中进入登录页面Login若在数据库中查询不到用户ID进入注册页面Register注册完成后返回初始页面main等待检查是否已经注册。登录成功之后选择查询信息Query Info、购物Shopping、充值Charging、退出Exit功能。完成查询、购物、充值功能后返回选择功能页面。选择退出功能返回初始页面。二层SubPage Login实现登录功能进入登录页面输入用户ID、密码验证该用户密码是否正确验证成功后完成登录操作。二层SubPage Register实现注册功能进入注册页面后输入用户ID、用户密码将信息记录入用户ID、用户ID-密码、用户物品余额数据库即可实现注册功能。二层SubPage Query Info实现查询物品余额信息功能接收传入的用户ID查询用户物品余额数据库并显示该用户拥有的物品和目前的余额。二层SubPage Shopping实现购物功能接收传入的用户ID用三层SubPage Query Info实现查询物品余额信息功能在数据库中查询到该用户目前拥有的物品和余额选择要购买的商品如果该用户余额大于等于该商品金额即可购买将该商品信息加入该用户拥有物品列表中并扣除该商品金额若该用户余额小于该商品金额无法购买该用户物品列表和余额信息不变。重新计算该用户拥有的物品列表和金额并在用户物品余额数据库中更新该信息并显示该信息即可实现购物功能。二层SubPage Charging实现用户充值功能接收传入的用户ID使用三层SubPage Query Info实现查询物品余额信息功能在数据库中查询到该用户目前拥有的物品和余额进入充值页面选择要充值的金额100、200、300充值成功即会在用户余额中增加相应的金额完成充值后在用户物品余额数据库中更新该信息并显示充值后的用户信息即可实现充值功能。二层SubPage Exit实现退出功能接收传入的用户ID在用户ID-密码数据库找到该用户的ID密码退出到初始页面待定。三层SubPage Query Info与二层SubPage Query Info功能相同实现查询物品余额信息功能接收传入的用户ID查询用户物品余额数据库并显示该用户拥有的物品和目前的余额。类型声明函数member(e,l)e是否在列表l中若存在返回true不存在返回falsefun member (e,l) if l []then falseelseif (e List.hd l)then trueelse member (e,List.tl l);函数unmember(e,l)e不在列表l中返回true存在返回falsefun unmember (e,l) if l []then trueelseif (e List.hd l)then falseelse unmember (e,List.tl l);函数insert (e,l)e插入到列表l中前面fun insert (e,l) if member (e,l)then lelse e::l;每层页面具体分析顶层PageShopping System库所main的颜色集为UserInfo有初始Token“1(user1,111111)1(user2,222222)1(user3,333333)1(user3,123456)1(user6,666666)”开始运行时token进入检查验证Verify UserID判断该用户UserId是否已经注册过判断方法利用防卫表达式[member(uid,userspack1)]和[unmember(uid,userspack1)]判断检查uid是否在存储所有已注册用户UserId列表的User融合集中若存在点火变迁in若不存在则点火变迁out若已经注册过可以进入登录Login页面若未注册过进入注册Register页面注册完成返回库所main可通过上述流程进入登录Login页面登录成功后可进行浏览选择查询个人用户进入Query info页面选择购物进入Shopping页面选择充值进入Charging页面完成功能退出页面后可返回至选择功能页面在该页面可以进入退出Exit页面返回库所main。二层SubPageLogin库所Login Page颜色集类型为UserInfo当该库所得到token用户账号密码激活变迁Input UserID,UserPw输入用户ID、用户密码该token到Verify Password下一步验证该用户密码是否正确只有该用户的账号uid和密码up与用户账号密码数据库融合集UserSDateBase一致即可激活变迁验证成功完成登录操作。二层SubPageRegister库所Register Page颜色集类型为UserInfo当该库所得到token用户账号密码激活变迁Input输入用户ID、用户密码(uid,up)将信息记录入用户ID、用户ID-密码、用户物品余额数据库即将该用户账号uid加入用户账号数据库User融合集、该用户账号uid和密码up加入用户ID-密码数据库UserSDateBase融合集、创建新的用户物品余额信息加入用户物品余额数据库UGDataBase融合集如此完成该用户注册。二层SubPageQuery Info库所user颜色集类型为UserID当该库所有token时实现查询物品余额信息功能接收传入的用户IDuid查询用户物品余额数据库UGDataBase融合集并显示该用户拥有的物品和目前的余额如此完成查询操作。二层SubPageShopping库所shopping颜色集类型为UserID接收传入的用户IDuid用三层SubPage Query Info实现查询物品余额信息功能库所shopping page颜色类型为UserGoodsInfo显示该用户目前拥有的物品和余额选择要购买的商品Goods如果该用户余额um大于等于该商品金额gm即可购买将该商品信息(gid,gname,gm)加入该用户拥有物品列表goodspack1中goodspack1^^[(gid,gname,gm)]并扣除该商品金额um-gm若该用户余额小于该商品金额无法购买该用户物品列表和余额信息不变返回该账号原始数据uid1,goodspack1,um。重新计算该用户拥有的物品列表和金额在用户物品余额数据库融合集UGDataBase找到该用户信息并更新在库所Info显示该信息即可实现购物功能。二层SubPageCharging库所user颜色集类型为UserID接收传入的用户IDuid用三层SubPage Query Info实现查询物品余额信息功能库所charging page颜色类型为UserGoodsInfo显示该用户目前拥有的物品和余额进入充值页面选择要充值的金额100、200、300充值成功即会在用户余额中增加相应的金额um200.0完成充值后重新计算该用户拥有的物品列表和金额在用户物品余额数据库融合集UGDataBase找到该用户信息并更新um→um1在库所Info显示充值后的用户信息即可实现充值功能。二层SubPageExit库所Select function颜色集类型为UserID接收传入的用户IDuid在用户ID-密码数据库融合集UserSDateBase找到该用户的ID密码退出到初始库所main。三层SubPageQuery Info与二层SubPage Query Info功能相同库所user颜色集类型为UserID当该库所有token时实现查询物品余额信息功能接收传入的用户IDuid查询用户物品余额数据库UGDataBase融合集并显示该用户拥有的物品和目前的余额如此完成查询操作。总结CPN作为一种形式化方法,得到了广泛的研究与应用。着色petri网的仿真工具CPN Tools支持强大的元语言(ML)具有很强的扩展性。具有易于建模、易于仿真、易于分析的特点,并集成了较为强大的模型检验功能。CPN的内容非常丰富本次的系统建模仅用了其中皮毛的知识建立了一个简单的购物系统模型仿真执行消费者登录购物系统的注册、登录、购物、充值等过程可以以此为基础建模分析更多管理系统的执行过程。