CPN Tools(着色petri网工具)

CPN Tools官方版是来自丹麦的奥尔胡斯大学的一款专用于有色Petri网编辑、模拟和分析的工具。CPN即Colored Petri nets的缩写，它提供的分层建模工具、时间颜色集表示以及自动分析工具使得HTCPN方法可以应用于安全协议的自动分析中。

值得一提的是，CPN Tools还具有增量语法检查和代码生成功能，不仅可在网络构建时进行，快速模拟器可有效处理不定时和定时网络，还可以生成和分析完整和部分状态空间，为用户提供标准状态空间报告包含诸如有界性属性和活性属性之类的信息，软件并且仍在不断地完善中，有需求的用户请下载体验！

软件功能

1、对需要的着色petri网进行模型的建立。

2、并且还对拥有时间、分层的着色petri网建立模型进行支持。

3、对用户经常使用的CPN ML编程语言支持。

4、根据自己的需求对颜色进行选择，包括了对时间的设置。

5、层次化的建模支持，对各种丰富的模型分析工具进行提供。

6、内置的监视器相当的实用，完成对空间状态的分析等。

软件特色

1、第三部分扩展。

2、非彩色网的简化使用。

3、支持出口到PNML。

4、支持实时和彩色集。

5、改进的时间支持(时间间隔和状态空间缩减)。

6、简化状态空间分析。

CPN Tools简易教程

CPN Tools功能丰富，其教程并不是一个范例就能概括，小编这里使用CPN Tools工具做一个登录模型作为说明，更过功能请参照CPN Tools的帮助文档。

提示：CPN Tools是需要JAVA环境的，所以记得提前配好JAVA环境程序才能正常运行。

1、首先打开CPN Tools程序，点击右键选择New Net，这样就新建了一个Net

2、把工具箱中的Create和Simulation拖到面板上

3、画place和transition及其连接

①在左侧Declarations下定义声明，右击Declarations新建decl 

②新建红色框里的decl（前后顺序不能乱）

  ③给place和transition中写上名字send，p1，receive

④选中send点击键盘上的Tab键把出现的UNIT改成INTxData，然后同样选中receive点击键盘上的Tab键把出现的UNIT改成DATA

⑤点击第一条带箭头的线，把expr改成（n，p），点击第二条带箭头的线，把expr改成if n=3 andalso p=”three” then “success” else “fail”（这句话的意思是如果用户名是3，密码是three则登录成功显示success，否则登录失败fail）

4、初始化数据

①选中send点击键盘上的Tab键两下，把出现的INIT MARK改成

②点击Sim工具中的箭头运行

5、至此一个简单的登录模型就完成了

更新日志

v4.0.1版本

1、声明约束

2、位置转换Petri网

3、新类型（IntInf，real，time）

4、次要功能

.模型统计

.模拟停止标准

.简化的状态空间分析

5、消息序列图

6、时间间隔和时间缩短

7、扩展：

.基本

.入门和基本抽象

.图形和回调