Changeset 3504
 Timestamp:
 Sep 26, 2014, 3:44:01 PM (5 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

LTS/Simulation.ma
r3486 r3504 1 1 include "Traces.ma". 2 2 3 record relations (S : abstract_status) : Type[0] ≝4 { Srel: S → S→ Prop5 ; Crel: S → S→ Prop3 record relations (S1,S2 : abstract_status) : Type[0] ≝ 4 { Srel: S1 → S2 → Prop 5 ; Crel: S1 → S2 → Prop 6 6 }. 7 7 8 definition Rrel ≝ λS : abstract_status.λrel : relations S.λs,s' : S.9 ∀s1,s1'. as_syntactical_succ S s1 s → Crel … rel s1 s1' → as_syntactical_succ Ss1' s'.10 11 record simulation_conditions (S : abstract_status) (rel : relations S) : Prop ≝8 definition Rrel ≝ λS1,S2 : abstract_status.λrel : relations S1 S2.λs,s'. 9 ∀s1,s1'. as_syntactical_succ S1 s1 s → Crel … rel s1 s1' → as_syntactical_succ S2 s1' s'. 10 11 record simulation_conditions (S1,S2 : abstract_status) (rel : relations S1 S2) : Prop ≝ 12 12 { initial_is_initial : 13 ∀s1,s2 : S.Srel … rel s1 s2 → (bool_to_Prop (as_initial … s1) → bool_to_Prop (as_initial … s2))13 ∀s1,s2.Srel … rel s1 s2 → (bool_to_Prop (as_initial … s1) → bool_to_Prop (as_initial … s2)) 14 14 ; final_is_final : 15 ∀s1,s2 : S.Srel … rel s1 s2 → (bool_to_Prop(as_final … s1) → bool_to_Prop (as_final … s2))15 ∀s1,s2.Srel … rel s1 s2 → (bool_to_Prop(as_final … s1) → bool_to_Prop (as_final … s2)) 16 16 ; simulate_tau: 17 ∀s1 ,s2,s1' : S.17 ∀s1:S1.∀s2:S2.∀s1':S1. 18 18 as_execute … (cost_act (None ?)) s1 s1'→ 19 19 Srel … rel s1 s2 → as_classify … s1 ≠ cl_io → as_classify … s1' ≠ cl_io → 20 ∃s2'. ∃t: raw_trace S s2 s2'.20 ∃s2'. ∃t: raw_trace S2 s2 s2'. 21 21 Srel … rel s1' s2' ∧ silent_trace … t 22 22 ; simulate_label: 23 ∀s1 ,s2,l,s1'.24 as_execute S (cost_act (Some ? l)) s1 s1' →23 ∀s1:S1.∀s2:S2.∀l.∀s1':S1. 24 as_execute S1 (cost_act (Some ? l)) s1 s1' → 25 25 as_classify … s1 ≠ cl_io → as_classify … s1' ≠ cl_io → 26 26 Srel … rel s1 s2 → 27 27 ∃s2',s2'',s2'''. 28 ∃t1: raw_trace S s2 s2'.28 ∃t1: raw_trace S2 s2 s2'. 29 29 as_execute … (cost_act (Some ? l)) s2' s2'' ∧ 30 ∃t3: raw_trace Ss2'' s2'''.30 ∃t3: raw_trace … s2'' s2'''. 31 31 Srel … rel s1' s2''' ∧ silent_trace … t1 ∧ pre_silent_trace … t3 32 32 ; simulate_call_pl: 33 ∀s1 ,s2,s1' : S.∀f,l.33 ∀s1:S1.∀s2:S2.∀s1':S1.∀f,l. 34 34 is_call_post_label … s1 → 35 35 as_execute … (call_act f l) s1 s1' → … … 37 37 Srel … rel s1 s2 → 38 38 ∃s2',s2'',s2'''. 39 ∃t1: raw_trace S s2 s2'.39 ∃t1: raw_trace S2 s2 s2'. 40 40 as_execute … (call_act f l) s2' s2'' ∧ 41 41 bool_to_Prop(is_call_post_label … s2') ∧ 42 ∃t3: raw_trace S s2'' s2'''.42 ∃t3: raw_trace S2 s2'' s2'''. 43 43 Srel … rel s1' s2''' ∧ silent_trace … t1 ∧ pre_silent_trace … t3 44 44 ; simulate_ret_l: 45 ∀s1 ,s2,s1' : S.∀l.46 as_execute S (ret_act (Some ? l)) s1 s1' →45 ∀s1:S1.∀s2:S2.∀s1':S1.∀l. 46 as_execute S1 (ret_act (Some ? l)) s1 s1' → 47 47 as_classify … s1 ≠ cl_io → as_classify … s1' ≠ cl_io → 48 48 Srel … rel s1 s2 → 49 49 ∃s2',s2'',s2'''. 50 ∃t1: raw_trace S s2 s2'.50 ∃t1: raw_trace S2 s2 s2'. 51 51 as_execute … (ret_act (Some ? l)) s2' s2'' ∧ 52 ∃t3: raw_trace S s2'' s2'''.52 ∃t3: raw_trace S2 s2'' s2'''. 53 53 Srel … rel s1' s2''' ∧ silent_trace … t1 ∧ pre_silent_trace … t3 54 54 ; simulate_call_n: 55 ∀s1 ,s2,s1' : S.∀f,l.55 ∀s1:S1.∀s2:S2.∀s1':S1.∀f,l. 56 56 as_execute … (call_act f l) s1 s1' → 57 57 ¬ is_call_post_label … s1 → … … 59 59 Srel … rel s1 s2 → 60 60 ∃s2',s2'',s2'''. 61 ∃t1: raw_trace S s2 s2'.61 ∃t1: raw_trace S2 s2 s2'. 62 62 bool_to_Prop (¬ is_call_post_label … s2') ∧ 63 63 as_execute … (call_act f l) s2' s2'' ∧ 64 ∃t3: raw_trace S s2'' s2'''.64 ∃t3: raw_trace S2 s2'' s2'''. 65 65 Srel … rel s1' s2''' ∧ silent_trace … t1 ∧ pre_silent_trace … t3 66 66 ∧ Crel … rel s1 s2' 67 67 ; simulate_ret_n: 68 ∀s1 ,s2,s1' : S.68 ∀s1:S1.∀s2:S2.∀s1':S1. 69 69 as_execute … (ret_act (None ?)) s1 s1' → 70 70 as_classify … s1 ≠ cl_io → as_classify … s1' ≠ cl_io → 71 71 Srel … rel s1 s2 → 72 ∃s2',s2'',s2''' .73 ∃t1: raw_trace S s2 s2'.72 ∃s2',s2'',s2''': S2. 73 ∃t1: raw_trace S2 s2 s2'. 74 74 as_execute … (ret_act (None ?)) s2' s2'' ∧ 75 ∃t3: raw_trace S s2'' s2'''.75 ∃t3: raw_trace S2 s2'' s2'''. 76 76 Srel … rel s1' s2''' ∧ pre_silent_trace … t1 ∧ pre_silent_trace … t3 77 77 ∧ Rrel … rel s1' s2'' 78 78 ; simulate_io_in : 79 ∀s1 ,s2,s1' : S.∀l.79 ∀s1:S1.∀s2:S2.∀s1':S1.∀l. 80 80 as_execute … (cost_act … (Some ? l)) s1 s1' → 81 81 as_classify … s1 ≠ cl_io → as_classify … s1' = cl_io → 82 82 Srel … rel s1 s2 → 83 ∃s2',s2'' : S.∃t: raw_trace … s2 s2'.83 ∃s2',s2''.∃t: raw_trace … s2 s2'. 84 84 pre_silent_trace … t ∧ as_execute … (cost_act … (Some ? l)) s2' s2'' ∧ 85 85 as_classify … s2'' = cl_io ∧ Srel … rel s1' s2'' 86 86 ; simulate_io_out : 87 ∀s1,s2,s1' : S.∀l.87 ∀s1:S1.∀s2:S2.∀s1':S1.∀l. 88 88 as_execute … (cost_act … (Some ? l)) s1 s1' → 89 89 as_classify … s1 = cl_io → as_classify … s1' ≠ cl_io → 90 90 Srel … rel s1 s2 → 91 ∃s2',s2'' : S.∃t : raw_trace … s2' s2''.91 ∃s2',s2''.∃t : raw_trace … s2' s2''. 92 92 pre_silent_trace … t ∧ as_execute … (cost_act … (Some ? l)) s2 s2' ∧ 93 93 as_classify … s2 = cl_io ∧ Srel … rel s1' s2'' 94 94 }. 95 96 let rec get_costlabels_of_trace (S : abstract_status) (st1 : S) (st2 : S)97 (t : raw_trace S st1 st2) on t : list CostLabel ≝98 match t with99 [ t_base st ⇒ [ ]100  t_ind st1' st2' st3' l prf t' ⇒101 let tl ≝ get_costlabels_of_trace … t' in102 match l with103 [ call_act f c ⇒ [ c ]104  ret_act x ⇒ match x with105 [ Some c ⇒ [ a_return_post c ]106  None ⇒ []107 ]108  cost_act x ⇒ match x with109 [ Some c ⇒ [ a_non_functional_label c ]110  None ⇒ []111 ]112 113 ] @ tl114 ].115 116 95 117 96 lemma append_premeasurable_silent : ∀S : abstract_status. … … 235 214 qed. 236 215 237 lemma get_cost_label_append : ∀S : abstract_status.∀st1,st2,st3 : S.238 ∀t1 : raw_trace … st1 st2. ∀t2 : raw_trace … st2 st3.239 get_costlabels_of_trace … (t1 @ t2) =240 append … (get_costlabels_of_trace … t1) (get_costlabels_of_trace … t2).241 #S #st1 #st2 #st3 #t1 elim t1 [ #st #t2 % ] #st1' #st2' #st3' *242 [#f * #l  * [ * #l]  * [ #l] ] #prf #tl #IH #t2 normalize try @eq_f @IH243 qed.244 245 216 (* 246 217 lemma raw_trace_ind_r : ∀S : abstract_status. … … 261 232 qed. 262 233 263 264 234 theorem simulates_pre_mesurable: 265 ∀S : abstract_status.∀rel : relations S.266 ∀s1,s1' : S . ∀t1: raw_trace Ss1 s1'.267 simulation_conditions Srel →235 ∀S1,S2 : abstract_status.∀rel : relations S1 S2. 236 ∀s1,s1' : S1. ∀t1: raw_trace S1 s1 s1'. 237 simulation_conditions … rel → 268 238 pre_measurable_trace … t1 → 269 ∀s2 : S .239 ∀s2 : S2. 270 240 as_classify … s2 ≠ cl_io → Srel … rel s1 s2 → 271 241 ∃s2'. ∃t2: raw_trace … s2 s2'. … … 273 243 get_costlabels_of_trace … t1 = get_costlabels_of_trace … t2 ∧ 274 244 Srel … rel s1' s2'. 275 #S #rel #s1 #s1' #t1 #good #pre_measurable elim pre_measurable245 #S1 #S2 #rel #s1 #s1' #t1 #good #pre_measurable elim pre_measurable 276 246 [ #st #H1 #s2 #REL #Hs2 %{s2} %{(t_base …)} 277 247 /8 by refl, silent_empty, conj, pre_silent_is_premeasurable/ … … 388 358 qed. 389 359 390 391 360 (* IDEA: aggiungere stati di I/O e cambiare la semantica del linguaggio 392 361 sorgente; aggiungere nella pre_measurable il vincolo nessuno stato e' di I/O; 393 362 cambiare la definizione di traccia tornando a una sola etichetta sugli archi *) 394 363 (* 395 364 (* measurable fattorizzata sotto come measurable' 396 365 definition measurable ≝ … … 402 371 403 372 record measurable_trace (S : abstract_status) : Type[0] ≝ 404 { L_s1 : S 373 { L_label: option ActionLabel 374 ; R_label : option ActionLabel 375 ; L_pre_state : option S 376 ; L_s1 : S 405 377 ; R_s2: S 378 ; R_post_state : option S 406 379 ; trace : raw_trace S L_s1 R_s2 407 380 ; pre_meas : pre_measurable_trace … trace 408 }. 381 ; L_init_ok : match L_pre_state with 382 [ None ⇒ bool_to_Prop(as_initial … L_s1) ∧ L_label = None ? 383  Some s ⇒ ∃l. L_label = Some ? l ∧ is_costlabelled_act l ∧ 384 as_execute … l s L_s1 385 ] 386 ; R_fin_ok : match R_label with 387 [ None ⇒ bool_to_Prop (as_final … R_s2) ∧ R_post_state = None ? 388  Some l ⇒ (is_costlabelled_act l ∨ is_unlabelled_ret_act l) ∧ 389 (is_call_act l → bool_to_Prop (is_call_post_label … R_s2)) ∧ 390 ∃ s'.R_post_state = Some ? s' ∧ as_execute … l R_s2 s' 391 ] 392 }. 409 393 410 394 lemma cl_io_case : ∀P : status_class → Prop. P cl_io → (∀x.x≠cl_io → P x) → ∀s.P s. … … 418 402 as_classify … st2 ≠ cl_io. 419 403 #S #st1 #st2 #t #H elim H // 420 qed.421 422 lemma get_cost_label_silent_is_empty : ∀S : abstract_status.423 ∀st1,st2.∀t : raw_trace S st1 st2.silent_trace … t → get_costlabels_of_trace … t = [ ].424 #S #st1 #st2 #t elim t [//] #s1 #s2 #s3 #l #prf #tl #IH * [2: * #ABS @⊥ @ABS % ]425 #H inversion H426 [#s #cl #EQ1 #EQ2 #EQ3 destruct] #s1' #s2' #s3' #prf' #tl' #cl' #Htl #_ #EQ1 #EQ2 #EQ3427 destruct #_ @IH % assumption428 404 qed. 429 405 … … 436 412 qed. 437 413 438 lemma instr_execute_commute : ∀S :abstract_status.439 ∀rel : relations S .414 lemma instr_execute_commute : ∀S1,S2 :abstract_status. 415 ∀rel : relations S1 S2. 440 416 simulation_conditions … rel → 441 ∀s1,s1': S .∀l.l ≠ cost_act (None ?) → as_execute Sl s1 s1' →417 ∀s1,s1': S1.∀l.l ≠ cost_act (None ?) → as_execute … l s1 s1' → 442 418 (as_classify … s1 ≠ cl_io ∨ as_classify … s1' ≠ cl_io) → 443 419 ∀s2. 444 420 Srel … rel s1 s2 → 445 ∃s2' : S .∃tr : raw_trace Ss2 s2'.silent_trace … tr ∧446 ∃s2'' : S .as_execute S l s2' s2'' ∧ ∃s2''' : S.447 ∃tr' : raw_trace Ss2'' s2'''. silent_trace … tr' ∧ Srel … rel s1' s2''' ∧421 ∃s2' : S2.∃tr : raw_trace … s2 s2'.silent_trace … tr ∧ 422 ∃s2'' : S2.as_execute … l s2' s2'' ∧ ∃s2''' : S2. 423 ∃tr' : raw_trace … s2'' s2'''. silent_trace … tr' ∧ Srel … rel s1' s2''' ∧ 448 424 (is_call_act l → is_call_post_label … s1 → is_call_post_label … s2') ∧ 449 425 (as_classify … s1' ≠ cl_io → as_classify … s2'' ≠ cl_io). 450 #S #rel #good #s1 #s1' #l #l_notau #prf #HIO #s2 #REL cases(case_cl_io … (as_classify … s1))426 #S1 #S2 #rel #good #s1 #s1' #l #l_notau #prf #HIO #s2 #REL cases(case_cl_io … (as_classify … s1)) 451 427 [ #EQs1_io cases(io_exiting … EQs1_io … prf) #lab #EQ destruct(EQ) 452 428 cases HIO [ >EQs1_io * #EQ @⊥ @EQ % ] #Hio_s1' … … 499 475 qed. 500 476 501 (*502 477 theorem simulate_LR_trace : 503 ∀S : abstract_status.504 ∀t : measurable_trace S .505 ∀rel : relations S .478 ∀S1,S2 : abstract_status. 479 ∀t : measurable_trace S1. 480 ∀rel : relations S1 S2. 506 481 simulation_conditions … rel → 507 ∀s2 : S .482 ∀s2 : S2. 508 483 match L_pre_state … t with 509 484 [ None ⇒ … … 511 486 Srel … rel (L_s1 … t) s2 512 487  Some s1 ⇒ Srel … rel s1 s2 ] → 513 ∃t' : measurable_trace S .488 ∃t' : measurable_trace S2. 514 489 L_label … t = L_label … t' ∧ R_label … t = R_label … t' ∧ 515 490 get_costlabels_of_trace … (trace … t) = … … 518 493 [ None ⇒ L_s1 … t' = s2 519 494  Some s1 ⇒ 520 ∃ pre_state : S .495 ∃ pre_state : S2. 521 496 L_pre_state … t' = Some ? pre_state ∧ 522 ∃tr_i : raw_trace Ss2 pre_state. silent_trace … tr_i497 ∃tr_i : raw_trace … s2 pre_state. silent_trace … tr_i 523 498 ] ∧ 524 499 match R_post_state … t with 525 500 [ None ⇒ Srel … rel (R_s2 … t) (R_s2 … t') 526 501  Some s1' ⇒ 527 ∃s2' : S . Srel … rel s1' s2' ∧528 ∃ post_state : S .502 ∃s2' : S2. Srel … rel s1' s2' ∧ 503 ∃ post_state : S2. 529 504 R_post_state … t' = Some ? post_state ∧ 530 ∃tr : raw_trace Spost_state s2'. silent_trace … tr505 ∃tr : raw_trace … post_state s2'. silent_trace … tr 531 506 ]. 532 #S #t #rel #good #s2 inversion(L_pre_state … t) [ #pre_s1] #EQpre normalize nodelta [* #Hclass_s2 ]507 #S1 #S2 #t #rel #good #s2 inversion(L_pre_state … t) [ #pre_s1] #EQpre normalize nodelta [* #Hclass_s2 ] 533 508 [2: #REL_pre 534 509 cut 535 (∃pre_state : S.∃ l.536 ∃tr_i : raw_trace Ss2 pre_state. silent_trace … tr_i ∧537 ∃middle_state : S.L_label … t = Some ? l ∧510 (∃pre_state.∃ l. 511 ∃tr_i : raw_trace … s2 pre_state. silent_trace … tr_i ∧ 512 ∃middle_state.L_label … t = Some ? l ∧ 538 513 as_execute … l pre_state middle_state ∧ 539 ∃final_state : S.540 ∃tr_i2: raw_trace Smiddle_state final_state. silent_trace … tr_i2 ∧514 ∃final_state. 515 ∃tr_i2: raw_trace … middle_state final_state. silent_trace … tr_i2 ∧ 541 516 as_classify … final_state ≠ cl_io ∧ 542 517 Srel … rel (L_s1 … t) final_state) … … 553 528 * #final_state * #tr_i2 ** #silent_i2 #final_not_io #REL 554 529  #REL 555 cut(bool_to_Prop (as_initial S s2)∧L_label St=None ?)530 cut(bool_to_Prop (as_initial … s2)∧L_label … t=None ?) 556 531 [ lapply(L_init_ok … t) >EQpre normalize nodelta * #H1 #H2 % [2: //] 557 532 @(initial_is_initial … good … H1) assumption ] * #initial_s2 #init_label … … 560 535 #fin_s2 * #t' ** #pre_meas_t' #EQcost #REL' inversion(R_post_state … t) 561 536 [2,4: #post_s2] #EQpost normalize nodelta 562 [3,4: cut (match R_label St in option return λ_:(option ActionLabel).Prop with563 [None⇒bool_to_Prop (as_final S fin_s2)∧None S=None S537 [3,4: cut (match R_label … t in option return λ_:(option ActionLabel).Prop with 538 [None⇒bool_to_Prop (as_final … fin_s2)∧None S2=None S2 564 539 Some (l:ActionLabel)⇒ 565 540 (is_costlabelled_act l∨is_unlabelled_ret_act l) 566 ∧(is_call_act l→is_call_post_label Sfin_s2)567 ∧(∃s' :S.None S=Some S s'∧as_execute Sl fin_s2 s')])541 ∧(is_call_act l→is_call_post_label … fin_s2) 542 ∧(∃s'.None S2=Some … s'∧as_execute … l fin_s2 s')]) 568 543 [1,3: lapply(R_fin_ok … t) cases(R_label … t) normalize nodelta 569 544 [1,3: * #H1 #H2 % [2,4: //] @(final_is_final … good … H1) assumption … … 575 550 #a #_ %{a} % ] * #final_label #EQfinal_label 576 551 cut 577 (∃middle_state : S.578 ∃tr : raw_trace Sfin_s2 middle_state. silent_trace … tr ∧579 ∃post_state : S.552 (∃middle_state. 553 ∃tr : raw_trace … fin_s2 middle_state. silent_trace … tr ∧ 554 ∃post_state. 580 555 as_execute … final_label middle_state post_state ∧ 581 556 (is_call_act final_label → bool_to_Prop (is_call_post_label … middle_state)) ∧ 582 ∃final_state : S.583 ∃tr_f2: raw_trace Spost_state final_state. silent_trace … tr_f2 ∧557 ∃final_state. 558 ∃tr_f2: raw_trace … post_state final_state. silent_trace … tr_f2 ∧ 584 559 Srel … rel post_s2 final_state) 585 560 [1,3: lapply(R_fin_ok … t) >EQfinal_label normalize nodelta ** #H1 #H2 * #sfin … … 833 808 ] 834 809 *) 835 *)
Note: See TracChangeset
for help on using the changeset viewer.