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 