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