Differences
This shows you the differences between two versions of the page.
| Next revision | Previous revisionBoth sides next revision | ||
| pn2mc:cov_cpntools [2014/11/16 20:06] jbiernacki created | pn2mc:cov_cpntools [2021/09/23 08:51] (current) | ||
|---|---|---|---|
| Line 1: | Line 1: | ||
| - | ====== | + | ====== |
| 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. \\ \\ {{: | - Load or create a CP-net in CPN Tools editor. \\ \\ {{: | ||
| - | - Reachability graph generation options can be found in the //State space// toolkit \\ \\ {{: | + | - Reachability graph generation options can be found in the //State space// toolkit. \\ \\ {{: |
| - | - //Calculate State Space// tool has some settings which can limit the maximum number of nodes (// | + | - //Calculate State Space// tool has some settings which can limit the maximum number of nodes (// |
| - | - In order to calculate the state space of the net select //Calculate State Space// tool and click on the page containing the model\\ \\ {{: | + | - In order to calculate the state space of the net select //Calculate State Space// tool and click on the page containing the model. \\ \\ {{: |
| - The next step is to select //Calculate SCC Graph// tool and again click on the page containing the net. \\ \\ {{: | - The next step is to select //Calculate SCC Graph// tool and again click on the page containing the net. \\ \\ {{: | ||
| - (Optionally) create a new page in which reachability graph will be drawn. \\ \\ | - (Optionally) create a new page in which reachability graph will be drawn. \\ \\ | ||
| - | - The //Aux// toolkit will be used to write a short function generating list of edges of the reachability graph.\\ \\ {{: | + | - The //Aux// toolkit will be used to write a short function generating list of edges of the reachability graph. \\ \\ {{: |
| - 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: \\ \\ '' | - 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: \\ \\ '' | ||
| - | - 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). | + | - 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) |
| + | - With the //Display partial state space// tool selected click on the code prepared in step 8. \\ \\ {{: | ||
| + | - 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. \\ \\ {{: | ||
| + | - Generated reachability graph will be saved in the model file. It can be then loaded into PetriNet2ModelChecker tool. | ||