Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / tools / stateflow / README.md @ cb781911

History | View | Annotate | Download (1.02 KB)

1
# stateflow_CPS_semantics
2
A continuation passing style semantics for Stateflow in Ocaml
3

    
4
Software implements:
5
- our generic CPS semantics, instanciated as
6
  - an evaluator (aka simulator)
7
  - an imperative code generator
8
  - a lustre automaton generator compatible with lustrec (github/coco-team/lustrec)
9
- the reference denotational semantics of Stateflow by Hamon as presented in his EMSOFT'05 paper.
10

    
11
Options:
12
sf_sem takes as input a model name and a backend. Traces are hard coded in the source files.
13

    
14
Backends are interpretor, imperative code generator, lustre code generator.
15
  -model model in {simple, stopwatch} (default: simple)
16
  -eval execute the model on trace <int>
17
  -eval-mode select evaluator: cps, emsoft05 or compare
18
  -gen_imp generate imperative code
19
  -gen_lustre generate lustre model
20
  -modular generate modular code (either for imperative or lustre backend) 0 is not modular, 1 modularize nodes, 2 modularize entry, during and exit actions (default 0)
21

    
22
Example:
23
./sf_sem -model stopwatch -eval-mode compare -eval 1
24