Project

General

Profile

Revision d4807c3d src/causality.ml

View differences:

src/causality.ml
113 113
let node_memory_variables nd =
114 114
 List.fold_left eq_memory_variables ISet.empty nd.node_eqs
115 115

  
116
let node_non_input_variables nd =
117
  let outputs = List.fold_left (fun outputs v -> ISet.add v.var_id outputs) ISet.empty nd.node_outputs in
118
  List.fold_left (fun non_inputs v -> ISet.add v.var_id non_inputs) outputs nd.node_locals
119

  
116 120
(* computes the equivalence relation relating variables 
117 121
   in the same equation lhs, under the form of a table 
118 122
   of class representatives *)
......
132 136
 | Types.Ttuple tl -> duplicate v (List.length tl)
133 137
 | _         -> [v]
134 138

  
139

  
135 140
(* Add dependencies from lhs to rhs in [g, g'], *)
136 141
(* no-mem/no-mem and mem/no-mem in g            *)
137 142
(* mem/mem in g'                                *)
138 143
(* excluding all/[inputs]                       *)
139
let add_eq_dependencies mems inputs eq (g, g') =
140
  let rec add_dep lhs_is_mem lhs rhs g =
141
    let add_var x (g, g') =
142
      if ISet.mem x inputs then (g, g') else
144
let add_eq_dependencies mems non_inputs eq (g, g') =
145
  let add_var lhs_is_mem lhs x (g, g') =
146
    if ISet.mem x non_inputs then
143 147
      match (lhs_is_mem, ISet.mem x mems) with
144 148
      | (false, true ) -> (add_edges [x] lhs g, g'                  )
145 149
      | (false, false) -> (add_edges lhs [x] g, g'                  )
146 150
      | (true , false) -> (add_edges lhs [x] g, g'                  )
147
      | (true , true ) -> (g                  , add_edges [x] lhs g') in
151
      | (true , true ) -> (g                  , add_edges [x] lhs g')
152
    else (g, g') in
153
(* Add dependencies from [lhs] to rhs clock [ck]. *)
154
  let rec add_clock lhs_is_mem lhs ck g =
155
    (*Format.eprintf "add_clock %a@." Clocks.print_ck ck;*)
156
    match (Clocks.repr ck).Clocks.cdesc with
157
    | Clocks.Con (ck', cr, _)   -> add_var lhs_is_mem lhs (Clocks.const_of_carrier cr) (add_clock lhs_is_mem lhs ck' g)
158
    | Clocks.Ccarrying (_, ck') -> add_clock lhs_is_mem lhs ck' g
159
    | _                         -> g in
160
  let rec add_dep lhs_is_mem lhs rhs g =
148 161
(* Add mashup dependencies for a user-defined node instance [lhs] = [f]([e]) *)
149 162
(* i.e every input is connected to every output, through a ghost var *)
150 163
    let mashup_appl_dependencies f e g =
151 164
      let f_var = mk_instance_var (sprintf "%s_%d" f eq.eq_loc.Location.loc_start.Lexing.pos_lnum) in
152 165
      List.fold_right (fun rhs -> add_dep lhs_is_mem (adjust_tuple f_var rhs) rhs)
153
	(expr_list_of_expr e) (add_var f_var g) in
166
	(expr_list_of_expr e) (add_var lhs_is_mem lhs f_var g) in
154 167
    match rhs.expr_desc with
155 168
    | Expr_const _    -> g
156 169
    | Expr_fby (e1, e2)  -> add_dep true lhs e2 (add_dep false lhs e1 g)
157 170
    | Expr_pre e      -> add_dep true lhs e g
158
    | Expr_ident x -> add_var x g
171
    | Expr_ident x -> add_var lhs_is_mem lhs x (add_clock lhs_is_mem lhs rhs.expr_clock g)
159 172
    | Expr_access (e1, _)
160 173
    | Expr_power (e1, _) -> add_dep lhs_is_mem lhs e1 g
161 174
    | Expr_array a -> List.fold_right (add_dep lhs_is_mem lhs) a g
162 175
    | Expr_tuple t -> List.fold_right2 (fun l r -> add_dep lhs_is_mem [l] r) lhs t g
163
    | Expr_merge (c, hl) -> add_var c (List.fold_right (fun (_, h) -> add_dep lhs_is_mem lhs h) hl g)
176
    | Expr_merge (c, hl) -> add_var lhs_is_mem lhs c (List.fold_right (fun (_, h) -> add_dep lhs_is_mem lhs h) hl g)
164 177
    | Expr_ite   (c, t, e) -> add_dep lhs_is_mem lhs c (add_dep lhs_is_mem lhs t (add_dep lhs_is_mem lhs e g))
165 178
    | Expr_arrow (e1, e2)  -> add_dep lhs_is_mem lhs e2 (add_dep lhs_is_mem lhs e1 g)
166
    | Expr_when  (e, c, _)  -> add_dep lhs_is_mem lhs e (add_var c g)
179
    | Expr_when  (e, c, _)  -> add_dep lhs_is_mem lhs e (add_var lhs_is_mem lhs c g)
167 180
    | Expr_appl (f, e, None) ->
168 181
      if Basic_library.is_internal_fun f
169 182
    (* tuple component-wise dependency for internal operators *)
......
173 186
      else
174 187
	mashup_appl_dependencies f e g
175 188
    | Expr_appl (f, e, Some (r, _)) ->
176
      mashup_appl_dependencies f e (add_var r g)
189
      mashup_appl_dependencies f e (add_var lhs_is_mem lhs r g)
177 190
    | Expr_uclock  (e, _)
178 191
    | Expr_dclock  (e, _)
179 192
    | Expr_phclock (e, _) -> add_dep lhs_is_mem lhs e g 
......
182 195
  
183 196

  
184 197
(* Returns the dependence graph for node [n] *)
185
let dependence_graph mems n =
198
let dependence_graph mems non_inputs n =
186 199
  eq_var_cpt := 0;
187 200
  instance_var_cpt := 0;
188 201
  let g = new_graph (), new_graph () in
189
  let inputs = List.fold_left (fun inputs v -> ISet.add v.var_id inputs) ISet.empty n.node_inputs in
190 202
  (* Basic dependencies *)
191
  let g = List.fold_right (add_eq_dependencies mems inputs) n.node_eqs g in
203
  let g = List.fold_right (add_eq_dependencies mems non_inputs) n.node_eqs g in
192 204
  g
193 205

  
194 206
end
......
385 397

  
386 398
let global_dependency node =
387 399
  let mems = ExprDep.node_memory_variables node in
388
  let (g_non_mems, g_mems) = ExprDep.dependence_graph mems node in
400
  let non_inputs = ExprDep.node_non_input_variables node in
401
  let (g_non_mems, g_mems) = ExprDep.dependence_graph mems non_inputs node in
389 402
  (*Format.eprintf "g_non_mems: %a" pp_dep_graph g_non_mems;
390 403
  Format.eprintf "g_mems: %a" pp_dep_graph g_mems;*)
391 404
  CycleDetection.check_cycles g_non_mems;

Also available in: Unified diff