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