1 | include "Common.ma". |
---|
2 | include "Traces.ma". |
---|
3 | |
---|
4 | record relations (S : abstract_status) : Type[0] ≝ |
---|
5 | { Srel: S → S → Prop |
---|
6 | ; Crel: S → S → Prop |
---|
7 | }. |
---|
8 | |
---|
9 | definition Rrel ≝ λS : abstract_status.λrel : relations S.λs,s' : S. |
---|
10 | ∀s1,s1'. as_syntactical_succ S s1 s → Crel … rel s1 s1' → as_syntactical_succ S s1' s'. |
---|
11 | |
---|
12 | record simulation_conditions (S : abstract_status) (rel : relations S) : Type[0] ≝ |
---|
13 | { simulate_tau: |
---|
14 | ∀s1,s2,s1' : S. |
---|
15 | as_execute … (cost_act (None ?)) s1 s1'→ |
---|
16 | Srel … rel s1 s2 → |
---|
17 | ∃s2'. ∃t: raw_trace S s2 s2'. |
---|
18 | Srel … rel s2 s2' ∧ silent_trace … t |
---|
19 | ; simulate_label: |
---|
20 | ∀s1,s2,l,s1'. |
---|
21 | as_execute S (cost_act (Some ? l)) s1 s1' → |
---|
22 | Srel … rel s1 s2 → |
---|
23 | ∃s2',s2'',s2'''. |
---|
24 | ∃t1: raw_trace S s2 s2'. |
---|
25 | as_execute … (cost_act (Some ? l)) s2' s2'' ∧ |
---|
26 | ∃t3: raw_trace S s2'' s2'''. |
---|
27 | Srel … rel s1' s2''' ∧ silent_trace … t1 ∧ silent_trace … t3 |
---|
28 | ; simulate_call_pl: |
---|
29 | ∀s1,s2,s1' : S.∀f,l. |
---|
30 | is_call_post_label … s1 → |
---|
31 | as_execute … (call_act f l) s1 s1' → |
---|
32 | Srel … rel s1 s2 → |
---|
33 | ∃s2',s2'',s2'''. |
---|
34 | ∃t1: raw_trace S s2 s2'. |
---|
35 | as_execute … (call_act f l) s2' s2'' ∧ |
---|
36 | ∃t3: raw_trace S s2'' s2'''. |
---|
37 | Srel … rel s1' s2''' ∧ silent_trace … t1 ∧ silent_trace … t3 |
---|
38 | ; simulate_ret_l: |
---|
39 | ∀s1,s2,s1' : S.∀l. |
---|
40 | as_execute S (ret_act (Some ? l)) s1 s1' → |
---|
41 | Srel … rel s1 s2 → |
---|
42 | ∃s2',s2'',s2'''. |
---|
43 | ∃t1: raw_trace S s2 s2'. |
---|
44 | as_execute … (ret_act (Some ? l)) s2' s2'' ∧ |
---|
45 | ∃t3: raw_trace S s2'' s2'''. |
---|
46 | Srel … rel s2 s2''' ∧ silent_trace … t1 ∧ silent_trace … t3 |
---|
47 | ; simulate_call_n: |
---|
48 | ∀s1,s2,s1' : S.∀f,l. |
---|
49 | as_execute … (call_act f l) s1 s1' → |
---|
50 | ¬ is_call_post_label … s1 → |
---|
51 | Srel … rel s1 s2 → |
---|
52 | ∃s2',s2'',s2'''. |
---|
53 | ∃t1: raw_trace S s2 s2'. |
---|
54 | as_execute … (call_act f l) s2' s2'' ∧ |
---|
55 | ∃t3: raw_trace S s2'' s2'''. |
---|
56 | Srel … rel s1' s2''' ∧ silent_trace … t1 ∧ silent_trace … t3 |
---|
57 | ∧ Crel … rel s1 s2' |
---|
58 | ; simulate_ret_n: |
---|
59 | ∀s1,s2,s1' : S. |
---|
60 | as_execute … (ret_act (None ?)) s1 s1' → |
---|
61 | Srel … rel s1 s2 → |
---|
62 | ∃s2',s2'',s2'''. |
---|
63 | ∃t1: raw_trace S s2 s2'. |
---|
64 | as_execute … (ret_act (None ?)) s2' s2'' ∧ |
---|
65 | ∃t3: raw_trace S s2'' s2'''. |
---|
66 | Srel … rel s1' s2''' ∧ silent_trace … t1 ∧ silent_trace … t3 |
---|
67 | ∧ Rrel … rel s2 s2'' |
---|
68 | }. |
---|
69 | |
---|
70 | let rec get_costlabels_of_trace (S : abstract_status) (st1 : S) (st2 : S) |
---|
71 | (t : raw_trace S st1 st2) on t : list CostLabel ≝ |
---|
72 | match t with |
---|
73 | [ t_base st ⇒ [ ] |
---|
74 | | t_ind st1' st2' st3' l prf t' ⇒ |
---|
75 | let tl ≝ get_costlabels_of_trace … t' in |
---|
76 | match l with |
---|
77 | [ call_act f c ⇒ c :: tl |
---|
78 | | ret_act x ⇒ match x with |
---|
79 | [ Some c ⇒ ret_act_label_to_cost_label c :: tl |
---|
80 | | None ⇒ tl |
---|
81 | ] |
---|
82 | | cost_act x ⇒ match x with |
---|
83 | [ Some c ⇒ a_non_functional_label c :: tl |
---|
84 | | None ⇒ tl |
---|
85 | ] |
---|
86 | | init_act ⇒ tl |
---|
87 | ] |
---|
88 | ]. |
---|
89 | |
---|
90 | |
---|
91 | theorem simulates_pre_mesurable: |
---|
92 | ∀S : abstract_status.∀rel : relations S. |
---|
93 | ∀s1,s1' : S. ∀t1: raw_trace S s1 s1'. |
---|
94 | pre_measurable_trace … t1 → |
---|
95 | well_formed_trace … t1 → ∀s2.Srel … rel s1 s2 → |
---|
96 | ∃s2'. ∃t2: raw_trace … s1' s2'. |
---|
97 | pre_measurable_trace … t2 ∧ |
---|
98 | well_formed_trace … t2 ∧ |
---|
99 | get_costlabels_of_trace … t1 = get_costlabels_of_trace … t2 ∧ |
---|
100 | Srel … rel s2 s2'. |
---|
101 | cases daemon (*TODO*) |
---|
102 | qed. |
---|
103 | |
---|
104 | (* IDEA: aggiungere stati di I/O e cambiare la semantica del linguaggio |
---|
105 | sorgente; aggiungere nella pre_measurable il vincolo nessuno stato e' di I/O; |
---|
106 | cambiare la definizione di traccia tornando a una sola etichetta sugli archi *) |
---|
107 | |
---|
108 | (* measurable fattorizzata sotto come measurable' |
---|
109 | definition measurable ≝ |
---|
110 | λL,s1,s2.λt: raw_trace … s1 s2. |
---|
111 | ∃L',s0,so. as_execute … s0 s1 L ∧ |
---|
112 | pre_measurable_trace … t ∧ |
---|
113 | well_formed_trace … t ∧ |
---|
114 | as_execute … s2 so L'. *) |
---|
115 | |
---|
116 | record LR_raw_trace (S : abstract_status) : Type[0] ≝ |
---|
117 | { L_label: ActionLabel |
---|
118 | ; R_label : ActionLabel |
---|
119 | ; LR_s1: S |
---|
120 | ; LR_s2: S |
---|
121 | ; LR_t : raw_trace S LR_s1 LR_s2 |
---|
122 | ; L_init_ok : bool_to_Prop(as_initial … LR_s1) → L_label = init_act |
---|
123 | ; L_noinit_ok : |
---|
124 | bool_to_Prop (¬ as_initial … LR_s1) → |
---|
125 | ∃s0. as_execute … L_label s0 LR_s1 ∧ is_costlabelled_act L_label |
---|
126 | ∧ ¬ bool_to_Prop (is_act_io_entering S L_label) |
---|
127 | ; R_nonfin_ok : |
---|
128 | bool_to_Prop (¬ as_final … (LR_s2)) → |
---|
129 | ∃so.as_execute … R_label LR_s2 so ∧ is_costlabelled_act R_label |
---|
130 | ∧ ¬ bool_to_Prop (is_act_io_exiting S R_label) |
---|
131 | }. |
---|
132 | |
---|
133 | definition measurable ≝ λS : abstract_status.λt : LR_raw_trace S. |
---|
134 | pre_measurable_trace … (LR_t … t) ∧ well_formed_trace … (LR_t … t). |
---|
135 | |
---|
136 | |
---|
137 | (*CSC: oppure fare il merge di L_raw_trace e measurable in un'unico record se |
---|
138 | non c'e' nulla di interessante sulle L_raw_trace non measurabili. Per esempio |
---|
139 | il teorema sotto sembra suggerire il merge *) |
---|
140 | |
---|
141 | definition unmovable_entry_label ≝ |
---|
142 | λS : abstract_status.λl. |
---|
143 | match l with |
---|
144 | [ call_act _ _ ⇒ false |
---|
145 | | ret_act _ ⇒ false |
---|
146 | | cost_act x ⇒ match x with [Some c ⇒ is_io_exiting S c |
---|
147 | | None ⇒ false |
---|
148 | ] |
---|
149 | | init_act ⇒ true |
---|
150 | ]. |
---|
151 | |
---|
152 | definition unmovable_exit_label ≝ |
---|
153 | λS : abstract_status.λl. |
---|
154 | match l with |
---|
155 | [ call_act _ _ ⇒ false |
---|
156 | | ret_act _ ⇒ false |
---|
157 | | cost_act x ⇒ match x with [Some c ⇒ is_io_entering S c |
---|
158 | | None ⇒ false |
---|
159 | ] |
---|
160 | | init_act ⇒ false |
---|
161 | ]. |
---|
162 | |
---|
163 | theorem simulates_LR_raw_trace : |
---|
164 | ∀S : abstract_status. |
---|
165 | ∀t : LR_raw_trace S. |
---|
166 | ∀rel : relations S. |
---|
167 | measurable S t → |
---|
168 | ∀s1'.Srel … rel (LR_s1 … t) s1' → |
---|
169 | ∃ t' : LR_raw_trace S. |
---|
170 | measurable S t' ∧ |
---|
171 | if as_initial … (LR_s1 … t) ∨ unmovable_entry_label S (L_label … t) then |
---|
172 | LR_s1 … t' = s1' |
---|
173 | else |
---|
174 | ∃pre : raw_trace … (LR_s1 … t') s1'.trace_prefix … pre (LR_t … t') |
---|
175 | ∧ ∃s1''.Srel … rel (LR_s2 … t) s1'' ∧ |
---|
176 | if as_final … (LR_s2 … t) ∨ unmovable_exit_label S (R_label … t) then |
---|
177 | LR_s2 … t' = s1'' |
---|
178 | else |
---|
179 | ∃suff : raw_trace … s1'' (LR_s2 … t'). trace_suffix … suff (LR_t … t') |
---|
180 | ∧ |
---|
181 | get_costlabels_of_trace … (LR_t … t) = get_costlabels_of_trace … (LR_t … t'). |
---|
182 | cases daemon (*TODO*) |
---|
183 | qed. |
---|
184 | |
---|
185 | xxxx |
---|
186 | |
---|
187 | theorem simulates_L_raw_trace: |
---|
188 | ∀t: L_raw_trace. |
---|
189 | pre_measurable_trace … (L_t t1) → |
---|
190 | well_formed_trace … (L_t t1) → |
---|
191 | ∀s1'. |
---|
192 | S (L_s1 t) s1' → |
---|
193 | s1' -flat-→ (L_s1 t2) → |
---|
194 | ∃s2',t2: L_raw_trace. |
---|
195 | pre_mesurable_trace … (L_t t2) ∧ |
---|
196 | well_formed_trace … (L_t t2) ∧ |
---|
197 | |t1| = |t2| ∧ |
---|
198 | S (L_s2 t1) s2' ∧ |
---|
199 | (L_s2 t2) -flat-→ s2'. |
---|
200 | (* o, nel caso in cui (L_label t1) e' unmovable_entry_label nessuna coda prefissa e |
---|
201 | nel caso in cui ??? e' unmovable_exit_label, nessuna coda suffissa *) |
---|
202 | |
---|
203 | |
---|
204 | (*********************************************************************) |
---|
205 | |
---|
206 | (* quello che segue tentava di permettere di evitare l'emissione di label |
---|
207 | associate a codice morto *) |
---|
208 | |
---|
209 | replace_last x : weak_trace → weak_trace |
---|
210 | [] ⇒ [], Some x |
---|
211 | | l::t ⇒ |
---|
212 | let 〈t',x'〉 ≝ replace_last x t in |
---|
213 | match x' with |
---|
214 | [ None ⇒ l::t', None |
---|
215 | | Some x'' ⇒ [], Some x'' |
---|
216 | |
---|
217 | theorem simulates: |
---|
218 | ∀s1,s2. ∀τ1: raw_trace … s1 s2. |
---|
219 | pre_measurable_trace … t1 → |
---|
220 | well_formed_trace … t1. |
---|
221 | ∀l1: option NonFunctionalLabel. |
---|
222 | ∀s1'. |
---|
223 | S s1 s1' → |
---|
224 | ∃dead_labels. |
---|
225 | ∃s2'. ∃t2: raw_trace … s1' s2'. |
---|
226 | pre_mesurable_trace … t2 ∧ |
---|
227 | well_formed_trace … t2. |
---|
228 | ∃l2: option NonFunctionalLabel. |
---|
229 | match l1 with |
---|
230 | [ None ⇒ |
---|
231 | match l2 with |
---|
232 | [ None ⇒ |t1| = |t2| |
---|
233 | | Some l2' ⇒ |t1| = l2'::|t2| ] |
---|
234 | | Some l1' ⇒ |
---|
235 | match l2 with |
---|
236 | [ None ⇒ |t1| = replace_last l1' |t2| ∧ ends_with l1' t1 |
---|
237 | | Some l2' ⇒ |
---|
238 | if |t2| = [] then |t1| = [l1'] ∧ l2' = l1' |
---|
239 | else |t1| = l2' :: replace_last l1' |t2| ∧ ends_with l1' t1 |
---|
240 | ] |
---|
241 | ] |
---|