Revision 45f0f48d src/clock_calculus.ml
src/clock_calculus.ml  

42  42 
 Ctuple ckl > 
43  43 
List.exists (occurs cvar) ckl 
44  44 
 Con (ck',_,_) > occurs cvar ck' 
45 
 Pck_up (ck',_) > occurs cvar ck' 

46 
 Pck_down (ck',_) > occurs cvar ck' 

47 
 Pck_phase (ck',_) > occurs cvar ck' 

48 
 Cvar _ > ck=cvar 

49 
 Cunivar _  Pck_const (_,_) > false 

45 
 Cvar > ck=cvar 

46 
 Cunivar > false 

50  47 
 Clink ck' > occurs cvar ck' 
51  48 
 Ccarrying (_,ck') > occurs cvar ck' 
52  49  
...  ...  
70  67 
 Ctuple clist > 
71  68 
List.iter generalize clist 
72  69 
 Con (ck',cr,_) > generalize ck'; generalize_carrier cr 
73 
 Cvar cset >


70 
 Cvar > 

74  71 
if ck.cscoped then 
75  72 
raise (Scope_clock ck); 
76 
ck.cdesc < Cunivar cset 

77 
 Pck_up (ck',_) > generalize ck' 

78 
 Pck_down (ck',_) > generalize ck' 

79 
 Pck_phase (ck',_) > generalize ck' 

80 
 Pck_const (_,_)  Cunivar _ > () 

73 
ck.cdesc < Cunivar 

74 
 Cunivar > () 

81  75 
 Clink ck' > 
82  76 
generalize ck' 
83  77 
 Ccarrying (cr,ck') > 
...  ...  
123  117 
 Con (ck',c,l) > 
124  118 
let c' = instantiate_carrier c inst_cr_vars in 
125  119 
{ck with cdesc = Con ((instantiate inst_ck_vars inst_cr_vars ck'),c',l)} 
126 
 Cvar _  Pck_const (_,_) > ck 

127 
 Pck_up (ck',k) > 

128 
{ck with cdesc = Pck_up ((instantiate inst_ck_vars inst_cr_vars ck'),k)} 

129 
 Pck_down (ck',k) > 

130 
{ck with cdesc = Pck_down ((instantiate inst_ck_vars inst_cr_vars ck'),k)} 

131 
 Pck_phase (ck',q) > 

132 
{ck with cdesc = Pck_phase ((instantiate inst_ck_vars inst_cr_vars ck'),q)} 

120 
 Cvar > ck 

133  121 
 Clink ck' > 
134  122 
{ck with cdesc = Clink (instantiate inst_ck_vars inst_cr_vars ck')} 
135  123 
 Ccarrying (cr,ck') > 
136  124 
let cr' = instantiate_carrier cr inst_cr_vars in 
137  125 
{ck with cdesc = 
138  126 
Ccarrying (cr',instantiate inst_ck_vars inst_cr_vars ck')} 
139 
 Cunivar cset >


127 
 Cunivar > 

140  128 
try 
141  129 
List.assoc ck.cid !inst_ck_vars 
142  130 
with Not_found > 
143 
let var = new_ck (Cvar cset) true in


131 
let var = new_ck Cvar true in


144  132 
inst_ck_vars := (ck.cid, var)::!inst_ck_vars; 
145  133 
var 
146  134  
147 
(** [subsume pck1 cset1] subsumes clock [pck1] by clock subset 

148 
[cset1]. The clock constraint is actually recursively transfered to 

149 
the clock variable appearing in [pck1] *) 

150 
let subsume pck1 cset1 = 

151 
let rec aux pck cset = 

152 
match cset with 

153 
 CSet_all > 

154 
() 

155 
 CSet_pck (k,(a,b)) > 

156 
match pck.cdesc with 

157 
 Cvar cset' > 

158 
pck.cdesc < Cvar (intersect cset' cset) 

159 
 Pck_up (pck',k') > 

160 
let rat = if a=0 then (0,1) else (a,b*k') in 

161 
aux pck' (CSet_pck ((k*k'),rat)) 

162 
 Pck_down (pck',k') > 

163 
let k''=k/(gcd k k') in 

164 
aux pck' (CSet_pck (k'',(a*k',b))) 

165 
 Pck_phase (pck',(a',b')) > 

166 
let (a'',b'')= max_rat (sum_rat (a,b) (a',b')) (0,1) in 

167 
aux pck' (CSet_pck (k, (a'',b''))) 

168 
 Pck_const (n,(a',b')) > 

169 
if n mod k <> 0  (max_rat (a,b) (a',b')) <> (a',b') then 

170 
raise (Subsume (pck1, cset1)) 

171 
 Clink pck' > 

172 
aux pck' cset 

173 
 Cunivar _ > () 

174 
 Ccarrying (_,ck') > 

175 
aux ck' cset 

176 
 _ > raise (Subsume (pck1, cset1)) 

177 
in 

178 
aux pck1 cset1 

179  135  
180  136 
let rec update_scope_carrier scoped cr = 
181  137 
if (not scoped) then 
...  ...  
196  152 
 Ctuple clist > 
197  153 
List.iter (update_scope scoped) clist 
198  154 
 Con (ck',cr,_) > update_scope scoped ck'(*; update_scope_carrier scoped cr*) 
199 
 Cvar cset > 

200 
ck.cdesc < Cvar cset 

201 
 Pck_up (ck',_) > update_scope scoped ck' 

202 
 Pck_down (ck',_) > update_scope scoped ck' 

203 
 Pck_phase (ck',_) > update_scope scoped ck' 

204 
 Pck_const (_,_)  Cunivar _ > () 

155 
 Cvar  Cunivar > () 

205  156 
 Clink ck' > 
206  157 
update_scope scoped ck' 
207  158 
 Ccarrying (cr,ck') > 
208  159 
update_scope_carrier scoped cr; update_scope scoped ck' 
209  160 
end 
210  161  
211 
(* Unifies two static pclocks. *) 

212 
let unify_static_pck ck1 ck2 = 

213 
if (period ck1 <> period ck2)  (phase ck1 <> phase ck2) then 

214 
raise (Unify (ck1,ck2)) 

215  162  
216  163 
(* Unifies two clock carriers *) 
217  164 
let unify_carrier cr1 cr2 = 
...  ...  
279  226 
with 
280  227 
 Unify (ck1',ck2') > 
281  228 
raise (Error (loc, Clock_clash (ck1',ck2'))) 
282 
 Subsume (ck,cset) > 

283 
raise (Error (loc, Clock_set_mismatch (ck,cset))) 

284  229 
 Mismatch (cr1,cr2) > 
285  230 
raise (Error (loc, Carrier_mismatch (cr1,cr2))) 
286  231  
...  ...  
292  237 
if ck1==ck2 then 
293  238 
() 
294  239 
else 
295 
let left_const = is_concrete_pck ck1 in 

296 
let right_const = is_concrete_pck ck2 in 

297 
if left_const && right_const then 

298 
unify_static_pck ck1 ck2 

299 
else 

300 
match ck1.cdesc,ck2.cdesc with 

301 
 Cvar cset1,Cvar cset2> 

302 
if ck1.cid < ck2.cid then 

303 
begin 

304 
ck2.cdesc < Clink (simplify ck1); 

305 
update_scope ck2.cscoped ck1; 

306 
subsume ck1 cset2 

307 
end 

308 
else 

309 
begin 

310 
ck1.cdesc < Clink (simplify ck2); 

311 
update_scope ck1.cscoped ck2; 

312 
subsume ck2 cset1 

313 
end 

314 
 Cvar cset, Pck_up (_,_)  Cvar cset, Pck_down (_,_) 

315 
 Cvar cset, Pck_phase (_,_)  Cvar cset, Pck_const (_,_) > 

316 
if (occurs ck1 ck2) then 

317 
begin 

318 
if (simplify ck2 = ck1) then 

319 
ck2.cdesc < Clink (simplify ck1) 

320 
else 

321 
raise (Unify (ck1,ck2)); 

322 
end 

323 
else 

324 
begin 

325 
ck1.cdesc < Clink (simplify ck2); 

326 
subsume ck2 cset 

327 
end 

328 
 Pck_up (_,_), Cvar cset  Pck_down (_,_), Cvar cset 

329 
 Pck_phase (_,_), Cvar cset  Pck_const (_,_), Cvar cset > 

330 
if (occurs ck2 ck1) then 

331 
begin 

332 
if ((simplify ck1) = ck2) then 

333 
ck1.cdesc < Clink (simplify ck2) 

334 
else 

335 
raise (Unify (ck1,ck2)); 

336 
end 

337 
else 

338 
begin 

339 
ck2.cdesc < Clink (simplify ck1); 

340 
subsume ck1 cset 

341 
end 

342 
 (Cvar cset,_) when (not (occurs ck1 ck2)) > 

343 
subsume ck2 cset; 

344 
update_scope ck1.cscoped ck2; 

345 
ck1.cdesc < Clink (simplify ck2) 

346 
 (_, (Cvar cset)) when (not (occurs ck2 ck1)) > 

347 
subsume ck1 cset; 

348 
update_scope ck2.cscoped ck1; 

349 
ck2.cdesc < Clink (simplify ck1) 

350 
 Ccarrying (cr1,ck1'),Ccarrying (cr2,ck2') > 

351 
unify_carrier cr1 cr2; 

352 
unify ck1' ck2' 

353 
 Ccarrying (_,_),_  _,Ccarrying (_,_) > 

354 
raise (Unify (ck1,ck2)) 

355 
 Carrow (c1,c2), Carrow (c1',c2') > 

356 
unify c1 c1'; unify c2 c2' 

357 
 Ctuple ckl1, Ctuple ckl2 > 

358 
if (List.length ckl1) <> (List.length ckl2) then 

359 
raise (Unify (ck1,ck2)); 

360 
List.iter2 unify ckl1 ckl2 

361 
 Con (ck',c1,l1), Con (ck'',c2,l2) when l1=l2 > 

362 
unify_carrier c1 c2; 

363 
unify ck' ck'' 

364 
 Pck_const (i,r), Pck_const (i',r') > 

365 
if i<>i'  r <> r' then 

366 
raise (Unify (ck1,ck2)) 

367 
 (_, Pck_up (pck2',k)) when (not right_const) > 

368 
let ck1' = simplify (new_ck (Pck_down (ck1,k)) true) in 

369 
unify ck1' pck2' 

370 
 (_,Pck_down (pck2',k)) when (not right_const) > 

371 
subsume ck1 (CSet_pck (k,(0,1))); 

372 
let ck1' = simplify (new_ck (Pck_up (ck1,k)) true) in 

373 
unify ck1' pck2' 

374 
 (_,Pck_phase (pck2',(a,b))) when (not right_const) > 

375 
subsume ck1 (CSet_pck (b,(a,b))); 

376 
let ck1' = simplify (new_ck (Pck_phase (ck1,(a,b))) true) in 

377 
unify ck1' pck2' 

378 
 Pck_up (pck1',k),_ > 

379 
let ck2' = simplify (new_ck (Pck_down (ck2,k)) true) in 

380 
unify pck1' ck2' 

381 
 Pck_down (pck1',k),_ > 

382 
subsume ck2 (CSet_pck (k,(0,1))); 

383 
let ck2' = simplify (new_ck (Pck_up (ck2,k)) true) in 

384 
unify pck1' ck2' 

385 
 Pck_phase (pck1',(a,b)),_ > 

386 
subsume ck2 (CSet_pck (b,(a,b))); 

387 
let ck2' = simplify (new_ck (Pck_phase (ck2,(a,b))) true) in 

388 
unify pck1' ck2' 

389 
 Cunivar _, _  _, Cunivar _ > () 

390 
 _,_ > raise (Unify (ck1,ck2)) 

240 
match ck1.cdesc,ck2.cdesc with 

241 
 Cvar, Cvar > 

242 
if ck1.cid < ck2.cid then 

243 
begin 

244 
ck2.cdesc < Clink (simplify ck1); 

245 
update_scope ck2.cscoped ck1 

246 
end 

247 
else 

248 
begin 

249 
ck1.cdesc < Clink (simplify ck2); 

250 
update_scope ck1.cscoped ck2 

251 
end 

252 
 (Cvar, _) when (not (occurs ck1 ck2)) > 

253 
update_scope ck1.cscoped ck2; 

254 
ck1.cdesc < Clink (simplify ck2) 

255 
 (_, Cvar) when (not (occurs ck2 ck1)) > 

256 
update_scope ck2.cscoped ck1; 

257 
ck2.cdesc < Clink (simplify ck1) 

258 
 Ccarrying (cr1,ck1'),Ccarrying (cr2,ck2') > 

259 
unify_carrier cr1 cr2; 

260 
unify ck1' ck2' 

261 
 Ccarrying (_,_),_  _,Ccarrying (_,_) > 

262 
raise (Unify (ck1,ck2)) 

263 
 Carrow (c1,c2), Carrow (c1',c2') > 

264 
unify c1 c1'; unify c2 c2' 

265 
 Ctuple ckl1, Ctuple ckl2 > 

266 
if (List.length ckl1) <> (List.length ckl2) then 

267 
raise (Unify (ck1,ck2)); 

268 
List.iter2 unify ckl1 ckl2 

269 
 Con (ck',c1,l1), Con (ck'',c2,l2) when l1=l2 > 

270 
unify_carrier c1 c2; 

271 
unify ck' ck'' 

272 
 Cunivar, _  _, Cunivar > () 

273 
 _,_ > raise (Unify (ck1,ck2)) 

391  274  
392  275 
(** [unify ck1 ck2] semiunifies clocks [ck1] and [ck2]. Raises [Unify 
393  276 
(ck1,ck2)] if the clocks are not semiunifiable.*) 
...  ...  
398  281 
() 
399  282 
else 
400  283 
match ck1.cdesc,ck2.cdesc with 
401 
 Cvar cset1,Cvar cset2>


284 
 Cvar, Cvar >


402  285 
if ck1.cid < ck2.cid then 
403  286 
begin 
404  287 
ck2.cdesc < Clink (simplify ck1); 
...  ...  
409  292 
ck1.cdesc < Clink (simplify ck2); 
410  293 
update_scope ck1.cscoped ck2 
411  294 
end 
412 
 (Cvar cset,_) > raise (Unify (ck1,ck2))


413 
 (_, (Cvar cset)) when (not (occurs ck2 ck1)) >


295 
 (Cvar, _) > raise (Unify (ck1,ck2))


296 
 (_, Cvar) when (not (occurs ck2 ck1)) >


414  297 
update_scope ck2.cscoped ck1; 
415  298 
ck2.cdesc < Clink (simplify ck1) 
416  299 
 Ccarrying (cr1,ck1'),Ccarrying (cr2,ck2') > 
...  ...  
430  313 
 Con (ck',c1,l1), Con (ck'',c2,l2) when l1=l2 > 
431  314 
semi_unify_carrier c1 c2; 
432  315 
semi_unify ck' ck'' 
433 
 Cunivar _, _  _, Cunivar _ > ()


316 
 Cunivar, _  _, Cunivar > ()


434  317 
 _,_ > raise (Unify (ck1,ck2)) 
435  318  
436  319 
(* Returns the value corresponding to a pclock (integer) factor 
...  ...  
456  339 
with 
457  340 
 Unify (ck1',ck2') > 
458  341 
raise (Error (loc, Clock_clash (ck1',ck2'))) 
459 
 Subsume (ck,cset) > 

460 
raise (Error (loc, Clock_set_mismatch (ck,cset))) 

461  342 
 Mismatch (cr1,cr2) > 
462  343 
raise (Error (loc, Carrier_mismatch (cr1,cr2))) 
463  344  
...  ...  
467  348 
with 
468  349 
 Unify (ck1',ck2') > 
469  350 
raise (Error (loc, Clock_clash (ck1',ck2'))) 
470 
 Subsume (ck,cset) > 

471 
raise (Error (loc, Clock_set_mismatch (ck,cset))) 

472  351 
 Mismatch (cr1,cr2) > 
473  352 
raise (Error (loc, Carrier_mismatch (cr1,cr2))) 
474  353  
...  ...  
500  379 
with 
501  380 
 Unify (ck1',ck2') > 
502  381 
raise (Error (loc, Clock_clash (ck1',ck2'))) 
503 
 Subsume (ck,cset) > 

504 
raise (Error (loc, Clock_set_mismatch (ck,cset))) 

505  382 
 Mismatch (cr1,cr2) > 
506  383 
raise (Error (loc, Carrier_mismatch (cr1,cr2))) 
507  384  
...  ...  
515  392 
let rec aux ck = 
516  393 
match (repr ck).cdesc with 
517  394 
 Con _ 
518 
 Cvar _ >


395 
 Cvar > 

519  396 
begin 
520  397 
match !ck_var with 
521  398 
 None > 
...  ...  
539  416 
let ck_var = ref ref_ck_opt in 
540  417 
let rec aux ck = 
541  418 
match (repr ck).cdesc with 
542 
 Cvar _ >


419 
 Cvar > 

543  420 
begin 
544  421 
match !ck_var with 
545  422 
 None > 
...  ...  
744  621 
let clock_coreclock env cck id loc scoped = 
745  622 
match cck.ck_dec_desc with 
746  623 
 Ckdec_any > new_var scoped 
747 
 Ckdec_pclock (n,(a,b)) > 

748 
let ck = new_ck (Pck_const (n,(a,b))) scoped in 

749 
if n mod b <> 0 then raise (Error (loc,Invalid_const ck)); 

750 
ck 

751  624 
 Ckdec_bool cl > 
752  625 
let temp_env = Env.add_value env id (new_var true) in 
753  626 
(* We just want the id to be present in the environment *) 
...  ...  
837  710 
 Carrow (ck1,ck2) > aux ck1; aux ck2 
838  711 
 Ctuple cl > List.iter aux cl 
839  712 
 Con (ck',_,_) > aux ck' 
840 
 Pck_up (_,_)  Pck_down (_,_)  Pck_phase (_,_) > 

841 
raise (Error (loc, (Invalid_imported_clock ck_node))) 

842 
 Pck_const (n,p) > 

843 
begin 

844 
match !pck with 

845 
 None > pck := Some (n,p) 

846 
 Some (n',p') > 

847 
if (n,p) <> (n',p') then 

848 
raise (Error (loc, (Invalid_imported_clock ck_node))) 

849 
end 

850  713 
 Clink ck' > aux ck' 
851  714 
 Ccarrying (_,ck') > aux ck' 
852 
 Cvar _  Cunivar _ >


715 
 Cvar  Cunivar >


853  716 
match !pck with 
854  717 
 None > () 
855  718 
 Some (_,_) > 
Also available in: Unified diff