本文提出一个基于层次型着色 Petri网（CPN）的购物系统建模方案。记录一个曾经做过的大作业，当时任课老师讲的很有意思，所以有认真学，这个作业也有在认真的做，课程比较小众，希望给有在刚刚学习的同学作为参考。
建模架构
本Colored Petri Nets用于为购物系统建模，架构为层次型着色Petri网，共分3层。
顶层Page为Main Page，包含Login，Register，Query Info，Shopping，Charging，Exit六个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，不存在返回false
fun member (e,l) =
if l = []
then false
else
if (e = List.hd l)
then true
else member (e,List.tl l);
函数unmember(e,l)，e不在列表l中返回true，存在返回false
fun unmember (e,l) =
if l = []
then true
else
if (e = List.hd l)
then false
else unmember (e,List.tl l);
函数insert (e,l)，e插入到列表l中前面
fun insert (e,l) =
if member (e,l)
then l
else e::l;
每层页面具体分析
顶层Page：Shopping 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。
二层SubPage：Login
库所Login Page颜色集类型为UserInfo，当该库所得到token，用户账号密码，激活变迁Input UserID,UserPw，输入用户ID、用户密码，该token到Verify Password下一步验证该用户密码是否正确，只有该用户的账号uid和密码up与用户账号密码数据库融合集UserSDateBase一致即可激活变迁验证成功，完成登录操作。
二层SubPage：Register
库所Register Page颜色集类型为UserInfo，当该库所得到token，用户账号密码，激活变迁Input输入用户ID、用户密码(uid,up)，将信息记录入用户ID、用户ID-密码、用户物品余额数据库（即将该用户账号uid加入用户账号数据库User融合集、该用户账号uid和密码up加入用户ID-密码数据库UserSDateBase融合集、创建新的用户物品余额信息加入用户物品余额数据库UGDataBase融合集），如此完成该用户注册。
二层SubPage：Query Info
库所user颜色集类型为UserID，当该库所有token时，实现查询物品余额信息功能，接收传入的用户ID（uid），查询用户物品余额数据库UGDataBase融合集，并显示该用户拥有的物品和目前的余额，如此完成查询操作。
二层SubPage：Shopping
库所shopping颜色集类型为UserID，接收传入的用户ID（uid），用三层SubPage Query Info实现查询物品余额信息功能，库所shopping page颜色类型为UserGoodsInfo显示该用户目前拥有的物品和余额，选择要购买的商品Goods，如果该用户余额um大于等于该商品金额gm即可购买，将该商品信息(gid,gname,gm)加入该用户拥有物品列表goodspack1中（goodspack1^^[(gid,gname,gm)]），并扣除该商品金额（um-gm）；若该用户余额小于该商品金额，无法购买，该用户物品列表和余额信息不变，返回该账号原始数据（uid1,goodspack1,um）。重新计算该用户拥有的物品列表和金额，在用户物品余额数据库融合集UGDataBase，找到该用户信息并更新，在库所Info显示该信息，即可实现购物功能。
二层SubPage：Charging
库所user颜色集类型为UserID，接收传入的用户ID（uid），用三层SubPage Query Info实现查询物品余额信息功能，库所charging page颜色类型为UserGoodsInfo显示该用户目前拥有的物品和余额，进入充值页面，选择要充值的金额（100、200、300），充值成功即会在用户余额中增加相应的金额（um+200.0），完成充值后，重新计算该用户拥有的物品列表和金额，在用户物品余额数据库融合集UGDataBase，找到该用户信息并更新（um→um1），在库所Info显示充值后的用户信息，即可实现充值功能。
二层SubPage：Exit
库所Select function颜色集类型为UserID，接收传入的用户ID（uid），在用户ID-密码数据库融合集UserSDateBase，找到该用户的ID密码，退出到初始库所main。
三层SubPage：Query Info
与二层SubPage Query Info功能相同，库所user颜色集类型为UserID，当该库所有token时，实现查询物品余额信息功能，接收传入的用户ID（uid），查询用户物品余额数据库UGDataBase融合集，并显示该用户拥有的物品和目前的余额，如此完成查询操作。
总结
CPN作为一种形式化方法,得到了广泛的研究与应用。着色petri网的仿真工具CPN Tools支持强大的元语言(ML)，具有很强的扩展性。具有易于建模、易于仿真、易于分析的特点,并集成了较为强大的模型检验功能。CPN的内容非常丰富，本次的系统建模仅用了其中皮毛的知识，建立了一个简单的购物系统模型，仿真执行消费者登录购物系统的注册、登录、购物、充值等过程，可以以此为基础建模分析更多管理系统的执行过程。
 agent和组件)