Revision 8f89eba8 src/clocks.ml
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