## 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 |