====== CP-net reachability graph generation in CPN Tools ======

Here is a description of reachability graphs generation for CP-nets modelled in CPN Tools.

===== Steps required to generate reachability graph of a CP-net in CPN Tools =====

  - 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|}} \\ \\ 
  - //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|}} \\ \\ 
  - 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. \\ \\ 
  - The //Aux// toolkit will be used to write a short function generating list of edges of the reachability graph. \\ \\  {{:pn2mc:cpntools:p6.png|}} \\ \\ 
  - 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|}} \\ \\ 
  - 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.





**[[:pn2mc:manual|Go back]]**