Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / tools / stateflow / semantics / cPS_interpreter.ml @ 3769b712

History | View | Annotate | Download (10.8 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
      Lustrec.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
      Lustrec.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
      Lustrec.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
      Lustrec.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
	  Lustrec.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
	  Lustrec.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
	  Lustrec.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
	  Lustrec.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 : prog_t 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),
220
                                                               (fun kenv -> eval_S kenv D p defp),
221
                                                               (fun kenv -> eval_S kenv X p defp)))::accu.cont_node }
222
	  | Junction (j, defj) -> { accu with cont_junc = (j, (fun kenv -> eval_T kenv defj))::accu.cont_junc }
223
          | SFFunction _       -> accu
224
        ) {cont_node = []; cont_junc = []} Prog.defs
225
    end
226

    
227
    module AppDenotation = Denotation (Kenv)
228
    module Theta = AppDenotation.Theta
229

    
230
    let eval_components = Theta.components
231

    
232
    let eval_prog =
233
      Transformer.(eval_cond (active [Prog.init]) (Theta.theta D [Prog.init]) (Theta.theta E [Prog.init] [] Loose))
234
  end
235
 (*
236
  module ThetaFix (Prog : ProgType) (Theta : ThetaType) : ThetaType =
237
  struct
238
    include Denotation (Theta)
239

    
240
    let theta =
241
      let kenv =
242
	List.fold_left (
243
	  fun accu d -> match d with
244
	  | 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  }
245
	  | Junction (j, defj) -> { accu with cont_junc = (j, (eval_T defj))::accu.cont_junc  }
246
	) {cont_node = []; cont_junc = []} Prog.defs
247
      in Obj.magic (fun tag -> theta_ify kenv tag)
248
  end
249
  module Rec (Prog : ProgType) =
250
  struct
251
    module rec Theta : ThetaType = ThetaFix (Prog) (Theta)
252
  end
253

    
254
  module Eval (Prog : ProgType) : EvaluationType =
255
  struct
256
    module RecTheta = Rec (Prog)
257
    module Theta = RecTheta.Theta
258

    
259
    let eval_prog =
260
	Transformer.(eval_cond (active [Prog.init]) (Theta.theta D [Prog.init]) (Theta.theta E [Prog.init] []))
261
  end
262

    
263
  module Eval (Prog : ProgType) =
264
  struct
265
    module ThetaFunctor (Evaluation : EvaluationType) : ThetaType =
266
    struct
267
      let theta tag = (theta_ify Evaluation.kenv) tag
268
    end
269
    module EvaluationFunctor (Theta : ThetaType) : EvaluationType =
270
    struct
271
      include Denotation (Theta)
272

    
273
      let kenv =
274
	List.fold_left (
275
	  fun accu d -> match d with
276
	  | 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  }
277
	  | Junction (j, defj) -> { accu with cont_junc = (j, (eval_T defj))::accu.cont_junc  }
278
	) {cont_node = []; cont_junc = []} Prog.defs
279

    
280
      let eval_prog =
281
	Transformer.(eval_cond (active [Prog.init]) (Theta.theta D [Prog.init]) (Theta.theta E [Prog.init] []))
282
    end
283
    module rec Theta : ThetaType = ThetaFunctor (Evaluation)
284
    and Evaluation : EvaluationType = EvaluationFunctor (Theta)
285
end
286
  *)
287
end