Changeset 3388 for LTS/Simulation.ma
 Timestamp:
 Aug 27, 2013, 6:11:57 PM (6 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

LTS/Simulation.ma
r3387 r3388 10 10 ∀s1,s1'. as_syntactical_succ S s1 s → Crel … rel s1 s1' → as_syntactical_succ S s1' s'. 11 11 12 record simulation_conditions (S : abstract_status) (rel : relations S) : Type[0]≝12 record simulation_conditions (S : abstract_status) (rel : relations S) : Prop ≝ 13 13 { simulate_tau: 14 14 ∀s1,s2,s1' : S. … … 16 16 Srel … rel s1 s2 → 17 17 ∃s2'. ∃t: raw_trace S s2 s2'. 18 Srel … rel s 2s2' ∧ silent_trace … t18 Srel … rel s1' s2' ∧ silent_trace … t 19 19 ; simulate_label: 20 20 ∀s1,s2,l,s1'. 21 21 as_execute S (cost_act (Some ? l)) s1 s1' → 22 as_classify … s1' ≠ cl_io → 22 23 Srel … rel s1 s2 → 23 24 ∃s2',s2'',s2'''. 24 25 ∃t1: raw_trace S s2 s2'. 25 as_execute … (cost_act (Some ? l)) s2' s2'' ∧ 26 as_execute … (cost_act (Some ? l)) s2' s2'' ∧ as_classify … s2'' ≠ cl_io ∧ 26 27 ∃t3: raw_trace S s2'' s2'''. 27 28 Srel … rel s1' s2''' ∧ silent_trace … t1 ∧ silent_trace … t3 … … 30 31 is_call_post_label … s1 → 31 32 as_execute … (call_act f l) s1 s1' → 33 as_classify … s1' ≠ cl_io → 32 34 Srel … rel s1 s2 → 33 35 ∃s2',s2'',s2'''. 34 36 ∃t1: raw_trace S s2 s2'. 37 as_classify … s2' ≠ cl_jump ∧ 35 38 as_execute … (call_act f l) s2' s2'' ∧ 39 bool_to_Prop(is_call_post_label … s2') ∧ 40 as_classify … s2'' ≠ cl_io ∧ 36 41 ∃t3: raw_trace S s2'' s2'''. 37 42 Srel … rel s1' s2''' ∧ silent_trace … t1 ∧ silent_trace … t3 … … 39 44 ∀s1,s2,s1' : S.∀l. 40 45 as_execute S (ret_act (Some ? l)) s1 s1' → 46 as_classify … s1' ≠ cl_io → 41 47 Srel … rel s1 s2 → 42 48 ∃s2',s2'',s2'''. 43 49 ∃t1: raw_trace S s2 s2'. 50 as_classify … s2' ≠ cl_jump ∧ 44 51 as_execute … (ret_act (Some ? l)) s2' s2'' ∧ 52 as_classify … s2'' ≠ cl_io ∧ 45 53 ∃t3: raw_trace S s2'' s2'''. 46 Srel … rel s 2s2''' ∧ silent_trace … t1 ∧ silent_trace … t354 Srel … rel s1' s2''' ∧ silent_trace … t1 ∧ silent_trace … t3 47 55 ; simulate_call_n: 48 56 ∀s1,s2,s1' : S.∀f,l. … … 89 97 90 98 99 lemma append_premeasurable_silent : ∀S : abstract_status. 100 ∀st1',st1,st2 : S.∀t : raw_trace S st1 st2.∀t' : raw_trace S st1' st1. 101 pre_measurable_trace … t → pre_silent_trace … t' → as_classify … st1' ≠ cl_io → 102 pre_measurable_trace … (t' @ t). 103 #S #st1' #st1 #st2 #t #t' lapply t t elim t' 104 [ #st #t #Hpre #_ #_ whd in ⊢ (????%); assumption] 105 #s1 #s2 #s3 #l #prf #tl #IH #t #Hpre #H inversion H in ⊢ ?; 106 [ #s #EQ1 #EQ2 destruct #EQ destruct] 107 #s1' #s2' #s3' #prf' #tl' #Hclass #silent_tl' #_ #EQ1 #EQ2 #EQ3 108 destruct #_ #Hs1' whd in ⊢ (????%); %2 109 [ assumption 110  %{(None ?)} % 111  @IH try assumption >Hclass % #EQ destruct 112 ] 113 qed. 114 115 definition is_trace_non_empty : ∀S : abstract_status.∀st1,st2. 116 raw_trace S st1 st2 → bool ≝ 117 λS,st1,st2,t.match t with [ t_base _ ⇒ false  _ ⇒ true ]. 118 119 lemma append_well_formed_silent : ∀S : abstract_status. 120 ∀st1',st1,st2 : S.∀t : raw_trace S st1 st2.∀t' : raw_trace S st1' st1. 121 well_formed_trace … t → pre_silent_trace … t' → 122 (is_trace_non_empty … t' → as_classify … st1' = cl_other) → 123 well_formed_trace … (t' @ t). 124 #S #st1' #st1 #st2 #t #t' lapply t t elim t' 125 [ #st #t #H #_ #_ assumption ] 126 #s1' #s2' #s3' #l #prf #tl #IH #t #well_formed_t #H 127 inversion H in ⊢ ?; 128 [ #st #EQ1 #EQ2 #EQ3 destruct] 129 #st1'' #st2' #st3' #prf' #tl' #Hclass #silent_tl #_ 130 #EQ1 destruct #EQ #EQ1 destruct #_ #Hclass1 %2 131 [2: >(Hclass1 I) % #EQ destruct] 132 @IH try assumption #_ assumption 133 qed. 134 135 lemma get_cost_label_invariant_for_append_silent_trace_l :∀S : abstract_status. 136 ∀st1,st2,st3 : S.∀t1 : raw_trace S st1 st2.∀t2 : raw_trace S st2 st3. 137 pre_silent_trace … t1 → 138 get_costlabels_of_trace … (t1 @ t2) = get_costlabels_of_trace … t2. 139 #S #st1 #st2 #st3 #t1 elim t1 140 [#st #t2 #_ %] #st1' #st2' #st3' #l' #prf #tl #IH #t2 #H 141 inversion H in ⊢ ?; [ #st #EQ1 #EQ2 #EQ3 destruct] 142 #st1'' #st2'' #st3'' #prf'' #tl'' #Hclass #Htl'' #_ #EQ1 #EQ2 #EQ3 destruct 143 #_ whd in ⊢ (??%?); >IH [%] assumption 144 qed. 145 146 (* 147 lemma raw_trace_ind_r : ∀S : abstract_status. 148 ∀P : (∀st1,st2.raw_trace S st1 st2 → Prop). 149 (∀st : S.P … (t_base … st)) → 150 (∀st1,st2,st3,l. 151 ∀prf : as_execute S l st2 st3. 152 ∀tl : raw_trace S st1 st2. P … tl → P … (tl @ (t_ind … prf … (t_base … st3)))) → 153 ∀st1,st2 : S.∀t : raw_trace S st1 st2.P … t. 154 #S #P #base #ind #st1 #st2 #t elim t [ assumption] 155 #st1 #st2 #st3 #l #prf #raw #IH 156 *) 157 158 91 159 theorem simulates_pre_mesurable: 92 160 ∀S : abstract_status.∀rel : relations S. 93 161 ∀s1,s1' : S. ∀t1: raw_trace S s1 s1'. 162 simulation_conditions S rel → 94 163 pre_measurable_trace … t1 → 95 well_formed_trace … t1 → ∀s2.Srel … rel s1 s2 → 96 ∃s2'. ∃t2: raw_trace … s1' s2'. 164 well_formed_trace … t1 → ∀s2 : S. 165 as_classify … s2 ≠ cl_io → Srel … rel s1 s2 → 166 ∃s2'. ∃t2: raw_trace … s2 s2'. 97 167 pre_measurable_trace … t2 ∧ 98 168 well_formed_trace … t2 ∧ 99 169 get_costlabels_of_trace … t1 = get_costlabels_of_trace … t2 ∧ 100 Srel … rel s2 s2'. 101 cases daemon (*TODO*) 102 qed. 170 Srel … rel s1' s2'. 171 #S #rel #s1 #s1' #t1 #good #pre_measurable elim pre_measurable 172 [ #st #H1 #well_formed #s2 #H2 #REL %{s2} %{(t_base …)} 173 /8 by refl, pm_empty, wf_empty, conj/ 174  #st1 #st2 #st3 #l #execute #tl #ClASS ** [#c] #EQ destruct 175 #pre_measurable_tl #IH #well_formed #s2 #classify_s2 #REL 176 [ cases(simulate_tau … good … execute … REL) #s2'' * #t_s2'' * #RELst2s2'' 177 * #silent_ts2'' #Hclass_s2 cases(IH … RELst2s2'') 178 [2: cases(well_formed_trace_inv … well_formed) 179 [2: * #st2''' * #l''' * #prf''' * #tl''' ** #H #_ 180 #EQ destruct(EQ) assumption 181  * 182 [2: * #st2''' * #l''' * #prf''' * #tl''' ** #H #_ #EQ destruct 183 assumption 184  * #EQ1 #EQ2 destruct 185 ] 186 ] 187 3: @(silent_io … silent_ts2'') assumption 188 ] 189 #s3 * #ts3 *** #pre_meas_ts3 #well_formed_ts3 #EQcost #RELst3s3 190 %{s3} %{(t_s2'' @ ts3)} % [2: assumption] % 191 [ % 192 [ @append_premeasurable_silent assumption 193  @append_well_formed_silent assumption 194 ] 195  whd in ⊢ (??%?); >EQcost >get_cost_label_invariant_for_append_silent_trace_l 196 [%  assumption] 197 ] 198  cases(simulate_label … good … execute … REL) 199 [2: cases pre_measurable_tl 200 [ #st #H @H 201  #st1 #st2 #st3 #l #prf #tl #H #_ #_ @H 202  #st1 #st2 #st3 #l #H #_ #tl #_ #_ @H 203  #st1 #st2 #st3 #l #_ #tl #H #_ #_ #_ @H 204  #st1 #st2 #st3 #st4 #st5 #l1 #l2 #_ #t1 #t2 #_ #H #_ #_ #_ #_ #_ #_ #_ @H 205 ] 206 ] 207 #s2'' * #s2''' * #s2'''' * #t_s2'' ** #exe_s2''' #CLASS' * #t_s2'''' ** #RELst2_s2'''' 208 * #sil_ts2'' #Hclass_s2 * #sil_t_s2'''' #Hclass_s2''' cases(IH … RELst2_s2'''') 209 [2: cases(well_formed_trace_inv … well_formed) 210 [2: * #st2''' * #l''' * #prf''' * #tl''' ** #H #_ 211 #EQ destruct(EQ) assumption 212  * 213 [2: * #st2''' * #l''' * #prf''' * #tl''' ** #H #_ #EQ destruct 214 assumption 215  * #EQ1 #EQ2 destruct 216 ] 217 ] 218 3: @(silent_io … sil_t_s2'''') assumption 219 ] 220 #s3 * #t_s3 *** #pre_s3 #well_s3 #EQcost #RElst3s3 %{s3} 221 %{(t_s2'' @ (t_ind … exe_s2''' …))} [ @(t_s2'''' @ t_s3) ] % [2: assumption] 222 % 223 [ % 224 [ @append_premeasurable_silent try assumption %2 225 [ @(silent_io … t_s2'') assumption 226  %{(Some ? c)} % 227 ] 228 @append_premeasurable_silent assumption 229  @append_well_formed_silent try assumption inversion(as_classify … s2'') 230 #Hclass 231 [ %3 [2: %{c} %] 232 *: %2 [2,4: >Hclass % #EQ destruct] 233 ] 234 @append_well_formed_silent assumption 235 ] 236  whd in ⊢ (??%?); >EQcost >get_cost_label_invariant_for_append_silent_trace_l 237 [2: assumption] whd in ⊢ (???%); 238 >get_cost_label_invariant_for_append_silent_trace_l 239 [ %  assumption] 240 ] 241 ] 242  #s2 #s2' #s2'' #l #class_s2 #exe_s2_s2' #tl whd in ⊢ (% → ?); * #ret_lab #EQ destruct(EQ) 243 #pre_meas_tl #IH #H inversion H 244 [ #s3 #EQ1 #EQ2 destruct #ABS destruct(ABS) ] 245 #st1 #st2 #st3 #l #exe_st1_st2 #tl' #wf_tl' 246 [ #class_no_jump  whd in ⊢ (% → ?); * #nf #EQ destruct(EQ) ] 247 #_ #EQ1 #EQ2 #EQ3 destruct #_ H #s2 #class_s2 #RELst1s2 248 cases(simulate_ret_l … good … exe_st1_st2 … RELst1s2) 249 [2: inversion pre_meas_tl 250 try #x1 try #x2 try #x3 try #x4 try #x5 try #x6 251 try #x11 try #x12 try #x13 try #x14 try #x15 try #x16 252 try #x17 try #x18 try #x19 try #x20 try #x21 try #x22 253 try #x37 try #x38 try #x39 try #x30 try #x31 try #x32 try #x33 254 destruct assumption ] 255 #s2' * #s2'' * #s2''' * #t1 *** #j_s2' #exe_s2'' #class_s2'' * #t2 ** #rel_s2_s2''' 256 #sil_t1 #sil_t2 257 cases(IH … wf_tl' … rel_s2_s2''') 258 [2: @(silent_io … (proj1 … sil_t2)) assumption] 259 #s2_fin * #t_fin *** #pre_t_fin #wf_t_fin #EQcost #REL 260 %{s2_fin} %{(t1 @ (t_ind … exe_s2'' … t2) @ t_fin)} % [2: assumption] 261 % [2: whd in ⊢ (??%?); 262 >(get_cost_label_invariant_for_append_silent_trace_l … (proj1 … sil_t1)) 263 whd in ⊢ (???%); 264 >(get_cost_label_invariant_for_append_silent_trace_l … (proj1 … sil_t2)) 265 @eq_f assumption ] 266 % 267 [ @append_premeasurable_silent try assumption [2: @(proj1 … sil_t1)] 268 %3 269 [ @(silent_io … (proj1 … sil_t1)) assumption 270  whd %{ret_lab} % 271  @append_premeasurable_silent try assumption @(proj1 … sil_t2) 272 ] 273  @append_well_formed_silent 274 [ %2 try assumption @append_well_formed_silent try assumption 275 [ @(proj1 … sil_t2) 276  @(proj2 … sil_t2) 277 ] 278  @(proj1 … sil_t1) 279  @(proj2 … sil_t1) 280 ] 281 ] 282  #s2 #s2' #s2'' #l #exe_s2_s2' #tl #class_s2 whd in ⊢ (% → ?); * #f * #lab #EQ destruct 283 #post #pre_tl #IH #H inversion H [ #s3 #EQ1 #EQ2 destruct #ABS destruct(ABS) ] 284 #st1 #st2 #st3 #l #exe_st1_st2 #tl' #wf_tl' 285 [#class_no_jump  whd in ⊢ (% → ?); * #nf #EQ destruct(EQ) ] 286 #_ #EQ1 #EQ2 #EQ3 destruct #_ H #s2 #io_s2 #REL_st1_s2 287 cases(simulate_call_pl … good … post … exe_st1_st2 … REL_st1_s2) 288 [2: inversion pre_tl 289 try #x1 try #x2 try #x3 try #x4 try #x5 try #x6 290 try #x11 try #x12 try #x13 try #x14 try #x15 try #x16 291 try #x17 try #x18 try #x19 try #x20 try #x21 try #x22 292 try #x37 try #x38 try #x39 try #x30 try #x31 try #x32 try #x33 293 destruct assumption ] 294 #s2' * #s2'' * #s2''' * #t1 **** #j_s2' #exe_s2'' #post' #io_s2'' * #t2 ** #REL #sil_t1 #sil_t2 295 cases(IH … wf_tl' … REL) 296 [2: @(silent_io … (proj1 … sil_t2)) assumption ] 297 #s2_fin * #t_fin *** #pre_t_fin #wf_t_fin #EQcost #REL1 %{s2_fin} 298 %{(t1 @ (t_ind … exe_s2'' … t2) @ t_fin)} % [2: assumption] % 299 [2: whd in ⊢ (??%?); 300 >(get_cost_label_invariant_for_append_silent_trace_l … (proj1 … sil_t1)) 301 whd in ⊢ (???%); 302 >(get_cost_label_invariant_for_append_silent_trace_l … (proj1 … sil_t2)) 303 @eq_f assumption ] 304 % 305 [ @append_premeasurable_silent try assumption [2: @(proj1 … sil_t1)] 306 %4 try assumption 307 [ @(silent_io … (proj1 … sil_t1)) assumption 308  whd %{f} %{lab} % 309  @append_premeasurable_silent try assumption @(proj1 … sil_t2) 310 ] 311  @append_well_formed_silent 312 [ %2 try assumption @append_well_formed_silent try assumption 313 [ @(proj1 … sil_t2) 314  @(proj2 … sil_t2) 315 ] 316  @(proj1 … sil_t1) 317  @(proj2 … sil_t1) 318 ] 319 ] 320  cases daemon (*TODO*) 321 ] 322 qed. 323 324 325 326 #st3 #l #class_st1 #exe #tl * #x #EQ destruct(EQ) #pre_tl #IH 327 #well_formed #s2 #class_s2 #REL cases(simulate_ret_l … good … exe … REL) 328 #s2'' * #s2''' * #s2'''' * #t1 * #exe' * #t2 ** #Rs2s2'''' #t1_sil #t2_sil 329 xxxxxxxxx 330 331 332 #st4 #st5 #l1 #l2 * #x #EQ whd in ⊢ (% → ?); 333 @append_premeasurable_silent 334 335 xxxxxxxxxxxxxx 336 ] 337 *: cases daemon (*TODO*) 338 ] 339 qed.*) 103 340 104 341 (* IDEA: aggiungere stati di I/O e cambiare la semantica del linguaggio
Note: See TracChangeset
for help on using the changeset viewer.