Basic steps using MOVIDA NCES Generator (MNG)

1. Open the source code file (.cxt):
1. Open the controller source file


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


3. Load Plant UML Model from XMI file:
Load Plant Model UML-XMI


4. Start the composition of Plant and Controller models
Interconnect 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.
Stub for Condition Inputs


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


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