Basic steps using MOVIDA
NCES Generator (MNG)
1. Open the source code file (.cxt):

2. Convert the source to the Net
Condition/Event Systems (NCES):

3. Load Plant UML Model from
XMI file:

4. Start the composition of
Plant and Controller models

5. You may want to use
stub for condition inputs for providing constant values to them. First
right-click on the model to bring up a popup menu. Then select the option
Add Stub For Condition Inputs to add the stub.

6. You may also find it usefull
to add an Event Latch that may get the status if some event has occured.

7. Interconnect all the
necessary modules and save the result to the Hard Disk
8. You may now use
model-checking tools for the system verification.