It is possible to invoke several integrated tools from the NCES Analyzer. These tools can be accessed via the Tools menu.
One of the sub applications accessible from the NCES Analyzer is the GUHA Analysis application. Before this application can be launched an NCES must have been loaded, a state space obtained and all markings computed. The application can then be started by selecting the GUHA models menu option from the Tools menu.
It is also possible to start the Reachability Graph Walker feature from the tools menu by selecting the Setup RG Walk menu option. To use the Walker a reachability graph must have been obtained. To stop the Walker select the Stop RG Walk menu option.
The Time Diagram application can be started by selecting the option Time diagram from the Tools menu. Before this feature can be started a reachability graph must have been obtained.
To reduce the size of the considered reachability graph the Analysis Bounds Editor can be utilized. The Bounds Editor can also be used to build constrained state spaces even if no state space has yet been constructed. To start the editor select the menu option Bounded Analysis from the Tools menu.
Also the Model Checker application can be invoked from the Tools menu. It works as an independent application and does not require any TNCES model to be loaded in the NCES Analyzer. To start the Model Checker select the option Model-checker from the Tools menu.
One can also invoke just the CTL-formula checking sub GUI of the Model Checker to check CTL-formulas in the obtained state space. To check CTL-formulas select the Check CTL formulae option in the Tools menu.
To visualize the functioning of the system the Simulator application can be started. To start the visualization tool select the menu option Simulator from the Tools menu.
The menu option Structural Reasoner provides an interface to the Structural Reasoner application. Note that before using the Structural Reasoner you must have computed markings by selecting the menu option Compute all markings from the Tools menu. The interface consists of the dialog window displayed below:
The window contains a table that is used for creating properties. The second column in the table contains the flatfile numbers of the NCES places. You can select the places to create properties from by checking the corresponding check boxes in the first column. You can specify names for the properties in the third column. The value in the third column indicates how many tokens the place should have in order for the property to hold.
Press the Save network button to create an XML file containing a Structural Reasoner project. The project will contain a network corresponding to the current reachability graph. Also the created properties will be assigned to the nodes if they hold in the corresponding states of the state space.
Press the Invoke SR button to start Structural Reasoner. From Structural Reasoner it is possible to load project files created with the window.
Pressing the Close button closes the dialog window.
In the upper part of the NCES Analyzer window there is a Formula text field where it is possible write simple marking formulas.
To check a marking formula write it in the text field and then press the button with the ? label. Now the combo box to the right of the button contains all of the states where the formula holds. When you select one of the states in this dropdown menu the NCES frame is updated so that it shows the marking in that state. Also the reachability graph view is centered so that it shows the selected state.
As a special case it is possible to search for deadlock states in the current state space by writing the word DEADLOCKS in the formula text field. Now all states that are deadlocks are displayed in the combo box. Another way to find the deadlocks is to select the menu item Find deadlocks in the Tools menu.