Differences
This shows you the differences between two versions of the page.
Next revision | Previous revisionBoth sides next revision | ||
pn2mc:cov_tina [2014/11/16 18:51] jbiernacki created | pn2mc:cov_tina [2021/09/23 08:51] (current) | ||
---|---|---|---|
Line 1: | Line 1: | ||
- | ====== | + | ====== |
- | ===== Steps required to generate | + | Here is a description of .kts files generation for coverability |
- | - Select the first of the tab pages (// | + | in TINA tool. |
- | - Select //RTCP Nets// option from the combo box. \\ {{: | + | |
- | - Enter direct path of the file to translate or select this file using file browser dialog shown after clicking the button designated with //[...]// symbol. \\ {{: | + | |
- | - Click the // | + | |
- | - NuXmv code after its appearance in the memo can be easily saved to a file by clicking on the //Save// button. \\ {{: | + | |
+ | ===== Steps required to generate coverability graph of a P/T-net in TINA tool ===== | ||
+ | - Load or create PT-net in TINA editor. \\ \\ {{: | ||
+ | - Select // | ||
+ | - In the // | ||
+ | - 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. \\ \\ {{: | ||
+ | - Generated file can be now imported into PetriNet2ModelChecker tool. | ||
**[[: | **[[: |