TINA电脑版是一款来自国外的功能强大的TIme petri 网络分析工具。全称为：TIme petri Net Analyzer，该软件主要作用是用于Petri网的编辑和分析。该软件支持包括抑制和读取弧。TIme Petri网，可能优先级和秒表，以及Time Petri网的数据处理扩展，称为时间转换系统。该软件已经在 OLC，然后是Verics，LAAS / CNRS的研究组中开发。TINA电脑版作为运行在WINDOWS系统上的petri网仿真软件，需要JAVA支持。TIAN用于Petri网，时间Petri网和自动机的编辑器和GUI，可达性图的构建，可达性图的构造和检查，网的结构分析，路径分析，州/事件LTL模型检查器，模态mu-calculus模型检查器，步进模拟器，路径查找器，时间Petri网的转换工具，Kripke转换系统的转换工具，Fiacre到tina tts编译器。TINA电脑版界面简洁干净，操作也很便捷。有需要的用户可以下载体验！

INA(TIme petri 网络分析工具)特色

1、nd（NetDraw）：用于Petri网，时间Petri网和自动机的编辑器和GUI
处理图形或文字描述的网或自动机。与以下分析工具连接。包括用于网和自动机的绘图设备和用于网的步进模拟器。
2、tina：可达性图的构建
以文字或图形形式描述的网络产生转换系统，以人类可读形式或以可用模型检查器和等效检查器的各种格式抽取其行为。取决于保留的选项，它构建：
卡尔普和米勒技术的Petri网的可维度图。
有界Petri网的标记图。
通过[6] [7]的覆盖步骤方法，持久集的方法或它们的几种组合在[8]中解释的Petri网的部分标记图。
遵循[1] [2] [3] [5]中讨论的技术，对时间Petri网（状态类图）进行各种状态空间抽象。根据选择的选项，该结构保留时间Petri网的具体状态空间的标记，状态，LTL属性或CTL *属性。
3、sift：可达性图的构造和检查
Sift是tina的一个专门版本，支持可达性属性的动态验证。如果提供的选项比蒂娜少，但速度通常更快，并且需要的空间更少。
4、struct：网的结构分析
计算半流的发电机组或在Petri网的位置和/或转换处的流量。也决定了不变性和一致性。

软件亮点

1、plan：路径分析
计算一些给定的发射序列上的全部或单个定时发射序列（时间表）。也可以计算最快和最慢的路径。
2、selt：州/事件LTL模型检查器
以批处理或交互模式运行。模型根据S / E LTL公式检查由上面的该软件或筛选工具构建的kripke转换系统。接受丰富的语言，允许显着地声明新的操作符或重新定义现有的操作符（以便实际上可以不加改变地加载可用的库）。生成的计数器示例可以以可加载到nd模拟器的格式保存，以便重放。为了将公式转换成Buchi自动机，selt依赖于ltl2ba。
3、muse：模态mu-calculus模型检查器
（进行中）以批处理或交互模式进行操作。模型检查通过上面的该软件或筛选工具构建的kripke转换系统与模态mu-演算公式。接受丰富的语言，明显地宣布新运营商或重新定义现有运营商。缪斯计算一系列服从一些公式的国家。然后可以使用pathto和plan工具计算某个状态的路径，并使用工具播放或nd步进器在模型上重播该路径。
4、play：步进模拟器。
允许以交互方式进行模拟，并以该软件接受的所有格式逐步进行网络描述。它的功能与nd步进器的功能相似，除了速度更快并且可以模拟时间转换系统。

软件优势

1、pathto：路径查找器
计算kripke转换系统中某些状态路径的实用工具。
2、ndrio：时间Petri网的转换工具
在其式.net，.ndr，.tpn和.pnml交换格式之间进行转换。
3、ktzio：Kripke转换系统的转换工具
将Tina .ktz格式转换为CADP格式.aut，.bcg和MEC4格式.mec。
4、frac：Fiacre到tina tts编译器
Fiacre是用于实时系统的高级描述语言; 压裂将Fiacre描述编译成大多数该软件工具接受的时间转换系统（tts）。由于它的移动速度与蒂娜不同，因此压裂不会与工具箱一起分发，而是通过专用的Fiacre站点提供。