====== 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 =====
  - 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]]**