Project

General

Profile

Revision 8f89eba8 src/clocks.ml

View differences:

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