Revision 8f89eba8
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