Project

General

Profile

Revision 3769b712 src/tools/stateflow/semantics/cPS_interpreter.ml

View differences:

src/tools/stateflow/semantics/cPS_interpreter.ml
92 92
    module Theta = Thetaify (Kenv)
93 93

  
94 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);
95
      Lustrec.Log.report ~level:sf_level (fun fmt -> Format.fprintf fmt "@[<v 2>D[[%a]]@ " SF.pp_dest dest);
96 96
      match dest with
97 97
      | DPath p -> wrapper p (success p)
98 98
      | DJunction j -> Theta.theta J j wrapper success fail
99 99

  
100 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);
101
      Lustrec.Log.report ~level:sf_level (fun fmt -> Format.fprintf fmt "@[<v 2>tau[[%a]]@ " SF.pp_trans trans);
102 102
      let success' p =
103 103
	Transformer.(success p >> eval_act (module Theta) trans.transition_act)
104 104
      in
......
108 108
		     fail.local)
109 109

  
110 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);
111
      Lustrec.Log.report ~level:sf_level (fun fmt -> Format.fprintf fmt "@[<v 2>T[[%a]]@ " SF.pp_transitions tl);
112 112
      match tl with
113 113
      | [] -> fail.global
114 114
      | t::[] ->  eval_tau t wrapper success fail
......
122 122
      | t::q -> [t], q
123 123

  
124 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);
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 126
      match frontier p1, frontier p2 with
127 127
      | ([x], ps), ([y], pd) when x = y -> eval_open_path mode (p@[x]) ps pd success_p2
128 128
      | (x  , _ ), (y  , pd)            ->
......
137 137
      fun tag prefix comp ->
138 138
	match tag with
139 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);
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 141
	  match comp with
142 142
	  | Or (_T, [])   -> null
143 143
	  | Or ([], [s0]) -> eval_open_path Enter prefix [] [s0] null
......
164 164
      fun tag p p_def ->
165 165
	match tag with
166 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);
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 168
	  ((frontier = Loose) >? (eval_act (module Theta) p_def.state_actions.entry_act >> eval_act (module Theta) (open_path p))) >>
169 169
	  match path with
170 170
	  | []         -> eval_C E p p_def.internal_composition
171 171
	  | s::path_tl -> Theta.theta E (p@[s]) path_tl Loose
172 172
	)
173 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);
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 175
	  let wrapper_i = eval_open_path Inner [] p in
176 176
	  let wrapper_o = eval_open_path Outer [] p in
177 177
	  let success p_d = null in
......
186 186
	  eval_T p_def.outer_trans wrapper_o success fail_o
187 187
	)
188 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);
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 190
	  eval_C X p p_def.internal_composition >>
191 191
	  ((frontier = Loose) >? (eval_act (module Theta) p_def.state_actions.exit_act >> eval_act (module Theta) (close_path p)))
192 192
	)

Also available in: Unified diff