CP-net reachability graph generation in CPN Tools

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

1. Load or create a CP-net in CPN Tools editor.
   
   
   
   
2. Reachability graph generation options can be found in the State space toolkit.
   
   
   
   
3. 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.
   
   
   
   
4. In order to calculate the state space of the net select Calculate State Space tool and click on the page containing the model.
   
   
   
   
5. The next step is to select Calculate SCC Graph tool and again click on the page containing the net.
   
   
   
   
6. (Optionally) create a new page in which reachability graph will be drawn.
   
   
7. The Aux toolkit will be used to write a short function generating list of edges of the reachability graph.
   
   
   
   
8. 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)
   
   
   
   
9. 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.
   
   
   
   
10. With the Display partial state space tool selected click on the code prepared in step 8.
    
    
    
    
11. 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.
    
    
    
    
12. Generated reachability graph will be saved in the model file. It can be then loaded into PetriNet2ModelChecker tool.

Go back