Skip to content
mudathirmahgoub edited this page Jun 5, 2018 · 18 revisions

CoCoSim Documentation

Verification

FrontEnd

All front end code is located inside src/frontEnd directory. It consists of 2 main steps preprocessing and generating the internal representation.

Preprocessing (PP)

In this step complex Simulink blocks are simplified and replaced with basic blocks that can be handled by the translator to Lustre.

Internal representation (IR)

This step reads the contents of the preprocessed model and outputs them in json format. The IR consists of

  • src/frondEnd/IR/IR_Config.m: (to be completed)

  • src/frondEnd/IR/cocosim_IR.m: This function creates a json file of the internal representation of the model, and returns the json representation json_model = COCOSIM_IR(model_path)

  • src/frondEnd/IR/blocks/subsystems_struct.m: This function recursively constructs the internal representation of subsystems or block_diagrams. S = subsystems_struct(file_name) for the IR of a simulink block.

  • src/frondEnd/IR/blocks/chart_struct.m: This function handles stateflow blocks. It receives the path to a stateflow block and returns a MATLAB structure with the contents of the stateflow block. This function depends on src/frondEnd/IR/utils/ChartParser.jar to parse the labels of states and transitions inside the stateflow block using the following 2 functions:

    • edu.uiowa.chart.state.StateParser.parse: This function receives the label string of state and returns an object containing state actions.
    • edu.uiowa.chart.transition.TransitionParser.parse: This function receives the label string of a transition and returns an object that contains its event, condition, condition action and transition action.

The source code for src/frondEnd/IR/utils/ChartParser.jar is written in Java and is located in src/frontEnd/IR/utils/ChartParser

MiddleEnd

BackEnd

CoCoSim Specification Library

CoCoSim menu

Clone this wiki locally