1 | include "Common.ma". |
---|
2 | |
---|
3 | record relations: Type[0] ≝ |
---|
4 | { Srel: status → status → Prop |
---|
5 | ; Crel: status → status → Prop |
---|
6 | }. |
---|
7 | |
---|
8 | definition Rrel ≝ λs,s'. |
---|
9 | ∀s1,s1'. succ s1 s → Crel s1 s1' → succ s1' s'. |
---|
10 | |
---|
11 | record simulation_conditions: Type[0] ≝ |
---|
12 | { simulate_tau: |
---|
13 | ∀s1,s2,s1'. |
---|
14 | as_execute s1 s2 (cost_act []) → |
---|
15 | Srel s1 s1' → |
---|
16 | ∃s2'. ∃t: raw_trace s1' s2'. |
---|
17 | Srel s2 s2' ∧ silent t |
---|
18 | ; simulate_label: |
---|
19 | ∀s1,s2,l,s1'. |
---|
20 | as_execute s1 s2 (cost_act [l]) → |
---|
21 | Srel s1 s1' → |
---|
22 | ∃s2',s2'',s2'''. |
---|
23 | ∃t1: raw_trace s1' s2'. |
---|
24 | as_execute s2' s2'' (cost_act [l]) ∧ |
---|
25 | ∃t3: raw_trace s2'' s2'''. |
---|
26 | Srel s2 s2''' ∧ silent t1 ∧ silent t3 |
---|
27 | ; simulate_call_pl: |
---|
28 | ∀s1,s2,l,s1'. |
---|
29 | post_labelled s1 → |
---|
30 | as_execute s1 s2 (call_act l) → |
---|
31 | Srel s1 s1' → |
---|
32 | ∃s2',s2'',s2'''. |
---|
33 | ∃t1: raw_trace s1' s2'. |
---|
34 | as_execute s2' s2'' (call_act l) ∧ |
---|
35 | ∃t3: raw_trace s2'' s2'''. |
---|
36 | Srel s2 s2''' ∧ silent t1 ∧ silent t3 |
---|
37 | ; simulate_ret_l: |
---|
38 | ∀s1,s2,l,s1'. |
---|
39 | as_execute s1 s2 (ret_act (Some l)) → |
---|
40 | Srel s1 s1' → |
---|
41 | ∃s2',s2'',s2'''. |
---|
42 | ∃t1: raw_trace s1' s2'. |
---|
43 | as_execute s2' s2'' (ret_act (Some l)) ∧ |
---|
44 | ∃t3: raw_trace s2'' s2'''. |
---|
45 | Srel s2 s2''' ∧ silent t1 ∧ silent t3 |
---|
46 | ; simulate_call_n: |
---|
47 | ∀s1,s2,l,s1'. |
---|
48 | as_execute s1 s2 (call_act l) → |
---|
49 | ¬ post_labelled … → |
---|
50 | Srel s1 s1' → |
---|
51 | ∃s2',s2'',s2'''. |
---|
52 | ∃t1: raw_trace s1' s2'. |
---|
53 | as_execute s2' s2'' (ret_act None) ∧ |
---|
54 | ∃t3: raw_trace s2'' s2'''. |
---|
55 | Srel s2 s2''' ∧ silent t1 ∧ silent t3 (*???? BUG? ∧ Rrel s2 s2''*) ∧ Crel s1 s2' |
---|
56 | ; simulate_ret_n: |
---|
57 | ∀s1,s2,l,s1'. |
---|
58 | as_execute s1 s2 (ret_act None) → |
---|
59 | Srel s1 s1' → |
---|
60 | ∃s2',s2'',s2'''. |
---|
61 | ∃t1: raw_trace s1' s2'. |
---|
62 | as_execute s2' s2'' (ret_act None) ∧ |
---|
63 | ∃t3: raw_trace s2'' s2'''. |
---|
64 | Srel s2 s2''' ∧ silent t1 ∧ silent t3 ∧ Rrel s2 s2'' |
---|
65 | }. |
---|
66 | |
---|
67 | theorem simulates_pre_mesurable: |
---|
68 | ∀s1,s2. ∀τ1: raw_trace … s1 s2. |
---|
69 | pre_measurable_trace … t1 → |
---|
70 | well_formed_trace … t1 → |
---|
71 | ∀s1'. |
---|
72 | S s1 s1' → |
---|
73 | ∃s2'. ∃t2: raw_trace … s1' s2'. |
---|
74 | pre_mesurable_trace … t2 ∧ |
---|
75 | well_formed_trace … t2 ∧ |
---|
76 | |t1| = |t2| ∧ |
---|
77 | S s2 s2'. |
---|
78 | |
---|
79 | (* IDEA: aggiungere stati di I/O e cambiare la semantica del linguaggio |
---|
80 | sorgente; aggiungere nella pre_measurable il vincolo nessuno stato e' di I/O; |
---|
81 | cambiare la definizione di traccia tornando a una sola etichetta sugli archi *) |
---|
82 | |
---|
83 | (* measurable fattorizzata sotto come measurable' |
---|
84 | definition measurable ≝ |
---|
85 | λL,s1,s2.λt: raw_trace … s1 s2. |
---|
86 | ∃L',s0,so. as_execute … s0 s1 L ∧ |
---|
87 | pre_measurable_trace … t ∧ |
---|
88 | well_formed_trace … t ∧ |
---|
89 | as_execute … s2 so L'. *) |
---|
90 | |
---|
91 | (*CSC: definire usando un record?*) |
---|
92 | record L_raw_trace ≝ |
---|
93 | { L_label: label |
---|
94 | ; L_s1: status |
---|
95 | ; L_s2: status |
---|
96 | ; L_t: raw_trace … s1 s2 |
---|
97 | ; L_ok: ∃s0. as_execute … s0 L_s1 L_label. |
---|
98 | (* o, nel caso in cui s1 sia lo stato iniziale, non serve nessun s0 |
---|
99 | e L e' la label init *) |
---|
100 | }. |
---|
101 | |
---|
102 | definition measurable' ≝ |
---|
103 | λt: L_raw_trace. |
---|
104 | ∃L',so. |
---|
105 | pre_measurable_trace … (L_t t) ∧ |
---|
106 | well_formed_trace … (L_t t) ∧ |
---|
107 | as_execute … (L_s2 t) so L'. |
---|
108 | (* o, nel caso in cui s2 sia uno stato finale, non serve nessun so e nessuna L' *) |
---|
109 | |
---|
110 | (*CSC: oppure fare il merge di L_raw_trace e measurable in un'unico record se |
---|
111 | non c'e' nulla di interessante sulle L_raw_trace non measurabili. Per esempio |
---|
112 | il teorema sotto sembra suggerire il merge *) |
---|
113 | |
---|
114 | definition unmovable_entry_label ≝ |
---|
115 | call, return post-labelled, init, I/O-uscente. |
---|
116 | |
---|
117 | definition unmovable_exit_lable ≝ |
---|
118 | I/O-entrante, stato finale (???). |
---|
119 | |
---|
120 | theorem simulates_L_raw_trace: |
---|
121 | ∀t: L_raw_trace. |
---|
122 | pre_measurable_trace … (L_t t1) → |
---|
123 | well_formed_trace … (L_t t1) → |
---|
124 | ∀s1'. |
---|
125 | S (L_s1 t) s1' → |
---|
126 | s1' -flat-→ (L_s1 t2) → |
---|
127 | ∃s2',t2: L_raw_trace. |
---|
128 | pre_mesurable_trace … (L_t t2) ∧ |
---|
129 | well_formed_trace … (L_t t2) ∧ |
---|
130 | |t1| = |t2| ∧ |
---|
131 | S (L_s2 t1) s2' ∧ |
---|
132 | (L_s2 t2) -flat-→ s2'. |
---|
133 | (* o, nel caso in cui (L_label t1) e' unmovable_entry_label nessuna coda prefissa e |
---|
134 | nel caso in cui ??? e' unmovable_exit_label, nessuna coda suffissa *) |
---|
135 | |
---|
136 | |
---|
137 | (*********************************************************************) |
---|
138 | |
---|
139 | (* quello che segue tentava di permettere di evitare l'emissione di label |
---|
140 | associate a codice morto *) |
---|
141 | |
---|
142 | replace_last x : weak_trace → weak_trace |
---|
143 | [] ⇒ [], Some x |
---|
144 | | l::t ⇒ |
---|
145 | let 〈t',x'〉 ≝ replace_last x t in |
---|
146 | match x' with |
---|
147 | [ None ⇒ l::t', None |
---|
148 | | Some x'' ⇒ [], Some x'' |
---|
149 | |
---|
150 | theorem simulates: |
---|
151 | ∀s1,s2. ∀τ1: raw_trace … s1 s2. |
---|
152 | pre_measurable_trace … t1 → |
---|
153 | well_formed_trace … t1. |
---|
154 | ∀l1: option NonFunctionalLabel. |
---|
155 | ∀s1'. |
---|
156 | S s1 s1' → |
---|
157 | ∃dead_labels. |
---|
158 | ∃s2'. ∃t2: raw_trace … s1' s2'. |
---|
159 | pre_mesurable_trace … t2 ∧ |
---|
160 | well_formed_trace … t2. |
---|
161 | ∃l2: option NonFunctionalLabel. |
---|
162 | match l1 with |
---|
163 | [ None ⇒ |
---|
164 | match l2 with |
---|
165 | [ None ⇒ |t1| = |t2| |
---|
166 | | Some l2' ⇒ |t1| = l2'::|t2| ] |
---|
167 | | Some l1' ⇒ |
---|
168 | match l2 with |
---|
169 | [ None ⇒ |t1| = replace_last l1' |t2| ∧ ends_with l1' t1 |
---|
170 | | Some l2' ⇒ |
---|
171 | if |t2| = [] then |t1| = [l1'] ∧ l2' = l1' |
---|
172 | else |t1| = l2' :: replace_last l1' |t2| ∧ ends_with l1' t1 |
---|
173 | ] |
---|
174 | ] |
---|