Project

General

Profile

Revision 7ecdb0aa src/causality.ml

View differences:

src/causality.ml
447 447
(* Module used to compute static disjunction of variables based upon their clocks. *)
448 448
module Disjunction =
449 449
struct
450
  (* map: var |-> list of disjoint vars, sorted in increasing branch length,
451
     maybe removing shorter branches *)
452
  type clock_map = (ident, ident list) Hashtbl.t
450
  module ClockedIdentModule =
451
  struct
452
    type t = var_decl
453
    let root_branch vdecl = Clocks.root vdecl.var_clock, Clocks.branch vdecl.var_clock
454
    let compare v1 v2 = compare (root_branch v2) (root_branch v1)
455
  end
456

  
457
  module CISet = Set.Make(ClockedIdentModule)
453 458

  
454
  let rec add_vdecl map vdecls =
455
    match vdecls with
456
    | []         -> ()
457
    | vdecl :: q -> begin
458
		      Hashtbl.add map vdecl.var_id (List.fold_left (fun r v -> if Clocks.disjoint v.var_clock vdecl.var_clock then v.var_id::r else r) [] q);
459
                      add_vdecl map q
460
		    end
459
  (* map: var |-> list of disjoint vars, sorted in increasing branch length order,
460
     maybe removing shorter branches *)
461
  type clock_map = (ident, var_decl list) Hashtbl.t
461 462

  
462 463
  let clock_disjoint_map vdecls =
463
    let root_branch vdecl = Clocks.root vdecl.var_clock, Clocks.branch vdecl.var_clock in
464 464
    let map = Hashtbl.create 23 in
465 465
    begin
466
      add_vdecl map (List.sort (fun v1 v2 -> compare (root_branch v1) (root_branch v2)) vdecls);
466
      List.iter
467
	(fun v1 -> let disj_v1 =
468
		     List.fold_left
469
		       (fun res v2 -> if Clocks.disjoint v1.var_clock v2.var_clock then CISet.add v2 res else res)
470
		       CISet.empty
471
		       vdecls in
472
		   (* disjoint vdecls are stored in increasing branch length order *)
473
		   Hashtbl.add map v1.var_id disj_v1)
474
	vdecls;
467 475
      map
468 476
    end
469 477

  
478
  (* replace variable [v] by [v'] in disjunction [map]. Then:
479
     - the mapping v |-> ... disappears
480
     - the mapping v' becomes v' |-> (map v) inter (map v')
481
     - other mappings become x |-> (map x) \ (if v in x then v else v')
482
  *)
483
  let replace_in_disjoint_map map v v' =
484
    begin
485
      Hashtbl.remove map v.var_id;
486
      Hashtbl.replace map v'.var_id (CISet.inter (Hashtbl.find map v.var_id) (Hashtbl.find map v'.var_id));
487
      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;
488
    end
489

  
470 490
  let pp_disjoint_map fmt map =
471 491
    begin
472 492
      Format.fprintf fmt "{ /* disjoint map */@.";
473
      Hashtbl.iter (fun k v -> Format.fprintf fmt "%s # { %a }@." k (Utils.fprintf_list ~sep:", " Format.pp_print_string) v) map;
493
      Hashtbl.iter (fun k v -> Format.fprintf fmt "%s # { %a }@." k (Utils.fprintf_list ~sep:", " Printers.pp_var_name) (CISet.elements v)) map;
474 494
      Format.fprintf fmt "}@."
475 495
    end
476 496
end

Also available in: Unified diff