The Bounds Editor Options Menu

The first two items in the Options menu are related to state space computation and reduction while the options beginning with the word Display affect which places are displayed in the table.

If you want to remove all set bounds and obtain the original unbounded reachability graph again select the option Restore Default State Space. Note that this option is enabled only if a state space has already been constructed with the NCES Analyzer and then it has been reduced.

The submenu Build State Space has two options:

Set Step Window
Select this to set the size of the state space window that is used in computing bounded state spaces when no state space has been created with NCES Analyzer.
Build
Selecting this will start state space reduction if a state space has been created in NCES Analyzer. Otherwise it will create a new bounded state space. It has the same effect as the Apply button.

Select the menu item Display I/O modules to display in the table only those places that belong to modules of types bool_input, bool_output and bool_output2.

Select the menu item Display inputs to list only the places belonging to modules of type bool_input.

If the menu item Display outputs is selected only places that belong to modules of types bool_output and bool_output2 are listed in the table.

Selecting the menu item Display modules... brings up a new dialog for selecting the modules whose places are to be displayed in the table.

All places in the current NCES will be listed in the table if the menu item Display all is selected.

Bounds Editor Options menu

The contents of the table of places can be used in forming bounds formulas. These bounds can then be applied on the current state space effectively reducing its size.