Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / tools / stateflow / semantics / cPS_interpreter.ml @ 93119c3f

History | View | Annotate | Download (10.6 KB)

1 2de7fa82 ploc
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 93119c3f ploc
      Log.report ~level:sf_level (fun fmt -> Format.fprintf fmt "@[<v 2>D[[%a]]@ " SF.pp_dest dest);
96 2de7fa82 ploc
      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 93119c3f ploc
      Log.report ~level:sf_level (fun fmt -> Format.fprintf fmt "@[<v 2>tau[[%a]]@ " SF.pp_trans trans);
102 2de7fa82 ploc
      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 93119c3f ploc
      Log.report ~level:sf_level (fun fmt -> Format.fprintf fmt "@[<v 2>T[[%a]]@ " SF.pp_transitions tl);
112 2de7fa82 ploc
      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 93119c3f ploc
      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 2de7fa82 ploc
      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 93119c3f ploc
	  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 2de7fa82 ploc
	  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 93119c3f ploc
	  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 2de7fa82 ploc
	  ((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 93119c3f ploc
	  Log.report ~level:sf_level (fun fmt -> Format.fprintf fmt "@[<v 2>S_%a[[node %a]]@ " pp_tag tag pp_path p);
175 2de7fa82 ploc
	  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 93119c3f ploc
	  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 2de7fa82 ploc
	  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