Exploring a state space

In order to explore the state space once it has been generated you may first need to make it visible. To make the state space visible right-click on the reachability graph pane (on the right side of the main window). This will bring up a popup menu. The menu contains the item Draw state space that needs to be checked in order for the state space to be drawn.

To explore individual states in the state space you can click on a state. The marking of that state will now be displayed in the Petri net in the center pane. The selected state will be displayed in green in the reachability graph.

Reachability graph popup menu

To browse through the state space you can invoke the State Space Browser. The State Browser window can be opened by right-clicking on the reachability graph and then selecting State Browser in the popup menu that opens. This will start the state browser with the clicked state as the initial state. If you right-clicked a spot in the reachability graph where there is no state the dialog that is displayed below will appear when you start the state browser. You can then select the initial state from the combo box.

Choosing the starting state

You can also choose to start the Reachability Graph Walker feature which automatically goes through the state transitions of the reachability graph. To start the walker select Start in the popup menu. A dialog will appear where you can set the time interval of the walker's steps. When you want to stop the walker right-click on the reachability graph again and select Stop in the popup menu.

You can also advance in the reachability graph one step at a time in either direction by selecting the option Step forward or Step backwards in the popup menu.

To quickly go to a certain state select the menu item Go to state.... This will open the dialog depicted below. In the dialog you can choose the state to go to and press the OK button. The view will then scroll to show the state and the state will become selected.

Selecting state to
  	go to