Once a model has been successfully loaded a reachability graph can be built. This graph will display all the states that can be reached and the transitions between them.
There are two ways to obtain a reachability graph for a Petri net. Firstly the state space can be computed by selecting one of the options in the Generate State Space submenu in the file menu. Secondly the reachability graph can be can constructed by loading an ARC file that contains the state transitions in the state space. Also the Load ARC File menu option can be found in the File menu. The ARC File is a text file that can be constructed with tools like SESA or the Movida Model Checker.
The Generate State Space menu contains three options:
Constructing the reachability graph for a large NCES can take several minutes. Also the end result is dependent not only on the NCES but also the ARC file that is used. For example loading an ARC file generated by SESA and generating the state space will in many cases produce different reachability graphs.
Once the state space has been constructed it is displayed in the right-hand side pane. The different states in the graph can then be examined.
If the obtained state space is very large (over 10000 states) drawing the reachability graph can be very time-consuming and degrade the application's performance. Therefore when such a state space is obtained a dialog will be displayed asking if the state space should be drawn. If you press the enter key the graph will be hidden to increase performance. However you can make it visible at any time by checking the menu item Draw state space in the popup menu that is accessible by right-clicking on the reachability graph pane.
After a state space hase been obtained its markings can be computed by selecting the item Compute all markings from the File menu. Computing markings this way can speed up some features and is even required for some tools to be used.
By selecting the option Compute cycles for a state it is possible to compute all the cycles for a given state.