Sidebar

Main

Internal

Trace:
Trace:

Differences

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

Link to this comparison view

Both sides previous revisionPrevious revision
Next revision		Previous revision
Both sides next revision
pn2mc:cov_cpntools [2014/11/16 20:09]
jbiernacki 		pn2mc:cov_cpntools [2021/09/23 08:51] (current)
Line 1: Line 1:
-====== Reachability graph generation in CPN Tools ======+====== CP-net reachability graph generation in CPN Tools ======
  
 Here is a description of reachability graphs generation for CP-nets modelled in CPN Tools. Here is a description of reachability graphs generation for CP-nets modelled in CPN Tools.
Line 6: Line 6:
  
   - Load or create a CP-net in CPN Tools editor. \\ \\ {{:pn2mc:cpntools:p1.png?400|}} \\ \\    - Load or create a CP-net in CPN Tools editor. \\ \\ {{:pn2mc:cpntools:p1.png?400|}} \\ \\ 
-  - Reachability graph generation options can be found in the //State space// toolkit \\ \\  {{:pn2mc:cpntools:p2.png|}} \\ \\  +  - Reachability graph generation options can be found in the //State space// toolkit. \\ \\  {{:pn2mc:cpntools:p2.png|}} \\ \\  
-  - //Calculate State Space// tool has some settings which can limit the maximum number of nodes (//nodestop//) or arcs (//arcstop//) of the generated reachability graph. Setting this limit can be a good idea due to the fact that many CP-net models have enormous or even infinite reachability graphs. These options are available in the context menu of the //Calculate State Space// tool \\ \\ {{:pn2mc:cpntools:p3.png?400|}} \\ \\  +  - //Calculate State Space// tool has some settings which can limit the maximum number of nodes (//nodestop//) or arcs (//arcstop//) of the generated reachability graph. Setting this limit can be a good idea due to the fact that many CP-net models have enormous or even infinite reachability graphs. These options are available in the context menu of the //Calculate State Space// tool. \\ \\ {{:pn2mc:cpntools:p3.png?400|}} \\ \\  
-  - In order to calculate the state space of the net select //Calculate State Space// tool and click on the page containing the model\\ \\  {{:pn2mc:cpntools:p4.png?400|}} \\ \\ +  - In order to calculate the state space of the net select //Calculate State Space// tool and click on the page containing the model. \\ \\  {{:pn2mc:cpntools:p4.png?400|}} \\ \\ 
   - The next step is to select //Calculate SCC Graph// tool and again click on the page containing the net. \\ \\  {{:pn2mc:cpntools:p5.png?400|}} \\ \\    - The next step is to select //Calculate SCC Graph// tool and again click on the page containing the net. \\ \\  {{:pn2mc:cpntools:p5.png?400|}} \\ \\ 
   - (Optionally) create a new page in which reachability graph will be drawn. \\ \\    - (Optionally) create a new page in which reachability graph will be drawn. \\ \\ 
Line 14: Line 14:
   - From the //Aux// toolkit select //Text// tool and add it to the page. In the field that will appear on the page input the  following text: \\ \\ ''EvalAllArcs (fn arc => arc)'' \\ \\ {{:pn2mc:cpntools:p7.png?400|}} \\ \\    - From the //Aux// toolkit select //Text// tool and add it to the page. In the field that will appear on the page input the  following text: \\ \\ ''EvalAllArcs (fn arc => arc)'' \\ \\ {{:pn2mc:cpntools:p7.png?400|}} \\ \\ 
   - In this step //Display partial state space// tool will be used. Before use, make sure that its option called //Nodes in the list// is **UNCHECKED** (by default it is checked) -  it will make the tool to interpret input list as the list of edges and not list of nodes. \\ \\  {{:pn2mc:cpntools:p8.png|}} \\ \\    - In this step //Display partial state space// tool will be used. Before use, make sure that its option called //Nodes in the list// is **UNCHECKED** (by default it is checked) -  it will make the tool to interpret input list as the list of edges and not list of nodes. \\ \\  {{:pn2mc:cpntools:p8.png|}} \\ \\ 
 +  - With the  //Display partial state space// tool selected click on the code prepared in step 8.  \\ \\  {{:pn2mc:cpntools:p9.png?400|}} \\ \\  
 +  - Reachability graph will be drawn on the selected page. State marking is shawn after clicking on the little triangle in the corner of the node.  \\ \\  {{:pn2mc:cpntools:p10.png?400|}} \\ \\ 
 +  - Generated reachability graph will be saved in the model file. It can be then loaded into PetriNet2ModelChecker tool.
  
  
© Marcin Szpyrka 2008-2024