Ignore:
Timestamp:
Oct 19, 2011, 6:05:50 PM (8 years ago)
Author:
sacerdot
Message:
  • spill no longer used
  • BUG IN Interference: generating the destruct principle takes too long
  • ERTLToLTL not compiling ATM
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/Interference.ma

    r1282 r1423  
    11include "ERTL/ERTL.ma".
    22include "ERTL/liveness.ma".
     3include "basics/jmeq.ma".
    34
    45definition vertex ≝ register ⊎ Register.
     
    1718  ].
    1819
     20(* prop_colouring is the non interferece
     21   prop_colouring 2 and 3 together say that spilled_no is the number of spilled
     22   registers *)
     23(* Wilmer: the generation of the destruct principle diverges;
     24   Ctr-C make the file pass *)
    1925record coloured_graph (v: valuation): Type[1] ≝
    20 {
    21   colouring: vertex → decision;
    22   prop_colouring: ∀l. ∀v1, v2: vertex.
    23     is_member v1 (v l) → is_member v2 (v l) → colouring v1 ≠ colouring v2
     26{ colouring: vertex → decision
     27; spilled_no: nat
     28; prop_colouring: ∀l. ∀v1, v2: vertex.
     29   is_member v1 (v l) → is_member v2 (v l) → colouring v1 ≠ colouring v2
     30; prop_colouring2:
     31   ∀v1:vertex. (∃l. bool_to_Prop (is_member v1 (v l))) → ∀i. colouring v1 = decision_spill i → lt i spilled_no
     32; prop_colouring3:
     33   spilled_no = 0 ∨
     34    ∃l.∃v1:vertex. bool_to_Prop (is_member v1 (v l)) ∧ colouring v1 = decision_spill (minus spilled_no 1)
    2435}.
    2536
Note: See TracChangeset for help on using the changeset viewer.