Sidebar

Main

Internal

Trace:

Differences

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

--- pn2mc:cov_tina [2014/11/16 19:00]
jbiernacki
+++ 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 ======
+Here is a description of .kts files generation for coverability graphs of P/T-nets modelled
+in TINA tool.
 ===== Steps required to generate coverability graph of a P/T-net in TINA tool =====
-  - Select the first of the tab pages (//Coverability graph to nuXmv parser//). \\ {{:pn2mc:cpntools:tina:1.png|}} \\
+  - 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]]**