· Tool (s2c): tool.zip.

· s2c examples: examples.zip.

· Basic definitions: basic_toolkit.tex.

· Circus model of the simulator: stateflow_toolkit: stateflow_toolkit.tex, stateflow_toolkit.pdf.

· Simulink model containing the Stateflow chart shift logic: sf_car.mdl.

· Circus model of shift logic chart: sf_car.tex, sf_car.pdf.

· Function library for specification sf_car.tex: calc_th.tex, calc_th.pdf

· Formal syntax of Stateflow: StateflowAbstractSyntax.tex, StateflowAbstractSyntax.pdf.

· Formal syntax of Z: ZFormalSyntax.tex, ZFormalSyntax.pdf.

· Formal syntax of Circus: CircusFormalSyntax.tex, CircusFormalSyntax.pdf.

· Formal translation rules: Stateflow2Circus.tex, Stateflow2Circus.pdf.

· Simulink model containing the Stateflow chart controller: air.mdl.

· Circus model of the controller in the Simulink diagram Air: air_Controller_model.tex, air_Controller_model.pdf.

· Source files for a parallel implementation of the Stateflow chart in air.mdl : parallel_implementation.zip.

· Circus model of the implementation of the controller in the Simulink diagram Air: air_Controller_impl_model.tex, air_Controller_impl_model.pdf.