Project

General

Profile

Revision 8f89eba8

View differences:

src/causality.ml
379 379

  
380 380
end
381 381

  
382
(* Module used to compute static disjunction of variables based upon their clocks. *)
383
module Disjunction =
384
struct
385
  (* map: var |-> list of disjoint vars, sorted in increasing branch length,
386
     maybe removing shorter branches *)
387
  type clock_map = (ident, ident list) Hashtbl.t
388

  
389
  let rec add_vdecl map vdecls =
390
    match vdecls with
391
    | []         -> ()
392
    | vdecl :: q -> begin
393
		      Hashtbl.add map vdecl.var_id (List.fold_left (fun r v -> if Clocks.disjoint v.var_clock vdecl.var_clock then v::r else r) [] q);
394
                      add_vdecl map q
395
		    end
396

  
397
  let build_clock_map vdecls =
398
    let root_branch vdecl = Clocks.root vdecl.var_clock, Clocks.branch vdecl.var_clock in
399
    let map = Hashtbl.create 23 in
400
    begin
401
      add_vdecl map (List.sort (fun v1 v2 -> compare (root_branch v1) (root_branch v2)) vdecls);
402
      map
403
    end
404
end
405

  
382 406
let pp_dep_graph fmt g =
383 407
  begin
384 408
    Format.fprintf fmt "{ /* graph */@.";
src/clocks.ml
355 355
  let (a,b) = aux ck in
356 356
  simplify_rat (a,b)
357 357
    
358
(* Returns the pck clock parent of a clock *)
359
let rec pclock_parent ck =
358
(* Returns the clock root of a clock *)
359
let rec root ck =
360 360
  match (repr ck).cdesc with
361 361
  | Con (ck',_,_) | Clink ck' | Ccarrying (_,ck') ->
362
      pclock_parent ck'
362
      root ck'
363 363
  | Pck_up _ | Pck_down _ | Pck_phase _ | Pck_const _ | Cvar _ | Cunivar _ -> ck
364 364
  | Carrow _ | Ctuple _ -> failwith "Internal error pclock_parent"
365 365

  
366
(* Returns the branch of clock [ck] in its clock tree *)
367
let rec branch ck =
368
  let rec branch ck acc =
369
    match (repr ck).cdesc with
370
    | Ccarrying (_, ck) -> branch ck acc
371
    | Con (ck, cr, l)   -> branch ck ((cr, l) :: acc)
372
    | Ctuple _
373
    | Carrow _          -> assert false
374
    | _                 -> acc
375
  in branch ck [];;
376

  
377
(* Tests whether clock branches [br1] nd [br2] are statically disjoint *)
378
let rec disjoint_branches br1 br2 =
379
 match br1, br2 with
380
 | []          , _
381
 | _           , []           -> false
382
 | (cr1,l1)::q1, (cr2,l2)::q2 -> cr1 = cr2 && ((l1 <> l2) || disjoint_branches q1 q2);;
383

  
384
(* Disjunction relation between variables based upon their static clocks. *)
385
let disjoint ck1 ck2 =
386
 root ck1 = root ck2 && disjoint_branches (branch ck1) (branch ck2);;
387

  
366 388
(** [normalize pck] returns the normal form of clock [pck]. *)
367 389
let normalize pck =
368 390
  let changed = ref true in

Also available in: Unified diff