1 |
2de7fa82
|
ploc
|
|
2 |
|
|
(*
|
3 |
|
|
(* CPS semantics *)
|
4 |
|
|
module CPS_Interpreter = CPS.Evaluator
|
5 |
|
|
|
6 |
|
|
(* Hamon's original semantics, EMSOFT'05 *)
|
7 |
|
|
module Orig_Interpreter
|
8 |
|
|
*)
|
9 |
|
|
|
10 |
|
|
type backend = Eval | GenLus | GenImp
|
11 |
|
|
|
12 |
|
|
(* Model choice *)
|
13 |
|
|
let model_name = ref "simple"
|
14 |
|
|
|
15 |
|
|
let models = [(module Model_simple : Datatype.MODEL_T);
|
16 |
|
|
(module Model_stopwatch : Datatype.MODEL_T);
|
17 |
|
|
(module Model_medium : Datatype.MODEL_T)
|
18 |
|
|
]
|
19 |
|
|
let get_model_name m = let module M = (val m : Datatype.MODEL_T) in M.name
|
20 |
|
|
let set_model name =
|
21 |
|
|
if List.exists (fun n -> get_model_name n = name) models then
|
22 |
|
|
model_name := name
|
23 |
|
|
else failwith ("incorrect model name. Use " ^
|
24 |
|
|
(List.fold_left (fun r n -> r ^ " or " ^ get_model_name n) "" models))
|
25 |
|
|
|
26 |
|
|
(* Backend selection *)
|
27 |
|
|
let modular = ref 0
|
28 |
|
|
let set_modular i = modular := i
|
29 |
|
|
|
30 |
|
|
let mode = ref Eval
|
31 |
|
|
type eval_mode_t = CPSEval | EMSOFT05Eval | CompareEval
|
32 |
|
|
let eval_mode = ref CPSEval
|
33 |
|
|
let trace_id = ref 0
|
34 |
|
|
|
35 |
|
|
let set_trace_run_mode i =
|
36 |
|
|
mode := Eval; trace_id := i
|
37 |
|
|
|
38 |
|
|
let set_eval_mode s =
|
39 |
|
|
match s with
|
40 |
|
|
| "cps" -> eval_mode := CPSEval
|
41 |
|
|
| "emsoft05" -> eval_mode := EMSOFT05Eval
|
42 |
|
|
| "compare" -> eval_mode := CompareEval
|
43 |
|
|
| _ -> assert false
|
44 |
|
|
|
45 |
|
|
let set_mode m =
|
46 |
|
|
mode := m
|
47 |
|
|
|
48 |
|
|
(* Main *)
|
49 |
|
|
|
50 |
|
|
let options = [
|
51 |
|
|
"-model", Arg.String set_model, "model in {simple, stopwatch} (default: simple)";
|
52 |
|
|
"-eval", Arg.Int set_trace_run_mode, "execute the model on trace <int>";
|
53 |
|
|
"-eval-mode", Arg.String set_eval_mode, "select evaluator: cps, emsoft05 or compare";
|
54 |
|
|
"-gen_imp", Arg.Unit (fun _ -> set_mode GenImp), "generate imperative code";
|
55 |
|
|
"-gen_lustre", Arg.Unit (fun _ -> set_mode GenLus), "generate lustre model";
|
56 |
|
|
"-modular", Arg.Int set_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)"
|
57 |
|
|
]
|
58 |
|
|
|
59 |
|
|
let usage =
|
60 |
|
|
"sf_sem takes as input a model name and a backend.\n"^
|
61 |
|
|
"Backends are interpretor, imperative code generator, lustre code generator."
|
62 |
|
|
|
63 |
|
|
let run_trace model func t =
|
64 |
|
|
let init_env = Datatype.SF.init_env model in
|
65 |
|
|
let _ = Format.printf "Model definitions@.%a@.Initial state: %s @.####" Datatype.SF.pp_src (snd model) (fst model) in
|
66 |
|
|
|
67 |
|
|
let final_env, cpt =
|
68 |
|
|
List.fold_left (fun (env, cpt) event ->
|
69 |
|
|
Format.printf "#### %i@.%a@." cpt ActiveStates.Env.pp_env env;
|
70 |
|
|
Format.printf "-- Event %a --@." Basetypes.pp_event event;
|
71 |
|
|
let env', actions_performed = func (event, env) in
|
72 |
|
|
let _ =
|
73 |
|
|
match actions_performed with
|
74 |
|
|
| [] -> Format.printf "-- no action performed --@."
|
75 |
|
|
| _ -> (
|
76 |
|
|
Format.printf "@[<v 2>-- action performed --@ ";
|
77 |
|
|
List.iter (fun a -> Format.printf "%s@ " a) actions_performed;
|
78 |
|
|
Format.printf "@]@."
|
79 |
|
|
) in
|
80 |
|
|
(* we do not consider produced events *)
|
81 |
|
|
env', cpt+1
|
82 |
|
|
) (init_env, 1) t
|
83 |
|
|
in
|
84 |
|
|
Format.printf "#### %i@.%a@." cpt ActiveStates.Env.pp_env final_env;
|
85 |
|
|
()
|
86 |
|
|
|
87 |
|
|
let _ =
|
88 |
|
|
Arg.parse options (fun _ -> ()) usage;
|
89 |
|
|
let model = List.find (fun m -> get_model_name m = !model_name) models in
|
90 |
|
|
let modularmode =
|
91 |
|
|
match !modular with
|
92 |
|
|
| 2 -> true, true, true
|
93 |
|
|
| 1 -> false, true, false
|
94 |
|
|
| _ (* 0 *) -> false, false ,false
|
95 |
|
|
in
|
96 |
|
|
match !mode with
|
97 |
|
|
| Eval ->
|
98 |
|
|
let module Model = (val model) in
|
99 |
|
|
let module T = CPS_transformer.Evaluator in
|
100 |
|
|
let module Sem = CPS.Semantics (T) (Model) in
|
101 |
|
|
let nb_traces = List.length Model.traces in
|
102 |
|
|
if nb_traces = 0 then
|
103 |
|
|
failwith ("no available traces for model " ^ Model.name);
|
104 |
|
|
if !trace_id >= 0 && !trace_id < nb_traces then
|
105 |
|
|
let eval_func =
|
106 |
|
|
match !eval_mode with
|
107 |
|
|
| CPSEval ->
|
108 |
|
|
fun (evt, env) ->
|
109 |
|
|
let _, env', actions_performed = Sem.compute modularmode (evt, env, []) in
|
110 |
|
|
env', actions_performed
|
111 |
|
|
| EMSOFT05Eval ->
|
112 |
|
|
Orig_Interpreter.eval_prog Model.model
|
113 |
|
|
| CompareEval ->
|
114 |
|
|
let evalCPS = Sem.compute modularmode in
|
115 |
|
|
let evalEMSOFT05 = (Orig_Interpreter.eval_prog Model.model) in
|
116 |
|
|
fun ((evt, env) as arg) ->
|
117 |
|
|
let _, env1, actionl1 = evalCPS (evt, env, []) in
|
118 |
|
|
let env2, actionl2 = evalEMSOFT05 arg in
|
119 |
|
|
if ActiveStates.Env.equal (=) env1 env2 then
|
120 |
|
|
if actionl1 = actionl2 then
|
121 |
|
|
env1, actionl1
|
122 |
|
|
else (
|
123 |
|
|
Format.printf "##### ERROR: different behavior for interpreters ######@.";
|
124 |
|
|
Format.printf "CPS Eval actions:@.%a@." (Utils.fprintf_list ~sep:"; " Format.pp_print_string) actionl1;
|
125 |
|
|
Format.printf "EMSOFT05 Eval actions:@.%a@." (Utils.fprintf_list ~sep:"; " Format.pp_print_string) actionl2;
|
126 |
|
|
Format.printf "@?";
|
127 |
|
|
Format.printf "##### END OF ERROR ######@.";
|
128 |
|
|
env1, actionl1
|
129 |
|
|
)
|
130 |
|
|
else (
|
131 |
|
|
Format.printf "##### ERROR: different behavior for interpreters ######@.";
|
132 |
|
|
Format.printf "CPS Eval env:@.%a@." ActiveStates.Env.pp_env env1;
|
133 |
|
|
Format.printf "EMSOFT05 Eval env:@.%a@." ActiveStates.Env.pp_env env2;
|
134 |
|
|
Format.printf "@?";
|
135 |
|
|
exit 1
|
136 |
|
|
)
|
137 |
|
|
in
|
138 |
|
|
run_trace Model.model eval_func (List.nth Model.traces !trace_id)
|
139 |
|
|
|
140 |
|
|
else
|
141 |
|
|
failwith (string_of_int !trace_id ^
|
142 |
|
|
" is not a valid trace index in [0.." ^ string_of_int nb_traces ^ "]")
|
143 |
|
|
| GenImp -> (
|
144 |
|
|
let module Model = (val model) in
|
145 |
|
|
let module T = CPS_transformer.CodeGenerator in
|
146 |
|
|
let module Sem = CPS.Semantics (T) (Model) in
|
147 |
|
|
Sem.code_gen Format.std_formatter modularmode
|
148 |
|
|
)
|
149 |
|
|
| GenLus ->
|
150 |
|
|
let module Model = (val model) in
|
151 |
|
|
let vars = Datatype.SF.states Model.model in
|
152 |
|
|
let module T = CPS_transformer.LustrePrinter (struct let vars = vars end) in
|
153 |
|
|
let module Sem = CPS.Semantics (T) (Model) in
|
154 |
|
|
Sem.code_gen Format.std_formatter modularmode
|
155 |
|
|
|
156 |
|
|
|
157 |
|
|
|