Middle End

All middle end code is located inside src/middleEnd directory. Currently there are 2 implementations:

CoCoSpec Compiler

This implementation uses the ir2lustre which is written in Java. This translator supports contracts blocks in CoCoSim Specification Library. However the translator doesn't fully support stateflow blocks.

• cocoSpecCompiler: This function receives a path to the original model to be verified and does the following:

  • Preprocess the model by calling src/frondEnd/pp/cocosim_pp.m.
  • Generate the json format of the internal representation (IR) of the preprocessed model by calling src/frondEnd/IR/cocosim_IR.m.
  • Translate the json (IR) into Lustre by calling the function edu.uiowa.json2lus.J2LTranslator which is located in the jar file src/backEnd/verification/cocoSpecVerify/utils/CocoSim_IR_Compiler-0.1-jar-with-dependencies.jar.
  • Generate the mapping between between block names and Lustre names by calling the function j2l_trans.dumpMappingInfoToJsonFile which is located in the jar file src/backEnd/verification/cocoSpecVerify/utils/CocoSim_IR_Compiler-0.1-jar-with-dependencies.jar.

• cocoSpecIRPP: This function does some preprocessing for the IR specific to the ir2lustre translator.

Lustre Compiler

[to be completed]