source: src/ERTL/Interference.ma @ 1423

Last change on this file since 1423 was 1423, checked in by sacerdot, 8 years ago
  • spill no longer used
  • BUG IN Interference: generating the destruct principle takes too long
  • ERTLToLTL not compiling ATM
File size: 1.2 KB
Line 
1include "ERTL/ERTL.ma".
2include "ERTL/liveness.ma".
3include "basics/jmeq.ma".
4
5definition vertex ≝ register ⊎ Register.
6
7inductive decision: Type[0] ≝
8  | decision_spill: nat → decision
9  | decision_colour: Register → decision.
10
11definition is_member ≝
12  λvertex.
13  λregister_lattice.
14  let 〈l, r〉 ≝ register_lattice in
15  match vertex with
16  [ inl v ⇒ set_member ? (eq_identifier RegisterTag) v l
17  | inr v ⇒ set_member ? eq_Register v r
18  ].
19
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 *)
25record coloured_graph (v: valuation): Type[1] ≝
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)
35}.
36
37axiom build: ∀valuation. coloured_graph valuation.
Note: See TracBrowser for help on using the repository browser.