Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / tools / stateflow / src / sf_sem.ml @ 2de7fa82

History | View | Annotate | Download (5.41 KB)

1

    
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