Differences
This shows you the differences between two versions of the page.
| Both sides previous revisionPrevious revisionNext revision | Previous revisionBoth sides next revision | ||
| pn2mc:features [2014/11/18 22:54] jbiernacki | pn2mc:features [2021/09/23 08:51] (current) | ||
|---|---|---|---|
| Line 11: | Line 11: | ||
| Each one of these tab pages is presented below. | Each one of these tab pages is presented below. | ||
| - | |||
| Line 68: | Line 67: | ||
| ===== RTCP Conversion ===== | ===== RTCP Conversion ===== | ||
| - | ---- | + | This tab page contains features enabling RTCP-nets compilation and generation of their coverability graphs. |
| + | {{: | ||
| + | |||
| + | It looks similar to the other two tab pages. In its top panel there are 4 different types of RTCP-nets processing operations: | ||
| + | |||
| + | * **CPN Tools >> RTCP** - Translation of RTCP-net modelled in CPN tools to original RTCP xml format which can be later compiled by the RTCPNC (RTCP-net compiler). This translation is possible due to integration with cpn2rtcpn tool. | ||
| + | * **RTCP net >> RTCP simulator** - RTCP-net compilation in RTCPNC compiler. As a result of this operation executable jar with simulator of the model is created. User can select the desired location for the output files. | ||
| + | * **RTCP net >> Coverability graph** - Generation of RTCP-net' | ||
| + | * **CPN Tools >> Coverability graph** - Direct conversion from CPN Tools file containig RTCP-net to its coverability graph. This step is concatenation of options 1 and 3. | ||
| + | |||
| + | {{: | ||
| + | |||
| + | |||
| + | In the bottom panel except from the //Save// there is a //Export to pdf// button. Whilst the first one is doing exactly the same thing as in other tab pages, the second one is a feature which enables automatic pdf generation for the coverability graph stored in the memo field. This feature works only if the distribution of Graphviz tool is properly installed on the machine. This feature considerably speeds up the process of model verification because user can immediately see the visual representation of the generated coverability graph. | ||
| + | |||
| + | {{: | ||
| + | |||
| + | After a coverability graph of an RTCP-net is generated it can be used as an input to the translation algorithms and be verified in nuXmv and CADP model checkers. | ||
| + | |||
| + | ---- | ||
| ===== Top menu bar ===== | ===== Top menu bar ===== | ||
| + | |||
| + | Top menu bar contains 4 submenus: | ||
| + | * **File** - containing //Open// and //Exit// buttons. First one of them allows to select a file from a file system - its path appears in the current tab page's //select file// edit. The other is obvious. | ||
| + | * **Parser** - contains translation settings. Currently there is only one parameter that can be set. It is called //omega// and represents the number of tokens which will be treated as infinity during PT-nets coverability graphs translation. | ||
| + | * **RTCP Simulator** - contains options of RTCP-nets compilation and coverability graph generation. Currently there is only one parameter that can be set - RTCP simulation //End time//. It sets maximal virtual time of simulation during coverability graph generation. If this time is reached, coverabilty graph generation will stop. \\ \\ {{: | ||
| + | * **Help** - Contains some basic information about the application. | ||
| + | |||
| ---- | ---- | ||
| **[[: | **[[: | ||