TINA(TIme petri 网络分析工具)

TINA是一款源自国外的Petri网分析工具，全称TIme petri Net Analyzer，主要用于Petri网的建模、仿真与验证。它由OLC、Verics以及LAAS/CNRS研究团队逐步开发而成，运行在Windows系统上并依赖Java环境。软件提供了图形化编辑器与多种分析模块，能处理普通Petri网、时间Petri网以及自动机模型。界面设计简洁，操作逻辑清晰，适合需要做形式化分析与模型检查的用户使用。

核心编辑与仿真环境

1、 nd（NetDraw）模块负责Petri网、时间Petri网和自动机的编辑与图形界面展示

2、 支持图形化绘制或文字描述两种方式创建网与自动机模型

3、 内置步进模拟器，可对网络进行逐步仿真与状态观察

4、 可与后续分析工具直接连接，形成从建模到验证的完整流程

模型检查与专用工具

- Sift是TINA的专用版本，侧重可达性属性的动态验证，选项较少但速度更快、占用空间更小

- 模型可依据S/E LTL公式对Kripke转换系统进行检查，支持批处理或交互模式

- 公式语言丰富，允许声明新操作符或重定义已有操作符，便于加载现有库

- 生成的计数器示例可保存为nd模拟器可加载的格式，方便重放分析

- Selt依赖ltl2ba将公式转换为Buchi自动机

- muse是模态mu演算模型检查器，同样支持批处理与交互模式，可计算满足公式的状态集

- pathto和plan工具可计算某状态的路径，并用play或nd步进器在模型上重播

格式转换与外部语言支持

- ndrio用于时间Petri网的格式转换，支持.net、.ndr、.tpn和.pnml交换格式

- ktzio可将Tina的.ktz格式转换为CADP的.aut、.bcg以及MEC4的.mec格式

- frac是Fiacre到TINA tts的编译器，Fiacre是一种面向实时系统的高级描述语言

- frac将Fiacre描述编译为多数TINA工具可接受的时间转换系统（tts）

- 由于frac更新节奏与TINA不同，它不随工具箱分发，而是通过Fiacre专用站点获取

运行方式与使用特点

1、 多个工具均支持批处理与交互两种运行模式，适应不同使用习惯

2、 步进模拟器允许以交互方式按TINA支持的所有格式逐步模拟网络描述

3、 该模拟器功能与nd步进器相近，但速度更快，且能模拟时间转换系统

4、 整体界面干净简洁，操作便捷，适合需要快速上手Petri网分析的用户