Model-checking
You can perform model-checking with the MOVIDA Model Checker application. The
Model Checker can be invoked from the
NCES Analyzer. To start NCES
Analyzer choose the menu option NCES Analyzer from the Validation
menu.
The validation menu also contain other options for model checking:
- To invoke SESA - which is an external tool - select the menu option
Call SESA.
- Before SESA can be run you must set its path correctly by selecting
the menu option Set SESA Path. A small dialog will appear with a
text field where you can type the correct path. You can alternatively
browse the correct path by clicking on the button next to the text
field.
- To start the
Training Utility select the menu option Training Utility.
- SESA requires special input files before it can analyze a model. These
files can be generated by selecting the menu option Generate SESA
Input Files. You will be prompted whether to create input files from
the current model. Click on the YES button to choose for which part of
the model the files will be generated. Otherwise click on the NO button to
choose a file containing the appropriate model.