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