Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / tools / stateflow / src / semantics / emsoft05 / orig_Interpreter.ml @ 2de7fa82

History | View | Annotate | Download (9.38 KB)

1
open Basetypes
2
open Datatype
3
open Format
4
open Log
5
open SF
6

    
7
let actions_performed = ref []
8

    
9
    
10
(*******************************)
11

    
12
type env_t = bool ActiveStates.Env.t (* Don't care for values yet *)
13
let pp_env = ActiveStates.Env.pp_env
14
  
15
type success_t = env_t -> path_t -> env_t
16
type fail_t = env_t -> env_t
17

    
18
type kenv_t = {
19
  cont_node : (
20
    path_t * (
21
      (kenv_t -> env_t -> path_t -> event_t -> env_t) *
22
	(kenv_t -> env_t -> event_t -> env_t) *
23
	(kenv_t -> env_t -> event_t -> env_t)
24
    )
25
  ) list;
26
  cont_junc : (
27
    junction_name_t * (
28
      kenv_t -> env_t -> success_t -> fail_t -> event_t -> env_t)
29
  ) list
30
}
31

    
32
let theta_j dest theta =
33
  (try
34
     List.assoc dest theta.cont_junc
35
   with Not_found ->
36
     (eprintf "Lost junction %a@ " pp_junction_name dest;
37
      assert false
38
     )
39
  ) theta
40

    
41
let theta_e, theta_d, theta_x =
42
  let theta_node id theta =
43
    try
44
      List.assoc id theta.cont_node
45
    with Not_found ->
46
      (eprintf "Lost path [%a]@." pp_path id;
47
       assert false
48
      )
49
  in
50
  (fun id theta -> let (e,d,x) = theta_node id theta in e theta),
51
  (fun id theta -> let (e,d,x) = theta_node id theta in d theta),
52
  (fun id theta -> let (e,d,x) = theta_node id theta in x theta)
53

    
54
let add_action a = actions_performed := !actions_performed @ [a]
55

    
56
let eval_act action theta rho =
57
  (match action with
58
  | Action.Call _  -> assert false
59
  | Action.Quote s -> add_action s; () (*Format.eprintf "----- action = %s@." s*)
60
  | Action.Nil  -> () (* no action *)
61
  | _ -> assert false (* other constructs should not appear here *)
62
  );
63
  rho
64

    
65
let rec eval_cond condition (evt, rho) =
66
  match condition, evt with
67
  | Condition.True, _ -> true
68
  | Condition.Active p, _ -> ActiveStates.Env.find p rho
69
  | Condition.Event e, Some evt -> e = evt
70
  | Condition.Event e, None -> false
71
  | Condition.Neg cond, _ -> not (eval_cond cond (evt, rho))
72
  | Condition.And (cond1, cond2), _ -> (eval_cond cond1 (evt, rho)) && (eval_cond cond2 (evt, rho))
73
  | Condition.Quote c, _ -> add_action c; true  (* invalid behavior but similar to the other: should evaluate condition *)
74
    
75
  (* (match condition with Some s -> printf "----- cond = %s@." s | _ -> ()); *)
76
  (* true *)
77

    
78
let bot _ = assert false
79

    
80
let eval_dest dest theta rho success fail e =
81
  log (fun fmt -> fprintf fmt "@[<v 2>D[[%a]] (%a)?@ " SF.pp_dest dest pp_env rho);
82
  let res =
83
    match dest with
84
    | DPath p -> success rho p
85
    | DJunction j -> theta_j j theta rho success fail e
86
  in
87
  log (fun fmt -> fprintf fmt "@]@ D[[%a]]: %a@ " SF.pp_dest dest pp_env res);
88
  res
89

    
90
let eval_tau trans theta rho success fail e =
91
  (* eprintf "%t@." (fun fmt -> fprintf fmt "@[<v 2>tau[[%a]] (%a)?@ " SF.pp_trans trans pp_env rho); *)
92
  let res =
93
    if (match trans.event with None -> true | _ -> e = trans.event) && eval_cond trans.condition (trans.event, rho) then
94
      let success' rho_s p =
95
	(* eprintf "succes de tau %a: p = %a@." pp_trans trans pp_path p; *)
96
	if p = [] then (
97
	  (* eprintf "cas1@."; *)
98
	  success rho_s [] (* was p but p is [] *)
99
	)
100
	else (
101
	  	  (* eprintf "cas2@."; *)
102
		    success (eval_act trans.transition_act theta rho_s) p
103
	)
104
      in
105
      eval_dest trans.dest theta (eval_act trans.condition_act theta rho) success' fail e
106
    else
107
      fail rho
108

    
109
  in
110
  (* eprintf "%t@."  (fun fmt -> fprintf fmt "@]@ tau[[%a]]: %a@ " pp_trans trans pp_env res); *)
111
  res
112

    
113
let rec eval_T tl theta rho success fail e =
114
  log (fun fmt -> fprintf fmt "@[<v 2>T[[%a]] (%a)?@ " pp_transitions tl pp_env rho);
115
  let res =
116
    match tl with
117
    | [] -> success rho []
118
    | t::[] -> eval_tau t theta rho success fail e
119
    | t::t'::tl ->
120
       let fail' rho_f = eval_T (t'::tl) theta rho_f success fail e in
121
       eval_tau t theta rho success fail' e
122
  in
123
  log (fun fmt -> fprintf fmt "@]@ T[[%a]]: %a@ " pp_transitions tl pp_env res);
124
  res
125

    
126
let eval_open rho p = ActiveStates.Env.add p true rho
127
let eval_close rho p = ActiveStates.Env.add p false rho
128

    
129
let eval_Ce prefix comp theta rho e =
130
  log (fun fmt -> fprintf fmt "@[<v 2>Ce[[%a, %a]] (%a)?@ " pp_path prefix pp_comp comp pp_env rho);
131
  let res =
132
    match comp with
133
    | Or (_T, []) -> log (fun fmt -> fprintf fmt "no content: = no impact@ "); rho
134
    | Or (_T, _S) -> eval_T _T theta rho (fun rho_s p -> theta_e p theta rho_s [] e) bot e
135
    | And (_S) -> List.fold_left (fun accu p -> theta_e (prefix@[p]) theta rho [] e) rho _S
136
  in
137
  log (fun fmt -> fprintf fmt "@]@ Ce[[%a, %a]]: %a@ " pp_path prefix pp_comp comp pp_env res);
138
  res
139

    
140
let rec eval_Cd prefix comp theta rho e =
141
  log (fun fmt -> fprintf fmt "@[<v 0>Cd[[%a, %a]] (%a)?@ " pp_path prefix pp_comp comp pp_env rho);
142
  let res =
143
    match comp with
144
    | Or (_T, []) -> rho
145
    | Or (_T, p::_S) ->
146
       if ActiveStates.Env.find (prefix@[p]) rho then (
147
	 log (fun fmt -> fprintf fmt "active node %a: running it@ " pp_path (prefix@[p]));
148

    
149
	 (* (\********** QUESTION SUR L'ORDRE A HAMZA **************\) *)
150
	 (* let rho', success = *)
151
	 (*   (\* if true (\\* cas 1: during_act effectué avant execution des components *\\) then *\) *)
152
	 (*     theta_d (prefix@[p]) theta rho e, (\* <-- update rho with theta_d of node (prefix@[p]) *\) *)
153
	 (*     (fun rho_s p' -> theta_d p' theta rho_s e) (\* <-- default success function *\) *)
154
	 (*     (\* je ne suis pas sur de ce p', peut etre faut il rajouter prefix@[p] devant ? *\) *)
155
	 (*   (\* else (\\* cas 2: during_act postponé apres execution des components *\\) *\) *)
156
	 (*   (\*   rho, (\\* <-- on ne touche pas a rho *\\) *\) *)
157
	 (*   (\*   (fun rho_s p' -> theta_d p' theta rho_s e) *\) *)
158
	 (*   (\*   (\\* je ne suis pas sur de ce p', peut etre faut il rajouter prefix@[p] devant ? *\\) *\) *)
159
	 (* in *)
160
	 (* eval_T _T theta rho' success bot e *)
161
	 (* (\********** QUESTION SUR L'ORDRE A HAMZA **************\) *)
162

    
163
       (* CODE PRECEDENT TEL QUE DECRIT DANS L'ARTICLE *)
164
        	 theta_d (prefix@[p]) theta rho e
165
       (* CODE PRECEDENT TEL QUE DECRIT DANS L'ARTICLE *)
166
       )
167
       else (
168
	 log (fun fmt -> fprintf fmt "inactive node %a: continuing on the list %a@ " pp_path (prefix@[p]) (Utils.fprintf_list ~sep:"; " pp_state_name) _S);
169
	 eval_Cd prefix (Or (_T, _S)) theta rho e
170
       )
171
    | And (_S) -> List.fold_left (fun accu p -> theta_d (prefix@[p]) theta rho e) rho _S
172
  in
173
  log (fun fmt -> fprintf fmt "@]@ Cd[[%a, %a]]: %a@ " pp_path prefix pp_comp comp pp_env res);
174
  res
175

    
176
let eval_Cx prefix comp theta rho e : env_t =
177
  log (fun fmt -> fprintf fmt "@[<v 2>Cx[[%a, %a]] (%a)?@ " pp_path prefix pp_comp comp pp_env rho);
178
  let res =
179
    match comp with
180
    | Or (_T, _S) ->
181
       List.fold_left
182
	 (fun rho p -> if ActiveStates.Env.find (prefix @ [p]) rho then theta_x (prefix@[p]) theta rho e else rho)
183
	 rho
184
	 _S
185
    | And (_S) -> List.fold_left (fun accu p -> theta_x (prefix@[p]) theta rho e) rho _S
186
  in
187
  log (fun fmt -> fprintf fmt "@]@ Cx[[%a, %a]]: %a@ " pp_path prefix pp_comp comp pp_env res);
188
  res
189

    
190
let eval_Se (p:path_t) p_def theta rho path e =
191
  log (fun fmt -> fprintf fmt "@[<v 2>Se[[node %a, path %a]] (%a)?@ " pp_path p pp_path path pp_env rho);
192
  let res =
193
    let rho' = eval_act p_def.state_actions.entry_act theta rho in
194
    match path with
195
    | [] -> eval_open (eval_Ce p p_def.internal_composition theta rho' e) p
196
    | s::path_tl -> eval_open (theta_e (p@[s]) theta rho' path_tl e) p
197
  in
198
  log (fun fmt -> fprintf fmt "@]@ Se[[node %a, path %a]]: %a@ " pp_path p pp_path path pp_env res);
199
  res
200

    
201
let eval_Sx p p_def theta rho e =
202
  log (fun fmt -> fprintf fmt "@[<v 2>Sx[[node %a]] (%a)?@ " pp_path p pp_env rho);
203
  let res =
204
  eval_close
205
    (eval_act p_def.state_actions.exit_act theta
206
       (eval_Cx p p_def.internal_composition theta rho e)
207
    )
208
    p
209
  in
210
  log (fun fmt -> fprintf fmt "@]@ Sx[[node %a]]: %a@ " pp_path p pp_env res);
211
  res
212

    
213
let rec eval_open_path theta rho p p1 p2 term e =
214
  match p1, p2 with
215
  | _, [] -> term rho
216
  | x::ps, y::pd ->
217
     if x = y then
218
       eval_open_path theta rho (p@[x]) ps pd term e
219
     else
220
       let rho_x = theta_x (p@[x]) theta rho e in
221
       theta_e (p@[y]) theta rho_x pd e
222
  | _ -> assert false
223

    
224
let eval_Sd p p_def theta rho e =
225
  log (fun fmt -> fprintf fmt "@[<v 2>Sd[[node %a]] (%a)?@ " pp_path p pp_env rho);
226
  let res =
227
    let fail rho_f =
228
      let faili (rho_fi: env_t) : env_t =
229
	eval_Cd p p_def.internal_composition theta (eval_act p_def.state_actions.during_act theta rho_fi) e
230
      in
231
      let successi rho_si p_d =
232
	eval_open_path theta rho_si [] p p_d faili e in
233
      log (fun fmt -> fprintf fmt "eval_inner %a@ " pp_transitions p_def.inner_trans);
234
      eval_T p_def.inner_trans theta rho_f successi faili e
235
    in
236
    let success rho_s p_d =
237
      eval_open_path theta rho_s [] p p_d fail e in
238
    log (fun fmt -> fprintf fmt "eval_outer %a@ " pp_transitions p_def.outer_trans);
239
    eval_T p_def.outer_trans theta rho success fail e
240
  in
241
  log (fun fmt -> fprintf fmt "@]@ Sd[[node %a]]: %a@ " pp_path p pp_env res);
242
  res
243

    
244

    
245
let eval_prog (s, defs) (e, rho) =
246
  (* Action list is uglily encoded using global variables. Shame on me! *)
247
  actions_performed := [];
248
  (* (match e with Some s -> printf "EVENT = %s@." s | _ -> ()); *)
249
  let theta = List.fold_left (
250
    fun accu d -> match d with
251
    | State (p, defp) -> { accu with cont_node = (p, (eval_Se p defp, eval_Sd p defp, eval_Sx p defp))::accu.cont_node  }
252
    | Junction (j, defj) -> { accu with cont_junc = (j, (eval_T defj))::accu.cont_junc  }
253
  ) {cont_node = []; cont_junc = []} defs in
254
  let res =
255
    if ActiveStates.Env.find [s] rho then
256
      theta_d [s] theta rho e
257
    else
258
      theta_e [s] theta rho [] e
259
  in
260
  res, !actions_performed
261