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
. 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.