Sidebar

Main

Internal

Trace:

Differences

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

--- pn2mc:features [2014/11/19 21:12]
jbiernacki [RTCP Conversion]
+++ pn2mc:features [2021/09/23 08:51] (current)
@@ Line 81: / Line 81: @@
+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.
 {{:pn2mc:features:rtcp3.png?400|}}
+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 contains 4 submenus:
-  * **File** - containing //Open// and //Exit// buttons. The 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.  \\ \\
+  * **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.  \\ {{:pn2mc:features:settings2.png?200|}}   {{:pn2mc:features:settings1.png?200|}} \\ \\
   * **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. \\ \\ {{:pn2mc:features:settings3.png?200|}} \\ \\