Project

General

Profile

Revision 45f0f48d src/clock_calculus.ml

View differences:

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] semi-unifies clocks [ck1] and [ck2]. Raises [Unify
393 276
    (ck1,ck2)] if the clocks are not semi-unifiable.*)
......
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