To set bounds on reachability graphs you must create formulas describing the bounds and apply them.
Formulas can be created by selecting rows in the places table. This will add to the formula a logical AND connective followed by the operand formula m(pN)=M, where N is the place number on the row and M is the token number currently on that row. If the formula is currently empty then no connective will be added but the formula will be simply the added operand until more operands are added.
Note that you can modify the marking value of each place in the table. This will allow you to add operands that have different marking value to the formula.
To remove an operand from the formula simply deselect the row in the table that contains the same place number. If this is not the first operand in the formula then the preceding AND connective is also removed.
The resulting formula is displayed in the text field under the table. When you have finished modifying it click on the Apply button in the lower part of the window. If there is already a state space computed in the NCES Analyzer this will reduce the state space according to the bounds formula. After the operation has finished you should see the reduced reachability graph in the NCES Analyzer window. If no state is yet available a bounded state space that conforms to the selected bounds formula will be created. It will then be passed on to NCES Analyzer.
Clicking on the Close button next to the Apply button closes the Analysis Bounds Editor. Another way to close it is to choose the option Exit from the File menu. This has exactly the same result as simply closing the editor window.