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

  1. Load or create PT-net in TINA editor.



  2. Select reachability analysis option from the Tools menu. It opens a dialog window in which graph generation options are collected.



  3. 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.



  4. 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.



  5. Generated file can be now imported into PetriNet2ModelChecker tool.

Go back