source: LTS/Simulation.ma @ 3391

Last change on this file since 3391 was 3391, checked in by piccolo, 6 years ago

Definition of well formed trace is in the operational semantics

File size: 19.5 KB
Line 
1include "Common.ma".
2include "Traces.ma".
3
4record relations (S : abstract_status) : Type[0] ≝
5 { Srel: S → S → Prop
6 ; Crel: S → S → Prop
7 }.
8
9definition 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
12record simulation_conditions (S : abstract_status) (rel : relations S) : Prop ≝
13 { simulate_tau:
14     ∀s1,s2,s1' : S.
15      as_execute … (cost_act (None ?))  s1 s1'→
16      Srel … rel s1 s2 → as_classify … s1 ≠ cl_io → as_classify … s1' ≠ cl_io →
17      ∃s2'. ∃t: raw_trace S s2 s2'.
18        Srel … rel s1' s2' ∧ silent_trace … t
19 ; simulate_label:
20     ∀s1,s2,l,s1'.
21      as_execute S (cost_act (Some ? l)) s1 s1' →
22      as_classify … s1 ≠ cl_io → as_classify … s1' ≠ cl_io →
23      Srel … rel s1 s2 →
24      ∃s2',s2'',s2'''.
25       ∃t1: raw_trace S s2 s2'.
26       as_execute … (cost_act (Some ? l)) s2' s2'' ∧
27       ∃t3: raw_trace S s2'' s2'''.
28        Srel … rel  s1' s2''' ∧ silent_trace … t1 ∧ silent_trace … t3
29 ; simulate_call_pl:
30     ∀s1,s2,s1' : S.∀f,l.
31      is_call_post_label … s1 →
32      as_execute … (call_act f l) s1 s1' →
33      as_classify … s1 ≠ cl_io → as_classify … s1' ≠ cl_io →
34      Srel … rel s1 s2 →
35      ∃s2',s2'',s2'''.
36       ∃t1: raw_trace S s2 s2'.
37       as_execute … (call_act f l) s2' s2'' ∧
38       bool_to_Prop(is_call_post_label … s2') ∧
39       ∃t3: raw_trace S s2'' s2'''.
40        Srel … rel s1' s2''' ∧ silent_trace … t1 ∧ silent_trace … t3
41 ; simulate_ret_l:
42     ∀s1,s2,s1' : S.∀l.
43      as_execute S (ret_act (Some ? l)) s1 s1' →
44      as_classify … s1 ≠ cl_io → as_classify … s1' ≠ cl_io →
45      Srel  … rel s1 s2 →
46      ∃s2',s2'',s2'''.
47       ∃t1: raw_trace S s2 s2'.
48       as_execute … (ret_act (Some ? l)) s2' s2'' ∧
49       ∃t3: raw_trace S s2'' s2'''.
50        Srel … rel s1' s2''' ∧ silent_trace … t1 ∧ silent_trace … t3
51 ; simulate_call_n:
52     ∀s1,s2,s1' : S.∀f,l.
53      as_execute … (call_act f l) s1 s1' →
54      ¬ is_call_post_label … s1 →
55      as_classify … s1 ≠ cl_io → as_classify … s1' ≠ cl_io →
56      Srel … rel s1 s2 →
57      ∃s2',s2'',s2'''.
58       ∃t1: raw_trace S s2 s2'.
59       bool_to_Prop (¬ is_call_post_label … s2') ∧
60       as_execute … (call_act f l) s2' s2'' ∧
61       ∃t3: raw_trace S s2'' s2'''.
62        Srel … rel s1' s2''' ∧ silent_trace … t1 ∧ silent_trace … t3
63        ∧ Crel … rel s1 s2'
64 ; simulate_ret_n:
65     ∀s1,s2,s1' : S.
66      as_execute … (ret_act (None ?)) s1 s1' →
67      as_classify … s1 ≠ cl_io → as_classify … s1' ≠ cl_io →
68      Srel … rel s1 s2 →
69      ∃s2',s2'',s2'''.
70       ∃t1: raw_trace S s2 s2'.
71       as_execute … (ret_act (None ?)) s2' s2''  ∧
72       ∃t3: raw_trace S s2'' s2'''.
73        Srel … rel s1' s2''' ∧ silent_trace … t1 ∧ silent_trace … t3
74        ∧ Rrel … rel s1' s2''
75 }.
76
77let rec get_costlabels_of_trace (S : abstract_status) (st1 : S) (st2 : S)
78(t : raw_trace S st1 st2) on t : list CostLabel ≝
79match t with
80[ t_base st ⇒ [ ]
81| t_ind st1' st2' st3' l prf t' ⇒
82    let tl ≝ get_costlabels_of_trace … t' in
83    match l with
84    [ call_act f c ⇒ c :: tl
85    | ret_act x ⇒ match x with
86                  [ Some c ⇒ ret_act_label_to_cost_label c :: tl
87                  | None ⇒ tl
88                  ]
89    | cost_act x ⇒ match x with
90                  [ Some c ⇒ a_non_functional_label c :: tl
91                  | None ⇒ tl
92                  ]
93    | init_act ⇒ tl
94    ]
95].
96
97
98lemma append_premeasurable_silent : ∀S : abstract_status.
99∀st1',st1,st2 : S.∀t : raw_trace S st1 st2.∀t' : raw_trace S st1' st1.
100pre_measurable_trace … t → silent_trace … t' → 
101pre_measurable_trace … (t' @ t).
102#S #st1' #st1 #st2 #t #t' lapply t -t elim t'
103[ #st #t #Hpre #_ whd in ⊢ (????%); assumption]
104#s1 #s2 #s3 #l #prf #tl #IH #t #Hpre #H inversion H in ⊢ ?;
105[ #s #H1 #EQ1 #EQ2 destruct #EQ destruct]
106#s1' #s2' #s3' #prf' #tl' #Hclass #silent_tl' #_ #EQ1 #EQ2 #EQ3
107destruct #_ whd in ⊢ (????%); %2
108[ assumption
109| %{(None ?)} %
110| @IH try assumption
111]
112qed.
113
114lemma silent_is_premeasurable : ∀S : abstract_status.
115∀st1,st2 : S. ∀t : raw_trace S st1 st2.silent_trace … t
116→ pre_measurable_trace … t.
117#S #st1 #st2 #t elim t
118[ #st #H inversion H in ⊢ ?; [ #st' #Hst #EQ1 #EQ2 #EQ3 destruct #_ %1 @Hst ]
119#st' #st'' #st''' #prf #tl #Hst'' #pre_tl #_ #EQ1 #EQ2 #EQ3 destruct ]
120-t -st1 -st2 #st1 #st2 #st3 #l #prf #tl #IH #H inversion H in ⊢ ?;
121[ #st #H2 #EQ1 #EQ2 #EQ3 destruct] #st1' #st2' #st3' #prf' #tl' #Hst2' #pre_tl'
122#_ #EQ1 #EQ2 #EQ3 destruct #_ %2 [ assumption | whd %{(None ?)} % ]
123@IH assumption
124qed.
125
126lemma append_tind_commute : ∀S : abstract_status.∀st1,st2,st3,st4 : S.∀l.
127    ∀prf : as_execute … l st1 st2. ∀t1 : raw_trace S st2 st3.
128    ∀t2 : raw_trace S st3 st4.t_ind … prf (t1 @ t2) = (t_ind … prf t1) @ t2.
129#S #st1 #st2 #st3 #st4 #l #prf #t1 #t2 % qed.   
130
131lemma append_silent_premeasurable : ∀S : abstract_status.
132∀st1',st1,st2 : S.∀t : raw_trace S st1 st2.∀t' : raw_trace S st1' st1.
133pre_measurable_trace … t' → silent_trace … t →
134pre_measurable_trace … (t' @ t).
135#S #st1' #st1 #st2 #t #t' #Ht' lapply t -t elim Ht'
136[ normalize #st #Hst #r #H1 @silent_is_premeasurable assumption
137|2,3,4: #s1 #s2 #s3 #l #prf #tl #Hs1 * #x [|| * #l' ] #EQ destruct
138  [|| #Hs1_post ] #pre_tl #IH #r #pre_sil_r [ %2 | %3 | %4 ]
139  try ( %{x} %) try @IH try assumption % ]
140#s1 #s2 #s3 #s4 #s5 #l1 #l2 #pr1 #t1 #t2 #prf2 #Hs1 #Hs3 * #f * #l1'
141#EQ destruct #Hpost_s1 #pre_t1 #pre_t2 #Hs1_s4 #EQ destruct #IH1 #IH2
142#r #pre_r normalize
143>append_tind_commute >append_tind_commute >append_associative
144<append_tind_commute in ⊢ (????(??????%)); %5
145try assumption [1,3: whd [ %{f} %{l1'} ] % ] @IH2 assumption
146qed.
147
148(*
149lemma append_well_formed_silent : ∀S : abstract_status.
150∀st1',st1,st2 : S.∀t : raw_trace S st1 st2.∀t' : raw_trace S st1' st1.
151well_formed_trace … t → pre_silent_trace … t' →
152(is_trace_non_empty … t' → as_classify … st) →
153well_formed_trace … (t' @ t).
154#S #st1' #st1 #st2 #t #t' lapply t -t elim t'
155[ #st #t #H #_ #_ assumption ]
156#s1' #s2' #s3' #l #prf #tl #IH #t #well_formed_t #H
157inversion H in ⊢ ?;
158[ #st #EQ1 #EQ2 #EQ3 destruct]
159#st1'' #st2' #st3' #prf' #tl' #Hclass #silent_tl #_
160#EQ1 destruct #EQ #EQ1 destruct #_ #Hclass1 %2
161[2: >(Hclass1 I) % #EQ destruct]
162@IH try assumption #_ assumption
163qed.*)
164
165(*
166lemma well_formed_append : ∀S : abstract_status.
167∀st1,st2,st3 : S. ∀t1 : raw_trace S st1 st2.∀t2 : raw_trace S st2 st3.
168well_formed_trace … (t1 @ t2) → well_formed_trace … t1 ∧ well_formed_trace … t2.
169#S #st1 #st2 #st3 #t1 #t2 #H %
170[ lapply H -H lapply t2 -t2 elim t1 [ //] #st1' #st2' #st3' #l #exe #tl #IH #r
171#H inversion H in ⊢ ?; [ #st #EQ1 #EQ2 #EQ3 normalize in EQ3; destruct ]
172#st1'' #st2'' #st3'' #l' #prf' #tl' #wf_tl' [#Hst1'' | * #x #EQ destruct] #_
173#EQ1 #EQ2 normalize in ⊢ (% → ?); #EQ3 destruct #_
174[ %2 [ @IH assumption ] assumption | %3 [ @IH assumption ] %{x} % ]
175]
176lapply H lapply t2 -t2 elim t1 [ #st #r normalize //]
177#s1 #s2 #s3 #l #prf #tl #IH #r #H inversion H in ⊢ ?;
178[ #st #EQ1 #EQ2 normalize #EQ3 destruct ]
179#s1' #s2' #s3' #l' #prf' #tl' #wf_tl' #Hs1' #_ normalize #EQ1 #EQ2 #EQ3 destruct
180#_ @IH assumption
181qed.
182
183
184lemma append_well_formed : ∀S : abstract_status.
185∀st1,st2,st3 : S.∀t1 : raw_trace S st1 st2.∀t2 : raw_trace S st2 st3.
186well_formed_trace … t1 → well_formed_trace … t2 → well_formed_trace … (t1 @ t2).
187#S #st1 #st2 #st3 #t1 #t2 #H lapply t2 -t2 elim H
188[ #st #r #H1 @H1 ]
189#s1 #s2 #s3 #l #prf #tl #wf_tl #Hs1 #IH #r #wf_r normalize [ %2 | %3]
190try @IH assumption
191qed.
192(*
193lemma silent_is_well_formed : ∀S : abstract_status.
194∀st1,st2 : S.∀t : raw_trace … st1 st2.silent_trace … t → well_formed_trace … t.
195#S #st1 #st2 #t elim t [ #st #_ %]
196#s1 #s2 #s3 #l #prf #tl #IH * #H inversion H [ #st #EQ1 #EQ2 #EQ3 destruct]
197#s1' #s2' #s3' #prf' #tl' #Hs2' #tl' #_ #EQ1 #EQ2 #EQ3 destruct #_ #H1 %2
198[ @IH % [2: #_ ] assumption | >(H1 I) % #EQ destruct]
199qed.
200*)
201*)
202lemma get_cost_label_invariant_for_append_silent_trace_l :∀S : abstract_status.
203∀st1,st2,st3 : S.∀t1 : raw_trace S st1 st2.∀t2 : raw_trace S st2 st3.
204silent_trace … t1 →
205get_costlabels_of_trace … (t1 @ t2) = get_costlabels_of_trace … t2.
206#S #st1 #st2 #st3 #t1 elim t1
207[#st #t2 #_ %] #st1' #st2' #st3' #l' #prf #tl #IH #t2 #H
208inversion H in ⊢ ?; [ #st #H1 #EQ1 #EQ2 #EQ3 destruct]
209#st1'' #st2'' #st3'' #prf'' #tl'' #Hclass #Htl'' #_ #EQ1 #EQ2 #EQ3 destruct
210#_ whd in ⊢ (??%?); >IH [%] assumption
211qed.
212
213lemma get_cost_label_append : ∀S : abstract_status.∀st1,st2,st3 : S.
214∀t1 : raw_trace … st1 st2. ∀t2 : raw_trace … st2 st3.
215get_costlabels_of_trace … (t1 @ t2) =
216 append … (get_costlabels_of_trace … t1) (get_costlabels_of_trace … t2).
217#S #st1 #st2 #st3 #t1 elim t1 [ #st #t2 % ] #st1' #st2' #st3' *
218[#f * #l | * [| * #l] | *  [| #l] |] #prf #tl #IH #t2 normalize try @eq_f @IH
219qed.
220 
221(*
222lemma raw_trace_ind_r : ∀S : abstract_status.
223∀P : (∀st1,st2.raw_trace S st1 st2 → Prop).
224(∀st : S.P … (t_base … st)) →
225(∀st1,st2,st3,l.
226 ∀prf : as_execute S l st2 st3.
227 ∀tl : raw_trace S st1 st2. P … tl → P … (tl @ (t_ind … prf … (t_base … st3)))) →
228∀st1,st2 : S.∀t : raw_trace S st1 st2.P … t.
229#S #P #base #ind #st1 #st2 #t elim t [ assumption]
230#st1 #st2 #st3 #l #prf #raw #IH
231*)
232
233lemma head_of_premeasurable_is_not_io : ∀S : abstract_status.
234∀st1,st2 : S. ∀t : raw_trace … st1 st2.pre_measurable_trace … t →
235as_classify … st1 ≠ cl_io.
236#S #st1 #st2 #t #H inversion H //
237qed.
238
239
240theorem simulates_pre_mesurable:
241 ∀S : abstract_status.∀rel : relations S.
242 ∀s1,s1' : S. ∀t1: raw_trace S s1 s1'.
243  simulation_conditions S rel →
244  pre_measurable_trace … t1 →
245  ∀s2 : S.
246 as_classify … s2 ≠ cl_io →   Srel … rel s1 s2 →
247  ∃s2'. ∃t2: raw_trace … s2 s2'.
248    pre_measurable_trace … t2 ∧
249    get_costlabels_of_trace … t1 = get_costlabels_of_trace … t2 ∧
250    Srel … rel s1' s2'.
251#S #rel #s1 #s1' #t1 #good #pre_measurable elim pre_measurable
252[ #st #H1 #s2 #REL #Hs2 %{s2} %{(t_base …)}
253  /8 by refl, silent_empty, conj, silent_is_premeasurable/
254| #st1 #st2 #st3 #l #execute #tl #ClASS ** [|#c] #EQ destruct
255  #pre_measurable_tl #IH #s2 #classify_s2 #REL
256  [ cases(simulate_tau … good … execute … REL) /2/ #s2'' * #t_s2'' * #RELst2s2''
257    #silent_ts2'' cases(IH … RELst2s2'') /2 by silent_io/
258    #s3 * #ts3 ** #pre_meas_ts3 #EQcost #RELst3s3
259    %{s3} %{(t_s2'' @ ts3)} % [2: assumption] % /2 by append_premeasurable_silent/
260    whd in ⊢ (??%?); /2/
261  | cases(simulate_label … good … execute … REL)
262    [2,3: /2/]
263    #s2'' * #s2''' * #s2'''' * #t_s2'' * #exe_s2''' * #t_s2'''' ** #RELst2_s2''''
264    #sil_ts2'' #sil_t_s2'''' cases(IH … RELst2_s2'''') /2 by silent_io/
265    #s3 * #t_s3 ** #pre_s3 #EQcost #RElst3s3 %{s3}
266    %{(t_s2'' @ (t_ind … exe_s2''' …))}  [ @(t_s2'''' @ t_s3) ] % [2: assumption]
267    %
268    [ /4 by pm_cons_cost_act, silent_io, ex_intro, append_premeasurable_silent/
269    | whd in ⊢ (??%?); >EQcost >get_cost_label_invariant_for_append_silent_trace_l
270      [2: assumption] whd in ⊢ (???%);
271      >get_cost_label_invariant_for_append_silent_trace_l //
272    ]
273  ]
274| #s2 #s2' #s2'' #l #class_s2 #exe_s2_s2' #tl whd in ⊢ (% → ?); * #ret_lab #EQ destruct(EQ)
275  #pre_meas_tl #IH #s2 #class_s2 #RELst1s2
276  cases(simulate_ret_l … good … exe_s2_s2' … RELst1s2) [2,3: /2/ ]
277  #st1 * #st2 * #st3 * #t1 * #exe_s2'' * #t2 ** #rel_s2_s2'''
278  #sil_t1 #sil_t2 cases(IH … rel_s2_s2''')
279  [2: @(silent_io … sil_t2) assumption]
280  #s2_fin * #t_fin ** #pre_t_fin #EQcost #REL
281  %{s2_fin} %{(t1 @ (t_ind … exe_s2'' … t2) @ t_fin)} % [2: assumption]
282  % [2: whd in ⊢ (??%?);
283        >(get_cost_label_invariant_for_append_silent_trace_l … sil_t1)
284        whd in ⊢ (???%);
285        >(get_cost_label_invariant_for_append_silent_trace_l … sil_t2)
286        @eq_f assumption ]
287  /4 by pm_cons_lab_ret, silent_io, ex_intro, append_premeasurable_silent/
288| #s1 #s2 #s3 #l #exe_s1_s2 #tl #class_s1 * #f * #lab #EQ destruct
289  #post #pre_tl #IH #s2' #io_s2' #REL_s1_s2'
290   cases(simulate_call_pl … good … post … exe_s1_s2 … REL_s1_s2')
291   [2,3: /2 by head_of_premeasurable_is_not_io/ ]
292   #s' * #s2'' * #s2''' * #t1 ** #exe_s2'' #post' * #t2 ** #REL #sil_t1 #sil_t2
293   cases(IH  … REL)
294   [2: /2 by silent_io/ ]
295   #s2_fin * #t_fin ** #pre_t_fin #EQcost #REL1 %{s2_fin}
296   %{(t1 @ (t_ind … exe_s2'' … t2) @ t_fin)} % [2: assumption] %
297   [2: whd in ⊢ (??%?);
298        >(get_cost_label_invariant_for_append_silent_trace_l … sil_t1)
299        whd in ⊢ (???%);
300        >(get_cost_label_invariant_for_append_silent_trace_l … sil_t2)
301        @eq_f assumption ]
302   @append_premeasurable_silent try assumption
303     %4 try assumption
304     [ /2 by silent_io/
305     | whd %{f} %{lab} %
306     | /2 by append_premeasurable_silent/
307     ]
308| #st1 #st2 #st3 #st4 #st5 #l1 #l2 #exe_12 #t1 #t2 #exe_34 #class_1 #class_3 *
309  #f * #l #EQ destruct #Hst1 #pre_t1 #pre_t2 #succ_14 whd in ⊢ (% → ?); #EQ destruct
310  #IH1 #IH2 #st1' #Hst1' #REL cases(simulate_call_n … good … exe_12 … Hst1 … REL) [2,3: /2/ ]
311  #st1'' * #st1''' * #st2' * #tr1 ** #nps_st1'' #exe_12' * #tr2 *** #REL1 #sil_tr1
312  #sil_tr2 #call_rel cases(IH1 … REL1)
313  [2: /2 by silent_io/ ]
314  #st3' * #tr3 ** #pre_tr3 #EQcost_tr3 #REL2
315  cases(simulate_ret_n … good … exe_34 … REL2) [2,3: /2 by head_of_premeasurable_is_not_io/ ]
316  #st3'' * #st4' * #st4'' *
317  #tr4 * #exe_34' * #tr5 *** #REL3 #sil_tr4 #sil_tr5 #RET_REL cases(IH2 … REL3) [2: /2 by silent_io/ ]
318  #st5' * #tr6 ** #pre_tr6 #EQcost_tr6 #REL4 %{st5'}
319  %{(tr1 @ (t_ind … exe_12' …  ((tr2 @ tr3 @ tr4) @ (t_ind … exe_34' … (tr5 @tr6)))))}
320  % [2: assumption] %
321  [ @append_premeasurable_silent try assumption %5
322       [1,2: /2 by silent_io/
323       | whd %{f} %{l} %
324       | assumption
325       | @append_premeasurable_silent try assumption
326         @append_silent_premeasurable assumption
327       | @append_premeasurable_silent try assumption
328       | @(RET_REL … call_rel) assumption
329       | %
330       ]
331  | >get_cost_label_invariant_for_append_silent_trace_l [2: // ]
332    whd in ⊢ (??%%); @eq_f >append_associative
333    >get_cost_label_invariant_for_append_silent_trace_l in ⊢ (???%);
334    [2: // ] >append_associative
335    >get_cost_label_append in ⊢ (???%);
336    >get_cost_label_invariant_for_append_silent_trace_l in ⊢ (???%);
337    [2: //] normalize
338    >get_cost_label_invariant_for_append_silent_trace_l in ⊢ (???%);
339    [2: // ] >get_cost_label_append in ⊢ (??%?); @eq_f2
340    assumption
341  ]
342]
343qed.
344
345sxxxxx
346
347
348(* IDEA: aggiungere stati di I/O e cambiare la semantica del linguaggio
349   sorgente; aggiungere nella pre_measurable il vincolo nessuno stato e' di I/O;
350   cambiare la definizione di traccia tornando a una sola etichetta sugli archi *)
351
352(* measurable fattorizzata sotto come measurable'
353definition measurable ≝
354 λL,s1,s2.λt: raw_trace … s1 s2.
355  ∃L',s0,so. as_execute … s0 s1 L ∧
356  pre_measurable_trace … t ∧
357  well_formed_trace … t ∧
358  as_execute … s2 so L'. *)
359
360record LR_raw_trace (S : abstract_status) : Type[0] ≝
361 { L_label: ActionLabel
362 ; R_label : ActionLabel
363 ; LR_s1: S
364 ; LR_s2: S
365 ; LR_t : raw_trace S LR_s1 LR_s2
366 ; L_init_ok : bool_to_Prop(as_initial … LR_s1) → L_label = init_act
367 ; L_noinit_ok :
368      bool_to_Prop (¬ as_initial … LR_s1) →
369        ∃s0. as_execute … L_label s0 LR_s1 ∧ is_costlabelled_act L_label
370        ∧ ¬ bool_to_Prop (is_act_io_entering S L_label)
371 ; R_nonfin_ok :
372    bool_to_Prop (¬ as_final … (LR_s2)) →
373      ∃so.as_execute … R_label LR_s2 so ∧ is_costlabelled_act R_label
374          ∧ ¬ bool_to_Prop (is_act_io_exiting S R_label)
375 }.
376 
377definition measurable ≝ λS : abstract_status.λt : LR_raw_trace S.
378pre_measurable_trace … (LR_t … t) ∧ well_formed_trace … (LR_t … t).
379
380
381(*CSC: oppure fare il merge di L_raw_trace e measurable in un'unico record se
382  non c'e' nulla di interessante sulle L_raw_trace non measurabili. Per esempio
383  il teorema sotto sembra suggerire il merge *)
384
385definition unmovable_entry_label ≝
386λS : abstract_status.λl.
387match l with
388[ call_act _ _ ⇒ false
389| ret_act _ ⇒ false
390| cost_act x ⇒ match x with [Some c ⇒ is_io_exiting S c
391                            | None ⇒ false
392                            ]
393| init_act ⇒ true
394].
395 
396definition unmovable_exit_label ≝
397λS : abstract_status.λl.
398match l with
399[ call_act _ _ ⇒ false
400| ret_act _ ⇒ false
401| cost_act x ⇒ match x with [Some c ⇒ is_io_entering S c
402                            | None ⇒ false
403                            ]
404| init_act ⇒ false
405].
406
407theorem simulates_LR_raw_trace :
408∀S : abstract_status.
409∀t : LR_raw_trace S.
410∀rel : relations S.
411simulation_conditions … rel →
412measurable S t →
413∀s1' : S.as_classify … s1' ≠ cl_io → Srel … rel (LR_s1 … t) s1' →
414∃ t' : LR_raw_trace S.
415measurable S t' ∧
416if as_initial … (LR_s1 … t) ∨ unmovable_entry_label  S (L_label … t) then
417   LR_s1 … t' = s1'
418else
419   ∃pre : raw_trace … (LR_s1 … t') s1'.trace_prefix … pre (LR_t … t')
420∧ ∃s1''.Srel … rel (LR_s2 … t) s1'' ∧
421if as_final … (LR_s2 … t) ∨ unmovable_exit_label S (R_label … t) then
422   LR_s2 … t' = s1''
423else
424  ∃suff : raw_trace … s1'' (LR_s2 … t'). trace_suffix … suff (LR_t … t')
425
426get_costlabels_of_trace … (LR_t … t) = get_costlabels_of_trace … (LR_t … t').
427#S #t #rel #good * #pre_t #wf_t #s1' #Hs1' #REL
428cases(simulates_pre_mesurable … (LR_t … t) … REL)
429[2: @good |3: @pre_t |4: @wf_t |5: @Hs1' ]
430#s2 * #t2 *** #pre_t2 #wf_t2 #EQcost #REL1
431inversion(as_initial … (LR_s1 … t)) #Has_initial
432inversion(unmovable_entry_label S (L_label … t)) #Hunmov_entry
433inversion(as_final … (LR_s2 … t)) #Has_final
434inversion(unmovable_exit_label S (R_label … t)) #Hunmov_exit
435normalize nodelta
436[ %{(mk_LR_raw_trace ? ?? s1' ? t2 ???)} [2: % [2:
437
438
439
440qed.
441
442xxxx
443
444theorem simulates_L_raw_trace:
445 ∀t: L_raw_trace.
446  pre_measurable_trace … (L_t t1) →
447  well_formed_trace … (L_t t1) →
448 ∀s1'.
449   S (L_s1 t) s1' →
450   s1' -flat-→ (L_s1 t2) →
451   ∃s2',t2: L_raw_trace.
452    pre_mesurable_trace … (L_t t2) ∧
453    well_formed_trace … (L_t t2) ∧
454    |t1| = |t2| ∧
455    S (L_s2 t1) s2' ∧
456    (L_s2 t2) -flat-→ s2'.
457 (* o, nel caso in cui (L_label t1) e' unmovable_entry_label nessuna coda prefissa e
458       nel caso in cui ??? e' unmovable_exit_label, nessuna coda suffissa *)
459
460
461(*********************************************************************)
462
463(* quello che segue tentava di permettere di evitare l'emissione di label
464   associate a codice morto *)
465
466replace_last x : weak_trace → weak_trace
467   [] ⇒ [], Some x
468 | l::t ⇒
469     let 〈t',x'〉 ≝ replace_last x t in
470     match x' with
471     [ None ⇒ l::t', None
472     | Some x'' ⇒ [], Some x''
473
474theorem simulates:
475 ∀s1,s2. ∀τ1: raw_trace … s1 s2.
476  pre_measurable_trace … t1 →
477  well_formed_trace … t1.
478 ∀l1: option NonFunctionalLabel.
479 ∀s1'.
480   S s1 s1' →
481   ∃dead_labels.
482   ∃s2'. ∃t2: raw_trace … s1' s2'.
483    pre_mesurable_trace … t2 ∧
484    well_formed_trace … t2.
485   ∃l2: option NonFunctionalLabel.
486    match l1 with
487    [ None ⇒
488       match l2 with
489       [ None ⇒ |t1| = |t2|
490       | Some l2' ⇒ |t1| = l2'::|t2| ]
491    | Some l1' ⇒
492       match l2 with
493       [ None ⇒ |t1| = replace_last l1' |t2| ∧ ends_with l1' t1
494       | Some l2' ⇒
495          if |t2| = [] then |t1| = [l1'] ∧ l2' = l1'
496          else |t1| = l2' :: replace_last l1' |t2| ∧ ends_with l1' t1
497       ]
498    ]
Note: See TracBrowser for help on using the repository browser.