|
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
|
|