TINA(TIme petri 网络分析工具) v3.4.4 官方安装版

TINA是来自国外的一款功能强大的TIme petri 网络分析工具，全称为：TIme petri Net Analyzer，其主要作用是用于Petri网的编辑和分析，支持包括抑制和读取弧，TIme Petri网，可能的优先级和秒表，以及Time Petri网的数据处理扩展，称为时间转换系统。TINA已经在 OLC，然后是Verics，LAAS / CNRS的研究组中开发。TINA作为运行在WINDOWS系统上的petri网仿真软件，需要JAVA支持，有需求的用户请下载使用！

TINA工具箱包含以下工具：

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网的位置和/或转换处的流量。也决定了不变性和一致性。

5、plan：路径分析。

计算一些给定的发射序列上的全部或单个定时发射序列（时间表）。也可以计算最快和最慢的路径。

6、selt：州/事件LTL模型检查器。

以批处理或交互模式运行。模型根据S / E LTL公式检查由上面的tina或筛选工具构建的kripke转换系统。接受丰富的语言，允许显着地声明新的操作符或重新定义现有的操作符（以便实际上可以不加改变地加载可用的库）。生成的计数器示例可以以可加载到nd模拟器的格式保存，以便重放。为了将公式转换成Buchi自动机，selt依赖于ltl2ba。

7、muse：模态mu-calculus模型检查器。

（进行中）以批处理或交互模式进行操作。模型检查通过上面的tina或筛选工具构建的kripke转换系统与模态mu-演算公式。接受丰富的语言，明显地宣布新运营商或重新定义现有运营商。缪斯计算一系列服从一些公式的国家。然后可以使用pathto和plan工具计算某个状态的路径，并使用工具播放或nd步进器在模型上重播该路径。

8、play：步进模拟器。

允许以交互方式进行模拟，并以tina接受的所有格式逐步进行网络描述。它的功能与nd步进器的功能相似，除了速度更快并且可以模拟时间转换系统。

9、pathto：路径查找器。

计算kripke转换系统中某些状态路径的实用工具。

10、ndrio：时间Petri网的转换工具。

在Tina格式.net，.ndr，.tpn和.pnml交换格式之间进行转换。

11、ktzio：Kripke转换系统的转换工具。

将Tina .ktz格式转换为CADP格式.aut，.bcg和MEC4格式.mec。

12、frac：Fiacre到tina tts编译器。

Fiacre是用于实时系统的高级描述语言; 压裂将Fiacre描述编译成大多数TINA工具接受的时间转换系统（tts）。由于它的移动速度与蒂娜不同，因此压裂不会与工具箱一起分发，而是通过专用的Fiacre站点提供。

更新日志

TINA 3.4.4更新：

1、现在通过筛选和播放来处理异常，而不是通过tts库处理，并提供更多有用的错误消息。