The compiler, translate modularly the pre-processed Simulink model and generates Lustre code. Moreover, it performs book-keeping of the different Simulink/Stateflow constructs (e.g. signal name, block type etc ..). This allows to trace Simulink/Stateflow constructs in the Lustre programs.

Takes the Lustre code and it performs either (i) compilation into imperative code (C or Rust) or (ii) it performs sfatey analysis of the provided property. For compilation it uses LustreC, while for safety verification it uses one of: Zustre, Kind2 or JKind. The result of the safety analysis is reported back to the Matlab environment. In case the property supplied is falsified, CoCoSim provides means to simulate the counterexample trace in the Matlab environment.