| 1 |
cb781911
|
ploc
|
# 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
|