TINA(TIme petri 网络分析工具)

TINA电脑版是一款强大的时间Petri网分析工具，全称为TIme Petri Net Analyzer。该软件主要用于编辑和分析Petri网，支持抑制和读取弧的功能，能够处理时间功能，包括优先级和计时器。TINA还具备时间转换系统，可以对时间Petri网进行深入的数据处理。该软件在OLC、Verics及LAAS/CNRS研究组开发，专门为Windows系统设计，并需要Java支持。TINA提供了编辑器和图形用户界面（GUI），用于可达性图的创建和验证，结构分析，路径分析，以及多种模型检查工具，如LTL和模态mu-calculus检查器。此外，它还具备步进模拟器、路径查找器以及各类转换工具，包括时间Petri网和Fiacre到TINA TTS的编译器。界面友好，操作简便，感兴趣的用户可以下载体验。

软件特色

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站点提供。