TINA是來自國外的一款功能強大的TIme petri 網(wǎng)絡(luò)分析工具，全稱為：TIme petri Net Analyzer，其主要作用是用于Petri網(wǎng)的編輯和分析，支持包括抑制和讀取弧，TIme Petri網(wǎng)，可能的優(yōu)先級和秒表，以及Time Petri網(wǎng)的數(shù)據(jù)處理擴展，稱為時間轉(zhuǎn)換系統(tǒng)。TINA已經(jīng)在 OLC，然后是Verics，LAAS / CNRS的研究組中開發(fā)。TINA作為運行在WINDOWS系統(tǒng)上的petri網(wǎng)仿真軟件，需要JAVA支持，有需求的用戶請下載使用！

TINA工具箱包含以下工具：

1、nd（NetDraw）：用于Petri網(wǎng)，時間Petri網(wǎng)和自動機的編輯器和GUI。

處理圖形或文字描述的網(wǎng)或自動機。與以下分析工具連接。包括用于網(wǎng)和自動機的繪圖設(shè)備和用于網(wǎng)的步進模擬器。

2、tina：可達性圖的構(gòu)建。

以文字或圖形形式描述的網(wǎng)絡(luò)產(chǎn)生轉(zhuǎn)換系統(tǒng)，以人類可讀形式或以可用模型檢查器和等效檢查器的各種格式抽取其行為。取決于保留的選項，它構(gòu)建：

卡爾普和米勒技術(shù)的Petri網(wǎng)的可維度圖。

有界Petri網(wǎng)的標記圖。

通過[6] [7]的覆蓋步驟方法，持久集的方法或它們的幾種組合在[8]中解釋的Petri網(wǎng)的部分標記圖。

遵循[1] [2] [3] [5]中討論的技術(shù)，對時間Petri網(wǎng)（狀態(tài)類圖）進行各種狀態(tài)空間抽象。根據(jù)選擇的選項，該結(jié)構(gòu)保留時間Petri網(wǎng)的具體狀態(tài)空間的標記，狀態(tài)，LTL屬性或CTL *屬性。

3、sift：可達性圖的構(gòu)造和檢查。

Sift是tina的一個專門版本，支持可達性屬性的動態(tài)驗證。如果提供的選項比蒂娜少，但速度通常更快，并且需要的空間更少。

4、struct：網(wǎng)的結(jié)構(gòu)分析。

計算半流的發(fā)電機組或在Petri網(wǎng)的位置和/或轉(zhuǎn)換處的流量。也決定了不變性和一致性。

5、plan：路徑分析。

計算一些給定的發(fā)射序列上的全部或單個定時發(fā)射序列（時間表）。也可以計算最快和最慢的路徑。

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

以批處理或交互模式運行。模型根據(jù)S / E LTL公式檢查由上面的tina或篩選工具構(gòu)建的kripke轉(zhuǎn)換系統(tǒng)。接受豐富的語言，允許顯著地聲明新的操作符或重新定義現(xiàn)有的操作符（以便實際上可以不加改變地加載可用的庫）。生成的計數(shù)器示例可以以可加載到nd模擬器的格式保存，以便重放。為了將公式轉(zhuǎn)換成Buchi自動機，selt依賴于ltl2ba。

7、muse：模態(tài)mu-calculus模型檢查器。

（進行中）以批處理或交互模式進行操作。模型檢查通過上面的tina或篩選工具構(gòu)建的kripke轉(zhuǎn)換系統(tǒng)與模態(tài)mu-演算公式。接受豐富的語言，明顯地宣布新運營商或重新定義現(xiàn)有運營商。繆斯計算一系列服從一些公式的國家。然后可以使用pathto和plan工具計算某個狀態(tài)的路徑，并使用工具播放或nd步進器在模型上重播該路徑。

8、play：步進模擬器。

允許以交互方式進行模擬，并以tina接受的所有格式逐步進行網(wǎng)絡(luò)描述。它的功能與nd步進器的功能相似，除了速度更快并且可以模擬時間轉(zhuǎn)換系統(tǒng)。

9、pathto：路徑查找器。

計算kripke轉(zhuǎn)換系統(tǒng)中某些狀態(tài)路徑的實用工具。

10、ndrio：時間Petri網(wǎng)的轉(zhuǎn)換工具。

在Tina格式.net，.ndr，.tpn和.pnml交換格式之間進行轉(zhuǎn)換。

11、ktzio：Kripke轉(zhuǎn)換系統(tǒng)的轉(zhuǎn)換工具。

將Tina .ktz格式轉(zhuǎn)換為CADP格式.aut，.bcg和MEC4格式.mec。

12、frac：Fiacre到tina tts編譯器。

Fiacre是用于實時系統(tǒng)的高級描述語言; 壓裂將Fiacre描述編譯成大多數(shù)TINA工具接受的時間轉(zhuǎn)換系統(tǒng)（tts）。由于它的移動速度與蒂娜不同，因此壓裂不會與工具箱一起分發(fā)，而是通過專用的Fiacre站點提供。

更新日志

TINA 3.4.4更新：

1、現(xiàn)在通過篩選和播放來處理異常，而不是通過tts庫處理，并提供更多有用的錯誤消息。