This section explains how you can add CTL formulas and check them in the NCES. That is, the basic functionality of the formula list sub user interface.
The formula list sub user interface is depicted below.There are two ways to enter CTL formulas to the table. You can either write them by hand or load them from a file.
To enter a single CTL formula write it into the text area in the bottom of the window and click the Add button. The formula will be added to the table unless it has grammatical errors.
To load CTL formulas from a file choose Load CTL formulae... from the File menu. From the navigator choose a file that contains the CTL formulas to be loaded. The file must have 'ctl' as its extension. Only those of the formulas in the file that are well-formed will be added to the list.
All entered CTL formulas must adhere to the supported CTL syntax.
You can either select formula rows one by one or select all of the formulas at once. To select a formula row click the check box in the second column of the row. Selected rows have a tick in their check box. To mark all formulas in the table as selected select Select all from the Edit menu.
To remove a formula from the table move the mouse pointer over the formula row and click the right mouse
button to bring up a popup menu. The popup menu is depicted below and has two choices: Check and Delete.
Select Delete and the formula row will be removed from the table.
You can also remove groups of formula rows at once. To do so first select the rows that you want to delete. Then choose the menu item Delete selected from the Edit menu.
You can save all the formulas currently entered on the table to a file on the disk. After saving the file will contain exactly those formulas on the list and all previous contents will be overwritten. To save the formulas select Save CTL formulae... from the File menu and choose the file to save to.
Once a CTL formula has been entered into the formula list table its truth value in the computed state space can be checked. You can either check formulas one by one or select a group of formulas to be checked at a single time.
To check a single formula move the mouse pointer over its row in the table and click the right mouse button. A popup menu will appear with two choises: Check and Delete. Select Check and a model checking algorithm will be executed for the corresponding formula. Once the algorithm finishes its truth value will appear in the third column of the table.
To check one or more CTL formulas at a time check the checkbox next to each of them. Once you have checked the formulas click on the check button. Before being subjected to model checking the formulas' consistency are checked and, if necessary, corrections are prompted.
Once a CTL formula has been evaluated to false and a counter example can be generated the button in fourth column on the formula's row is enabled. By clicking this button you can bring up a list of states that form a counter example to the formula. (This feature is not working correctly at the moment.)