run_to_completion operation specification

The project UMLStateMachineContract projet of the Eclipse workspace contained in is implementing the execution contract for the run_to_completion operation. It contains the following files:

To check the validity of an execution step, one simply has to execute the ATL transformation. The source model is the file containing the execution step models, and the target model the file that will contain the contract evaluation result.

This workspace has been set up to work with Topcased V3.3 (ATL v3.0.1). Topcased is a software environment based on the Eclipse/EMF framework and dedicated to the realization of critical embedded systems.