Changeset 3549 for LTS/Simulation.ma
 Timestamp:
 Apr 2, 2015, 3:44:19 PM (5 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

LTS/Simulation.ma
r3531 r3549 4 4 discriminator option. 5 5 6 record relations ( S1,S2 : abstract_status) : Type[0] ≝6 record relations (p : label_params) (S1,S2 : abstract_status p) : Type[0] ≝ 7 7 { Srel: S1 → S2 → Prop 8 8 ; Crel: S1 → S2 → Prop 9 9 }. 10 10 11 definition Rrel ≝ λS1,S2 : abstract_status.λrel : relations S1 S2.λs,s'. 12 ∀s1,s1'. as_syntactical_succ S1 s1 s → Crel … rel s1 s1' → as_syntactical_succ S2 s1' s'. 13 14 record simulation_conditions (S1,S2 : abstract_status) (rel : relations S1 S2) : Prop ≝ 11 definition Rrel ≝ λp.λS1,S2 : abstract_status p.λrel : relations … S1 S2.λs,s'. 12 ∀s1,s1'. as_syntactical_succ … S1 s1 s → Crel … rel s1 s1' → as_syntactical_succ … S2 s1' s'. 13 14 record simulation_conditions (p : label_params) (S1,S2 : abstract_status p) 15 (rel : relations …S1 S2) : Prop ≝ 15 16 { initial_is_initial : 16 17 ∀s1,s2.Srel … rel s1 s2 → (bool_to_Prop (as_initial … s1) → bool_to_Prop (as_initial … s2)) … … 21 22 ; simulate_tau: 22 23 ∀s1:S1.∀s2:S2.∀s1':S1. 23 as_execute … (cost_act (None ?)) s1 s1'→24 as_execute … (cost_act … (None ?)) s1 s1'→ 24 25 Srel … rel s1 s2 → as_classify … s1 ≠ cl_io → as_classify … s1' ≠ cl_io → 25 ∃s2'. ∃t: raw_trace S2 s2 s2'.26 ∃s2'. ∃t: raw_trace … S2 s2 s2'. 26 27 Srel … rel s1' s2' ∧ silent_trace … t 27 28 ; simulate_label: 28 29 ∀s1:S1.∀s2:S2.∀l.∀s1':S1. 29 as_execute S1 (cost_act(Some ? l)) s1 s1' →30 as_execute … S1 (cost_act … (Some ? l)) s1 s1' → 30 31 as_classify … s1 ≠ cl_io → as_classify … s1' ≠ cl_io → 31 32 Srel … rel s1 s2 → 32 33 ∃s2',s2'',s2'''. 33 ∃t1: raw_trace S2 s2 s2'.34 as_execute … (cost_act (Some ? l)) s2' s2'' ∧34 ∃t1: raw_trace … S2 s2 s2'. 35 as_execute … (cost_act … (Some ? l)) s2' s2'' ∧ 35 36 ∃t3: raw_trace … s2'' s2'''. 36 37 Srel … rel s1' s2''' ∧ silent_trace … t1 ∧ pre_silent_trace … t3 … … 38 39 ∀s1:S1.∀s2:S2.∀s1':S1.∀f,l. 39 40 is_call_post_label … s1 → 40 as_execute … (call_act f l) s1 s1' →41 as_execute … (call_act … f l) s1 s1' → 41 42 as_classify … s1 ≠ cl_io → as_classify … s1' ≠ cl_io → 42 43 Srel … rel s1 s2 → 43 44 ∃s2',s2'',s2'''. 44 ∃t1: raw_trace S2 s2 s2'.45 as_execute … (call_act f l) s2' s2'' ∧45 ∃t1: raw_trace … S2 s2 s2'. 46 as_execute … (call_act … f l) s2' s2'' ∧ 46 47 bool_to_Prop(is_call_post_label … s2') ∧ 47 ∃t3: raw_trace S2 s2'' s2'''.48 ∃t3: raw_trace … S2 s2'' s2'''. 48 49 Srel … rel s1' s2''' ∧ silent_trace … t1 ∧ pre_silent_trace … t3 49 50 ; simulate_ret_l: 50 51 ∀s1:S1.∀s2:S2.∀s1':S1.∀l. 51 as_execute S1 (ret_act(Some ? l)) s1 s1' →52 as_execute … S1 (ret_act … (Some ? l)) s1 s1' → 52 53 as_classify … s1 ≠ cl_io → as_classify … s1' ≠ cl_io → 53 54 Srel … rel s1 s2 → 54 55 ∃s2',s2'',s2'''. 55 ∃t1: raw_trace S2 s2 s2'.56 as_execute … (ret_act(Some ? l)) s2' s2'' ∧57 ∃t3: raw_trace S2 s2'' s2'''.56 ∃t1: raw_trace … S2 s2 s2'. 57 as_execute p S2 (ret_act p (Some ? l)) s2' s2'' ∧ 58 ∃t3: raw_trace … S2 s2'' s2'''. 58 59 Srel … rel s1' s2''' ∧ silent_trace … t1 ∧ pre_silent_trace … t3 59 60 ; simulate_call_n: 60 61 ∀s1:S1.∀s2:S2.∀s1':S1.∀f,l. 61 as_execute … (call_act f l) s1 s1' →62 as_execute … (call_act … f l) s1 s1' → 62 63 ¬ is_call_post_label … s1 → 63 64 as_classify … s1 ≠ cl_io → as_classify … s1' ≠ cl_io → 64 65 Srel … rel s1 s2 → 65 66 ∃s2',s2'',s2'''. 66 ∃t1: raw_trace S2 s2 s2'.67 ∃t1: raw_trace … S2 s2 s2'. 67 68 bool_to_Prop (¬ is_call_post_label … s2') ∧ 68 as_execute … (call_act f l) s2' s2'' ∧69 ∃t3: raw_trace S2 s2'' s2'''.69 as_execute … (call_act … f l) s2' s2'' ∧ 70 ∃t3: raw_trace … S2 s2'' s2'''. 70 71 Srel … rel s1' s2''' ∧ silent_trace … t1 ∧ pre_silent_trace … t3 71 72 ∧ Crel … rel s1 s2' 72 73 ; simulate_ret_n: 73 74 ∀s1:S1.∀s2:S2.∀s1':S1. 74 as_execute … (ret_act (None ?)) s1 s1' →75 as_execute … (ret_act … (None ?)) s1 s1' → 75 76 as_classify … s1 ≠ cl_io → as_classify … s1' ≠ cl_io → 76 77 Srel … rel s1 s2 → 77 78 ∃s2',s2'',s2''': S2. 78 ∃t1: raw_trace S2 s2 s2'.79 as_execute … (ret_act (None ?)) s2' s2'' ∧80 ∃t3: raw_trace S2 s2'' s2'''.79 ∃t1: raw_trace … S2 s2 s2'. 80 as_execute … (ret_act … (None ?)) s2' s2'' ∧ 81 ∃t3: raw_trace … S2 s2'' s2'''. 81 82 Srel … rel s1' s2''' ∧ pre_silent_trace … t1 ∧ pre_silent_trace … t3 82 83 ∧ Rrel … rel s1' s2'' … … 104 105 qed. 105 106 106 lemma simulate_labelled_action : ∀ S1,S2 : abstract_status.107 ∀rel : relations S1 S2.107 lemma simulate_labelled_action : ∀p.∀S1,S2 : abstract_status p. 108 ∀rel : relations … S1 S2. 108 109 ∀s1,s2 : S1.∀s1' : S2. 109 ∀l : ActionLabel .110 ∀l : ActionLabel p. 110 111 simulation_conditions … rel → 111 is_costlabelled_act l →112 (is_call_act l → is_call_post_label … s1) →112 is_costlabelled_act … l → 113 (is_call_act … l → is_call_post_label … s1) → 113 114 as_execute … l s1 s2 → 114 115 Srel … rel s1 s1' → … … 119 120 silent_trace … t_pre ∧ silent_trace … t_post ∧ 120 121 as_execute … l pre_em post_em ∧ 121 (is_call_act l → is_call_post_label … pre_em) ∧122 (is_call_act … l → is_call_post_label … pre_em) ∧ 122 123 Srel … rel s2 s2'. 123 # S1 #S2 #rel #s1 #s2 #s1' *124 #p #S1 #S2 #rel #s1 #s2 #s1' * 124 125 [ #f #c  * [#lbl]  * [#lbl]] 125 126 #sim * #Hcall #prf #REL * #Hio … … 162 163 163 164 164 theorem simulates_pre_mesurable: 165 ∀S1,S2 : abstract_status .∀rel : relationsS1 S2.166 ∀s1,s1' : S1. ∀t1: raw_trace S1 s1 s1'.165 theorem simulates_pre_mesurable: ∀p. 166 ∀S1,S2 : abstract_status p.∀rel : relations … S1 S2. 167 ∀s1,s1' : S1. ∀t1: raw_trace … S1 s1 s1'. 167 168 simulation_conditions … rel → 168 169 pre_measurable_trace … t1 → … … 175 176 (measurable_suffix … t1 → measurable_suffix … t2) ∧ 176 177 (silent_trace … t1 → silent_trace … t2). 177 # S1 #S2 #rel #s1 #s1' #t1 #sim #H elim H t1 s1 s1'178 #p #S1 #S2 #rel #s1 #s1' #t1 #sim #H elim H t1 s1 s1' 178 179 [ #st #Hst #s2 #Hs2 #Rsts2 %{s2} %{(t_base …)} % 179 180 [ % [ % // % // % //] * #s_em ** [ #sx  #x1 #x2 #x3 #l1 #prf1 #tl1] * #t_pre * #s_post * #t_post * #sil_tpost … … 243 244  #Hsuff cases(measurable_suffix_tind … Hsuff) 244 245 [ * #_ #sil_tl lapply(Hs sil_tl) #sil_ts3 %{s2''} %{t_s2''} %{s2'''} %{(t_s2'''' @ t_s3)} 245 % [ /3 by or_introl, append_silent/ ] %{(cost_act (Some ? lbl))} %{(exe_s2''')} % // % // * #f * #c #EQ destruct246  #H @measurable_suffix_append change with ((t_ind ?????? t_s2'''')@t_s3) in ⊢ (????%);246 % [ /3 by or_introl, append_silent/ ] %{(cost_act … (Some ? lbl))} %{(exe_s2''')} % // % // * #f * #c #EQ destruct 247  #H @measurable_suffix_append change with ((t_ind ??????? t_s2'''')@t_s3) in ⊢ (?????%); 247 248 @measurable_suffix_append /2/ 248 249 ] … … 279 280  #Hsuff cases(measurable_suffix_tind … Hsuff) 280 281 [ * #_ #sil_tl lapply(Hs sil_tl) #sil_ts3 %{st1} %{t1} %{st2} %{(t2 @ t_fin)} 281 % [ /3 by or_introl, append_silent/ ] %{(ret_act (Some ? ret_lab))} %{(exe_s2'')} % // % // * #f * #c #EQ destruct282  #H @measurable_suffix_append change with ((t_ind ?????? t2)@t_fin) in ⊢ (????%);282 % [ /3 by or_introl, append_silent/ ] %{(ret_act … (Some ? ret_lab))} %{(exe_s2'')} % // % // * #f * #c #EQ destruct 283  #H @measurable_suffix_append change with ((t_ind ??????? t2)@t_fin) in ⊢ (?????%); 283 284 @measurable_suffix_append /2/ 284 285 ] … … 317 318  #Hsuff cases(measurable_suffix_tind … Hsuff) 318 319 [ * #_ #sil_tl lapply(Hs sil_tl) #sil_ts3 %{s'} %{t1} %{s2''} %{(t2 @ t_fin)} 319 % [ /3 by or_introl, append_silent/ ] %{(call_act f lab)} %{(exe_s2'')} % // % //320  #H @measurable_suffix_append change with ((t_ind ?????? t2)@t_fin) in ⊢ (????%);320 % [ /3 by or_introl, append_silent/ ] %{(call_act … f lab)} %{(exe_s2'')} % // % // 321  #H @measurable_suffix_append change with ((t_ind ??????? t2)@t_fin) in ⊢ (?????%); 321 322 @measurable_suffix_append /2/ 322 323 ] … … 381 382 #st #EQ1 #EQ2 #EQ3 destruct normalize in ⊢ (% → ?); #EQ lapply(eq_to_jmeq ??? EQ) EQ #EQ destruct 382 383 #ABS1 >ABS1 in Hst1; [2: /3 by ex_intro/] * 383  #Hsuff @measurable_suffix_append change with (t_ind ??????? @ ?) in ⊢ (????%); @measurable_suffix_append384 change with (t_ind ??????? @ ?) in ⊢ (????%); @measurable_suffix_append @Hm2384  #Hsuff @measurable_suffix_append change with (t_ind ???????? @ ?) in ⊢ (?????%); @measurable_suffix_append 385 change with (t_ind ???????? @ ?) in ⊢ (?????%); @measurable_suffix_append @Hm2 385 386 cases(measurable_suffix_append_case … Hsuff) 386 387 [ * #_ * [2: * #H cases(H I)] #H inversion H in ⊢ ?; … … 403 404 qed. 404 405 405 lemma silent_in_silent : ∀ S1,S2 : abstract_status.∀rel : relationsS1 S2.406 ∀s1,s1' : S1. ∀t1: raw_trace S1 s1 s1'.406 lemma silent_in_silent : ∀p.∀S1,S2 : abstract_status p.∀rel : relations … S1 S2. 407 ∀s1,s1' : S1. ∀t1: raw_trace … S1 s1 s1'. 407 408 simulation_conditions … rel → 408 409 ∀s2 : S2.Srel … rel s1 s2 → … … 411 412 silent_trace … t2 ∧ 412 413 Srel … rel s1' s2'. 414 #p 413 415 #S1 #S2 #rel #s1 #s1' #t1 #sim #s2 #REL * 414 416 [ #pre_sil_ti0 cases(simulates_pre_mesurable … sim … (pre_silent_is_premeasurable … pre_sil_ti0) … REL) … … 423 425 qed. 424 426 425 lemma tail_of_premeasurable_is_not_io : ∀ S : abstract_status.427 lemma tail_of_premeasurable_is_not_io : ∀p.∀S : abstract_status p. 426 428 ∀s1,s2 : S.∀t : raw_trace … s1 s2. 427 429 pre_measurable_trace … t → 428 as_classify … s2 ≠ cl_io. 430 as_classify … s2 ≠ cl_io. #p 429 431 #S #s1 #s2 #t #H elim H // 430 432 qed. 431 433 432 434 theorem simulates_measurable: 433 ∀S1,S2: abstract_status. 434 435 ∀rel: relations S1 S2. simulation_conditions … rel → 435 ∀p. 436 ∀S1,S2: abstract_status p. 437 438 ∀rel: relations … S1 S2. simulation_conditions … rel → 436 439 437 440 ∀si,sn: S1. ∀t: raw_trace … si sn. … … 451 454 452 455 ∃s1',s2'. measurable … s1' s2' … t'. 453 # S1 #S2 #rel #sim_rel #si #sn #t #s1 #s3 #Hmeas #s1' #Hclass #Rsi_si'456 #p #S1 #S2 #rel #sim_rel #si #sn #t #s1 #s3 #Hmeas #s1' #Hclass #Rsi_si' 454 457 cases Hmeas Hmeas #s0 * #s2 * #ti0 * #t12 * #t3n * #l1 * #l2 * #prf1 * #prf2 ******* 455 458 #pre_t12 #EQ destruct #Hl1 #Hl2 #Hcall_fin #sil_ti0 #sil_t3n #Hcall_init … … 469 472 #sn' * #t_3n' * #sil_t3n' #Rsn_sn' %{sn'} 470 473 %{(ti0'@ t_s0'' @ (t_ind … prf1' (t_s1''@t12' @ t_s2'' @ (t_ind … prf2' (t_s3'' @ t_3n')))))} 471 % [ % // cases daemon (*TODO*) ] 474 % [ % // >(get_cost_label_invariant_for_append_silent_trace_l … sil_ti0) 475 >(get_cost_label_invariant_for_append_silent_trace_l … sil_ti0') 476 >(get_cost_label_invariant_for_append_silent_trace_l … sil_ts0'') 477 whd in ⊢ (??%%); @eq_f2 // 478 >(get_cost_label_invariant_for_append_silent_trace_l … sil_ts1'') 479 >get_cost_label_append >get_cost_label_append in ⊢ (???%); @eq_f2 // 480 >(get_cost_label_invariant_for_append_silent_trace_l … sil_ts2'') 481 whd in ⊢ (??%%); @eq_f2 // 482 >(get_cost_label_invariant_for_append_silent_trace_l … sil_ts3'') 483 >(get_cost_label_silent_is_empty … sil_t3n') >(get_cost_label_silent_is_empty … sil_t3n) % ] 472 484 %{s1''} %{s3''} whd %{s0''} %{s2''} %{(ti0' @t_s0'')} %{(t_s1'' @ t12' @ t_s2'')} 473 485 %{(t_s3'' @ t_3n')} %{l1} %{l2} %{prf1'} %{prf2'} % [2: /2/] 474 486 % [2: /2 by append_silent/] % [2: /2 by append_silent/] % [2: /2/] % // % // % // 475 487 @append_premeasurable_silent /2/ 476 qed. 477 478 488 qed. 489 490
Note: See TracChangeset
for help on using the changeset viewer.