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.
- 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 (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.
- 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.
- (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.
- 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)
- 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.
- 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.
