Sidebar

Main

Internal

Trace:

Differences

This shows you the differences between two versions of the page.

--- pn2mc:cov_tina [2014/11/16 18:51]
jbiernacki created
+++ pn2mc:cov_tina [2021/09/23 08:51] (current)
@@ Line 1: / Line 1: @@
-====== Coverability graph export in TINA ======
+====== PT-net coverability graph generation in TINA ======
-===== Steps required to generate coverability graph of a P/T-net in TINA tool =====
+Here is a description of .kts files generation for coverability graphs of P/T-nets modelled
-  - Select the first of the tab pages (//Coverability graph to nuXmv parser//). \\ {{:pn2mc:quickstart:tabs.png|}} \\
+in TINA tool.
-  - Select //RTCP Nets// option from the combo box. \\ {{:pn2mc:quickstart:nettypes.png|}} \\
-  - Enter direct path of  the file to translate or select this file using file browser dialog shown after clicking the button designated with //[...]// symbol. \\ {{:pn2mc:quickstart:selectfile.png?600|}} \\
-  - Click the //Translate// button \\ {{:pn2mc:quickstart:translate.png|}} \\
-  - NuXmv code after its appearance in the memo can be easily  saved to a file by clicking on the //Save// button. \\ {{:pn2mc:quickstart:save.png?600|}} \\
+===== Steps required to generate coverability graph of a P/T-net in TINA tool =====
+  - Load or create PT-net in TINA editor. \\ \\ {{:pn2mc:tina:1.png?400|}} \\ \\
+  - Select //reachability analysis// option from the //Tools// menu. It opens a dialog window in which graph generation options are collected. \\ \\  {{:pn2mc:tina:2.png?400|}} \\ \\
+  - In the //building// section select an option called //coverability graph//. In the //output// section select option //kts (.ktz)// - it will set the proper output format of the generated file. The other option leave with their default values and confirm by clicking //OK// button. \\ \\ {{:pn2mc:tina:3.png?400|}} \\ \\
+  - Text file containing coverability graph of the modelled net will appear in the memo component of the window. Right click on this memo and select //save view// option from the context menu. Select name and location for the file. \\ \\  {{:pn2mc:tina:4.png?400|}} \\ \\
+  - Generated file can be now imported into PetriNet2ModelChecker tool.
 **[[:pn2mc:manual|Go back]]**