TINA電腦版是一款來(lái)自國(guó)外的功能強(qiáng)大的TIme petri 網(wǎng)絡(luò)分析工具。全稱為：TIme petri Net Analyzer，該軟件主要作用是用于Petri網(wǎng)的編輯和分析。該軟件支持包括抑制和讀取弧。TIme Petri網(wǎng)，可能優(yōu)先級(jí)和秒表，以及Time Petri網(wǎng)的數(shù)據(jù)處理擴(kuò)展，稱為時(shí)間轉(zhuǎn)換系統(tǒng)。該軟件已經(jīng)在 OLC，然后是Verics，LAAS / CNRS的研究組中開發(fā)。TINA電腦版作為運(yùn)行在WINDOWS系統(tǒng)上的petri網(wǎng)仿真軟件，需要JAVA支持。TIAN用于Petri網(wǎng)，時(shí)間Petri網(wǎng)和自動(dòng)機(jī)的編輯器和GUI，可達(dá)性圖的構(gòu)建，可達(dá)性圖的構(gòu)造和檢查，網(wǎng)的結(jié)構(gòu)分析，路徑分析，州/事件LTL模型檢查器，模態(tài)mu-calculus模型檢查器，步進(jìn)模擬器，路徑查找器，時(shí)間Petri網(wǎng)的轉(zhuǎn)換工具，Kripke轉(zhuǎn)換系統(tǒng)的轉(zhuǎn)換工具，F(xiàn)iacre到tina tts編譯器。TINA電腦版界面簡(jiǎn)潔干凈，操作也很便捷。有需要的用戶可以下載體驗(yàn)！

INA(TIme petri 網(wǎng)絡(luò)分析工具)特色

1、nd（NetDraw）：用于Petri網(wǎng)，時(shí)間Petri網(wǎng)和自動(dòng)機(jī)的編輯器和GUI
處理圖形或文字描述的網(wǎng)或自動(dòng)機(jī)。與以下分析工具連接。包括用于網(wǎng)和自動(dòng)機(jī)的繪圖設(shè)備和用于網(wǎng)的步進(jìn)模擬器。
2、tina：可達(dá)性圖的構(gòu)建
以文字或圖形形式描述的網(wǎng)絡(luò)產(chǎn)生轉(zhuǎn)換系統(tǒng)，以人類可讀形式或以可用模型檢查器和等效檢查器的各種格式抽取其行為。取決于保留的選項(xiàng)，它構(gòu)建：
卡爾普和米勒技術(shù)的Petri網(wǎng)的可維度圖。
有界Petri網(wǎng)的標(biāo)記圖。
通過(guò)[6] [7]的覆蓋步驟方法，持久集的方法或它們的幾種組合在[8]中解釋的Petri網(wǎng)的部分標(biāo)記圖。
遵循[1] [2] [3] [5]中討論的技術(shù)，對(duì)時(shí)間Petri網(wǎng)（狀態(tài)類圖）進(jìn)行各種狀態(tài)空間抽象。根據(jù)選擇的選項(xiàng)，該結(jié)構(gòu)保留時(shí)間Petri網(wǎng)的具體狀態(tài)空間的標(biāo)記，狀態(tài)，LTL屬性或CTL *屬性。
3、sift：可達(dá)性圖的構(gòu)造和檢查
Sift是tina的一個(gè)專門版本，支持可達(dá)性屬性的動(dòng)態(tài)驗(yàn)證。如果提供的選項(xiàng)比蒂娜少，但速度通常更快，并且需要的空間更少。
4、struct：網(wǎng)的結(jié)構(gòu)分析
計(jì)算半流的發(fā)電機(jī)組或在Petri網(wǎng)的位置和/或轉(zhuǎn)換處的流量。也決定了不變性和一致性。

軟件亮點(diǎn)

1、plan：路徑分析
計(jì)算一些給定的發(fā)射序列上的全部或單個(gè)定時(shí)發(fā)射序列（時(shí)間表）。也可以計(jì)算最快和最慢的路徑。
2、selt：州/事件LTL模型檢查器
以批處理或交互模式運(yùn)行。模型根據(jù)S / E LTL公式檢查由上面的該軟件或篩選工具構(gòu)建的kripke轉(zhuǎn)換系統(tǒng)。接受豐富的語(yǔ)言，允許顯著地聲明新的操作符或重新定義現(xiàn)有的操作符（以便實(shí)際上可以不加改變地加載可用的庫(kù)）。生成的計(jì)數(shù)器示例可以以可加載到nd模擬器的格式保存，以便重放。為了將公式轉(zhuǎn)換成Buchi自動(dòng)機(jī)，selt依賴于ltl2ba。
3、muse：模態(tài)mu-calculus模型檢查器
（進(jìn)行中）以批處理或交互模式進(jìn)行操作。模型檢查通過(guò)上面的該軟件或篩選工具構(gòu)建的kripke轉(zhuǎn)換系統(tǒng)與模態(tài)mu-演算公式。接受豐富的語(yǔ)言，明顯地宣布新運(yùn)營(yíng)商或重新定義現(xiàn)有運(yùn)營(yíng)商。繆斯計(jì)算一系列服從一些公式的國(guó)家。然后可以使用pathto和plan工具計(jì)算某個(gè)狀態(tài)的路徑，并使用工具播放或nd步進(jìn)器在模型上重播該路徑。
4、play：步進(jìn)模擬器。
允許以交互方式進(jìn)行模擬，并以該軟件接受的所有格式逐步進(jìn)行網(wǎng)絡(luò)描述。它的功能與nd步進(jìn)器的功能相似，除了速度更快并且可以模擬時(shí)間轉(zhuǎn)換系統(tǒng)。

軟件優(yōu)勢(shì)

1、pathto：路徑查找器
計(jì)算kripke轉(zhuǎn)換系統(tǒng)中某些狀態(tài)路徑的實(shí)用工具。
2、ndrio：時(shí)間Petri網(wǎng)的轉(zhuǎn)換工具
在其式.net，.ndr，.tpn和.pnml交換格式之間進(jìn)行轉(zhuǎn)換。
3、ktzio：Kripke轉(zhuǎn)換系統(tǒng)的轉(zhuǎn)換工具
將Tina .ktz格式轉(zhuǎn)換為CADP格式.aut，.bcg和MEC4格式.mec。
4、frac：Fiacre到tina tts編譯器
Fiacre是用于實(shí)時(shí)系統(tǒng)的高級(jí)描述語(yǔ)言; 壓裂將Fiacre描述編譯成大多數(shù)該軟件工具接受的時(shí)間轉(zhuǎn)換系統(tǒng)（tts）。由于它的移動(dòng)速度與蒂娜不同，因此壓裂不會(huì)與工具箱一起分發(fā)，而是通過(guò)專用的Fiacre站點(diǎn)提供。