lustrec / src / tools / stateflow / semantics / cPS_interpreter.ml @ 93119c3f
History  View  Annotate  Download (10.6 KB)
1 
open Basetypes 

2 
open Datatype 
3 
(* open ActiveEnv *) 
4 
open CPS_transformer 
5 
(* open Simulink *) 
6 
open Theta 
7  
8 
module Interpreter (Transformer : TransformerType) = 
9 
struct 
10 
module KT = KenvTheta (Transformer) 
11 
open KT 
12  
13 
let ( >? ) cond tr = 
14 
if cond then tr else Transformer.null 
15  
16 
module type DenotationType = 
17 
sig 
18 
module Theta : MemoThetaType 
19  
20 
val eval_dest : destination_t > Transformer.t wrapper_t > Transformer.t success_t > Transformer.t fail_t > Transformer.t 
21 
val eval_tau : trans_t > Transformer.t wrapper_t > Transformer.t success_t > Transformer.t fail_t > Transformer.t 
22 
val eval_T : transitions_t > Transformer.t wrapper_t > Transformer.t success_t > Transformer.t fail_t > Transformer.t 
23 
val eval_C : (path_t, 'b, Transformer.t) tag_t > path_t > composition_t > Transformer.t 
24 
val eval_open_path : mode_t > path_t > path_t > Transformer.t wrapper_t 
25 
val eval_S : (path_t, 'b, Transformer.t) tag_t > path_t > state_def_t > 'b 
26 
end 
27  
28 
module type AbsDenotationType = 
29 
sig 
30 
val eval_dest : kenv_t > destination_t > Transformer.t wrapper_t > Transformer.t success_t > Transformer.t fail_t > Transformer.t 
31 
val eval_tau : kenv_t > trans_t > Transformer.t wrapper_t > Transformer.t success_t > Transformer.t fail_t > Transformer.t 
32 
val eval_T : kenv_t > transitions_t > Transformer.t wrapper_t > Transformer.t success_t > Transformer.t fail_t > Transformer.t 
33 
val eval_C : kenv_t > (path_t, 'b, Transformer.t) tag_t > path_t > composition_t > Transformer.t 
34 
val eval_open_path : kenv_t > mode_t > path_t > path_t > Transformer.t wrapper_t 
35 
val eval_S : kenv_t > (path_t, 'b, Transformer.t) tag_t > path_t > state_def_t > 'b 
36 
end 
37  
38 
module AbstractKenv (Denot : functor (Kenv : KenvType) > DenotationType) : AbsDenotationType = 
39 
struct 
40 
let eval_dest kenv = 
41 
let module Kenv = 
42 
struct 
43 
let kenv = kenv 
44 
end in 
45 
let module D = Denot (Kenv) in 
46 
D.eval_dest 
47  
48 
let eval_tau kenv = 
49 
let module Kenv = 
50 
struct 
51 
let kenv = kenv 
52 
end in 
53 
let module D = Denot (Kenv) in 
54 
D.eval_tau 
55  
56 
let eval_T kenv = 
57 
let module Kenv = 
58 
struct 
59 
let kenv = kenv 
60 
end in 
61 
let module D = Denot (Kenv) in 
62 
D.eval_T 
63  
64 
let eval_C kenv = 
65 
let module Kenv = 
66 
struct 
67 
let kenv = kenv 
68 
end in 
69 
let module D = Denot (Kenv) in 
70 
D.eval_C 
71  
72 
let eval_open_path kenv = 
73 
let module Kenv = 
74 
struct 
75 
let kenv = kenv 
76 
end in 
77 
let module D = Denot (Kenv) in 
78 
D.eval_open_path 
79  
80 
let eval_S kenv = 
81 
let module Kenv = 
82 
struct 
83 
let kenv = kenv 
84 
end in 
85 
let module D = Denot (Kenv) in 
86 
D.eval_S 
87 
end 
88  
89 
module Denotation : functor (Thetaify : ThetaifyType) (Kenv : KenvType) > DenotationType = 
90 
functor (Thetaify : ThetaifyType) (Kenv : KenvType) > 
91 
struct 
92 
module Theta = Thetaify (Kenv) 
93  
94 
let eval_dest dest wrapper success fail = 
95 
Log.report ~level:sf_level (fun fmt > Format.fprintf fmt "@[<v 2>D[[%a]]@ " SF.pp_dest dest); 
96 
match dest with 
97 
 DPath p > wrapper p (success p) 
98 
 DJunction j > Theta.theta J j wrapper success fail 
99  
100 
let eval_tau trans wrapper success fail = 
101 
Log.report ~level:sf_level (fun fmt > Format.fprintf fmt "@[<v 2>tau[[%a]]@ " SF.pp_trans trans); 
102 
let success' p = 
103 
Transformer.(success p >> eval_act (module Theta) trans.transition_act) 
104 
in 
105 
let cond = Transformer.(event trans.event && trans.condition) in 
106 
Transformer.(eval_cond cond 
107 
(eval_act (module Theta) trans.condition_act >> eval_dest trans.dest wrapper success' fail) 
108 
fail.local) 
109  
110 
let rec eval_T tl wrapper success fail = 
111 
Log.report ~level:sf_level (fun fmt > Format.fprintf fmt "@[<v 2>T[[%a]]@ " SF.pp_transitions tl); 
112 
match tl with 
113 
 [] > fail.global 
114 
 t::[] > eval_tau t wrapper success fail 
115 
 t::tl > 
116 
let fail' = { fail with local = eval_T tl wrapper success fail } in 
117 
eval_tau t wrapper success fail' 
118  
119 
let frontier path = 
120 
match path with 
121 
 [] > [], [] 
122 
 t::q > [t], q 
123  
124 
let rec eval_open_path mode p p1 p2 success_p2 = 
125 
Log.report ~level:sf_level (fun fmt > Format.fprintf fmt "@[<v 2>open_path_rec[[mode %a, prefix %a, src %a, dst %a]]@ " pp_mode mode pp_path p pp_path p1 pp_path p2); 
126 
match frontier p1, frontier p2 with 
127 
 ([x], ps), ([y], pd) when x = y > eval_open_path mode (p@[x]) ps pd success_p2 
128 
 (x , _ ), (y , pd) > 
129 
match mode with 
130 
 Outer > (Transformer.(Theta.theta X (p@x) Loose >> success_p2 >> Theta.theta E (p@y) pd Loose)) 
131 
 Inner > (assert (x = []); 
132 
Transformer.(Theta.theta X (p@x) Strict >> success_p2 >> Theta.theta E (p@y) pd Strict)) 
133 
 Enter > (assert (x = [] && y <> []); 
134 
Transformer.( success_p2 >> Theta.theta E (p@y) pd Loose)) 
135  
136 
let rec eval_C : type a b. (a, b, Transformer.t) tag_t > path_t > composition_t > Transformer.t = 
137 
fun tag prefix comp > 
138 
match tag with 
139 
 E > Transformer.( 
140 
Log.report ~level:sf_level (fun fmt > Format.fprintf fmt "@[<v 2>C_%a[[%a, %a]]@ " pp_tag tag pp_path prefix SF.pp_comp comp); 
141 
match comp with 
142 
 Or (_T, []) > null 
143 
 Or ([], [s0]) > eval_open_path Enter prefix [] [s0] null 
144 
 Or (_T, _S) > let wrapper = eval_open_path Enter [] prefix in 
145 
let success p_d = null in 
146 
eval_T _T wrapper success { local = bot; global = bot } 
147 
 And (_S) > List.fold_right (fun p > (>>) (Theta.theta E (prefix@[p]) [] Loose)) _S null 
148 
) 
149 
 D > Transformer.( 
150 
match comp with 
151 
 Or (_T, []) > null 
152 
 Or (_T, p::_S) > eval_cond (active (prefix@[p])) (Theta.theta D (prefix@[p])) (eval_C D prefix (Or (_T, _S))) 
153 
 And (_S) > List.fold_right (fun p > (>>) (Theta.theta D (prefix@[p]))) _S null 
154 
) 
155 
 X > Transformer.( 
156 
match comp with 
157 
 Or (_T, []) > null 
158 
 Or (_T, p::_S) > eval_cond (active (prefix@[p])) (Theta.theta X (prefix@[p]) Loose) (eval_C X prefix (Or (_T, _S))) 
159 
 And (_S) > List.fold_right (fun p > (>>) (Theta.theta X (prefix@[p]) Loose)) _S null 
160 
) 
161 
 J > assert false 
162  
163 
let eval_S : type b. (path_t, b, Transformer.t) tag_t > path_t > state_def_t > b = 
164 
fun tag p p_def > 
165 
match tag with 
166 
 E > fun path frontier > Transformer.( 
167 
Log.report ~level:sf_level (fun fmt > Format.fprintf fmt "@[<v 2>S_%a[[node %a, dest %a, frontier %a]]@ " pp_tag tag pp_path p pp_path path pp_frontier frontier); 
168 
((frontier = Loose) >? (eval_act (module Theta) p_def.state_actions.entry_act >> eval_act (module Theta) (open_path p))) >> 
169 
match path with 
170 
 [] > eval_C E p p_def.internal_composition 
171 
 s::path_tl > Theta.theta E (p@[s]) path_tl Loose 
172 
) 
173 
 D > Transformer.( 
174 
Log.report ~level:sf_level (fun fmt > Format.fprintf fmt "@[<v 2>S_%a[[node %a]]@ " pp_tag tag pp_path p); 
175 
let wrapper_i = eval_open_path Inner [] p in 
176 
let wrapper_o = eval_open_path Outer [] p in 
177 
let success p_d = null in 
178 
let fail_o = 
179 
let fail_i = 
180 
let same_fail_C = eval_C D p p_def.internal_composition in 
181 
{ local = same_fail_C; global = same_fail_C } 
182 
in 
183 
let same_fail_i = eval_act (module Theta) p_def.state_actions.during_act >> eval_T p_def.inner_trans wrapper_i success fail_i in 
184 
{ local = same_fail_i; global = same_fail_i } 
185 
in 
186 
eval_T p_def.outer_trans wrapper_o success fail_o 
187 
) 
188 
 X > fun frontier > Transformer.( 
189 
Log.report ~level:sf_level (fun fmt > Format.fprintf fmt "@[<v 2>S_%a[[node %a, frontier %a]]@ " pp_tag tag pp_path p pp_frontier frontier); 
190 
eval_C X p p_def.internal_composition >> 
191 
((frontier = Loose) >? (eval_act (module Theta) p_def.state_actions.exit_act >> eval_act (module Theta) (close_path p))) 
192 
) 
193 
end 
194  
195 
module type ProgType = 
196 
sig 
197 
val init : state_name_t 
198 
val defs : src_components_t list 
199 
end 
200  
201 
module type EvaluationType = 
202 
sig 
203 
module Theta : ThetaType with type t = Transformer.t 
204 
val eval_prog : Transformer.t 
205 
val eval_components : 'c call_t > ('c * Transformer.t) list 
206 
end 
207 

208 
module Evaluation (Thetaify : ThetaifyType) (Prog : ProgType) : EvaluationType = 
209 
struct 
210 
module Denotation = Denotation (Thetaify) 
211 
module AbsDenotation = AbstractKenv (Denotation) 
212 
include AbsDenotation 
213  
214 
module Kenv : KenvType = 
215 
struct 
216 
let kenv = 
217 
List.fold_left ( 
218 
fun accu d > match d with 
219 
 State (p, defp) > { accu with cont_node = (p, ((fun kenv > eval_S kenv E p defp), (fun kenv > eval_S kenv D p defp), (fun kenv > eval_S kenv X p defp)))::accu.cont_node } 
220 
 Junction (j, defj) > { accu with cont_junc = (j, (fun kenv > eval_T kenv defj))::accu.cont_junc } 
221 
) {cont_node = []; cont_junc = []} Prog.defs 
222 
end 
223  
224 
module AppDenotation = Denotation (Kenv) 
225 
module Theta = AppDenotation.Theta 
226  
227 
let eval_components = Theta.components 
228  
229 
let eval_prog = 
230 
Transformer.(eval_cond (active [Prog.init]) (Theta.theta D [Prog.init]) (Theta.theta E [Prog.init] [] Loose)) 
231 
end 
232 
(* 
233 
module ThetaFix (Prog : ProgType) (Theta : ThetaType) : ThetaType = 
234 
struct 
235 
include Denotation (Theta) 
236  
237 
let theta = 
238 
let kenv = 
239 
List.fold_left ( 
240 
fun accu d > match d with 
241 
 State (p, defp) > { accu with cont_node = (p, (eval_S E p defp, eval_S D p defp, eval_S X p defp))::accu.cont_node } 
242 
 Junction (j, defj) > { accu with cont_junc = (j, (eval_T defj))::accu.cont_junc } 
243 
) {cont_node = []; cont_junc = []} Prog.defs 
244 
in Obj.magic (fun tag > theta_ify kenv tag) 
245 
end 
246 
module Rec (Prog : ProgType) = 
247 
struct 
248 
module rec Theta : ThetaType = ThetaFix (Prog) (Theta) 
249 
end 
250  
251 
module Eval (Prog : ProgType) : EvaluationType = 
252 
struct 
253 
module RecTheta = Rec (Prog) 
254 
module Theta = RecTheta.Theta 
255  
256 
let eval_prog = 
257 
Transformer.(eval_cond (active [Prog.init]) (Theta.theta D [Prog.init]) (Theta.theta E [Prog.init] [])) 
258 
end 
259  
260 
module Eval (Prog : ProgType) = 
261 
struct 
262 
module ThetaFunctor (Evaluation : EvaluationType) : ThetaType = 
263 
struct 
264 
let theta tag = (theta_ify Evaluation.kenv) tag 
265 
end 
266 
module EvaluationFunctor (Theta : ThetaType) : EvaluationType = 
267 
struct 
268 
include Denotation (Theta) 
269  
270 
let kenv = 
271 
List.fold_left ( 
272 
fun accu d > match d with 
273 
 State (p, defp) > { accu with cont_node = (p, (fun kenv > eval_S E p defp, eval_S D p defp, eval_S X p defp))::accu.cont_node } 
274 
 Junction (j, defj) > { accu with cont_junc = (j, (eval_T defj))::accu.cont_junc } 
275 
) {cont_node = []; cont_junc = []} Prog.defs 
276  
277 
let eval_prog = 
278 
Transformer.(eval_cond (active [Prog.init]) (Theta.theta D [Prog.init]) (Theta.theta E [Prog.init] [])) 
279 
end 
280 
module rec Theta : ThetaType = ThetaFunctor (Evaluation) 
281 
and Evaluation : EvaluationType = EvaluationFunctor (Theta) 
282 
end 
283 
*) 
284 
end 