Revision 1837ce98 src/causality.ml
src/causality.ml  

141  141 
let node_output_variables nd = 
142  142 
List.fold_left (fun outputs v > ISet.add v.var_id outputs) ISet.empty nd.node_outputs 
143  143  
144 
let node_auxiliary_variables nd = 

145 
ISet.diff (node_local_variables nd) (node_memory_variables nd) 

146  
144  147 
let node_variables nd = 
145  148 
let inputs = node_input_variables nd in 
146  149 
let inoutputs = List.fold_left (fun inoutputs v > ISet.add v.var_id inoutputs) inputs nd.node_outputs in 
...  ...  
452  455  
453  456 
(* map: var > list of disjoint vars, sorted in increasing branch length order, 
454  457 
maybe removing shorter branches *) 
455 
type clock_map = (ident, var_decl list) Hashtbl.t


458 
type clock_map = (ident, ident list) Hashtbl.t


456  459  
457  460 
let clock_disjoint_map vdecls = 
458  461 
let map = Hashtbl.create 23 in 
...  ...  
460  463 
List.iter 
461  464 
(fun v1 > let disj_v1 = 
462  465 
List.fold_left 
463 
(fun res v2 > if Clocks.disjoint v1.var_clock v2.var_clock then CISet.add v2 res else res)


464 
CISet.empty


466 
(fun res v2 > if Clocks.disjoint v1.var_clock v2.var_clock then ISet.add v2.var_id res else res)


467 
ISet.empty 

465  468 
vdecls in 
466  469 
(* disjoint vdecls are stored in increasing branch length order *) 
467  470 
Hashtbl.add map v1.var_id disj_v1) 
...  ...  
470  473 
end 
471  474  
472  475 
(* replace variable [v] by [v'] in disjunction [map]. Then: 
473 
 the mapping v > ... disappears 

474 
 the mapping v' becomes v' > (map v) inter (map v') 

475 
 other mappings become x > (map x) \ (if v in x then v else v') 

476 
 the mapping v' becomes v' > (map v) inter (map v') 

477 
 the mapping v > ... then disappears 

478 
 other mappings become x > (map x) \ (if v in x then v else v') 

479 


476  480 
*) 
477  481 
let replace_in_disjoint_map map v v' = 
478  482 
begin 
479 
Hashtbl.remove map v.var_id;


480 
Hashtbl.replace map v'.var_id (CISet.inter (Hashtbl.find map v.var_id) (Hashtbl.find map v'.var_id));


481 
Hashtbl.iter (fun x map_x > Hashtbl.replace map x (CISet.remove (if CISet.mem v map_x then v else v') map_x)) map;


483 
Hashtbl.replace map v' (ISet.inter (Hashtbl.find map v) (Hashtbl.find map v'));


484 
Hashtbl.remove map v;


485 
Hashtbl.iter (fun x map_x > Hashtbl.replace map x (ISet.remove (if ISet.mem v map_x then v else v') map_x)) map;


482  486 
end 
483  487  
484  488 
let pp_disjoint_map fmt map = 
485  489 
begin 
486  490 
Format.fprintf fmt "{ /* disjoint map */@."; 
487 
Hashtbl.iter (fun k v > Format.fprintf fmt "%s # { %a }@." k (Utils.fprintf_list ~sep:", " Printers.pp_var_name) (CISet.elements v)) map;


491 
Hashtbl.iter (fun k v > Format.fprintf fmt "%s # { %a }@." k (Utils.fprintf_list ~sep:", " Format.pp_print_string) (ISet.elements v)) map;


488  492 
Format.fprintf fmt "}@." 
489  493 
end 
490  494 
end 
Also available in: Unified diff