Changeset 3506 for LTS/Simulation.ma


Ignore:
Timestamp:
Sep 26, 2014, 5:00:57 PM (5 years ago)
Author:
sacerdot
Message:

Refactoring.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • LTS/Simulation.ma

    r3504 r3506  
    361361   sorgente; aggiungere nella pre_measurable il vincolo nessuno stato e' di I/O;
    362362   cambiare la definizione di traccia tornando a una sola etichetta sugli archi *)
     363
    363364(*
    364 (* measurable fattorizzata sotto come measurable'
    365 definition measurable ≝
    366  λL,s1,s2.λt: raw_trace … s1 s2.
    367   ∃L',s0,so. as_execute … s0 s1 L ∧
    368   pre_measurable_trace … t ∧
    369   well_formed_trace … t ∧
    370   as_execute … s2 so L'. *)
    371 
    372 record measurable_trace (S : abstract_status) : Type[0] ≝
    373  { L_label: option ActionLabel
    374  ; R_label : option ActionLabel
    375  ; L_pre_state : option S
    376  ; L_s1 : S
    377  ; R_s2: S
    378  ; R_post_state : option S
    379  ; trace : raw_trace S L_s1 R_s2
    380  ; pre_meas : pre_measurable_trace … trace
    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 }.
    393 
    394365lemma cl_io_case : ∀P : status_class → Prop. P cl_io → (∀x.x≠cl_io → P x) → ∀s.P s.
    395366#P #H1 #H2 * // @H2 % #EQ destruct qed.
     
    474445]
    475446qed.
    476 
    477 theorem simulate_LR_trace :
    478 ∀S1,S2 : abstract_status.
    479 ∀t : measurable_trace S1.
    480 ∀rel : relations S1 S2.
    481 simulation_conditions … rel →
    482 ∀s2 : S2.
    483 match L_pre_state … t with
    484 [ None ⇒
    485    as_classify … s2 ≠ cl_io ∧
    486    Srel … rel (L_s1 … t) s2 
    487 | Some s1 ⇒ Srel … rel s1 s2 ] →
    488 ∃t' : measurable_trace S2.
    489  L_label … t = L_label … t' ∧ R_label … t = R_label … t' ∧
    490  get_costlabels_of_trace … (trace … t) =
    491   get_costlabels_of_trace … (trace … t') ∧
    492 match L_pre_state … t with
    493 [ None ⇒ L_s1 … t' = s2
    494 | Some s1 ⇒
    495          ∃ pre_state : S2.
    496          L_pre_state … t' = Some ? pre_state ∧
    497          ∃tr_i : raw_trace … s2 pre_state. silent_trace … tr_i
    498 ] ∧
    499 match R_post_state … t with         
    500 [ None ⇒ Srel … rel (R_s2 … t) (R_s2 … t')
    501 | Some s1' ⇒
    502           ∃s2' : S2. Srel … rel s1' s2' ∧
    503           ∃ post_state : S2.
    504           R_post_state … t' = Some ? post_state ∧
    505           ∃tr : raw_trace … post_state s2'. silent_trace … tr
    506 ].
    507 #S1 #S2 #t #rel #good #s2 inversion(L_pre_state … t) [| #pre_s1] #EQpre normalize nodelta [* #Hclass_s2 ]
    508 [2: #REL_pre
    509     cut
    510      (∃pre_state.∃ l.
    511       ∃tr_i : raw_trace … s2 pre_state. silent_trace … tr_i ∧
    512       ∃middle_state.L_label … t = Some ? l ∧
    513        as_execute … l pre_state middle_state ∧
    514       ∃final_state.
    515       ∃tr_i2: raw_trace … middle_state final_state. silent_trace … tr_i2 ∧
    516        as_classify … final_state ≠ cl_io ∧
    517        Srel … rel (L_s1 … t) final_state)
    518       [ lapply(L_init_ok … t) >EQpre normalize nodelta * #l ** #EQllabe #Hcost #exe   
    519       cases(instr_execute_commute … good … l … exe … REL_pre)
    520       [2: % #EQ >EQ in Hcost; * |3: %2 @(head_of_premeasurable_is_not_io … (pre_meas … t)) ]
    521       #s2' * #t1 * #sil_t1 * #s2'' * #exe * #s2''' * #t3 *** #sil_t3 #REL' #Hcall
    522       #Hclass %{s2'} %{l} %{t1} %{sil_t1} %{s2''} % [% //] %{s2'''} %{t3} % // % //
    523       cases sil_t3 [/2 by pre_silent_io/ ] inversion t3
    524       [ #H109 #H110 #H111 #H112 #H113 destruct @Hclass @(head_of_premeasurable_is_not_io … (pre_meas … t)) ]
    525       #H115 #H116 #H117 #H118 #H119 #H120 #H121 #H122 #H123 #H124 #H125 cases H125
    526       #H @⊥ @H %]
    527     * #pre_state * #l' * #tr_i * #silent_i * #middle_state ** #EQl' #step_pre_middle
    528     * #final_state * #tr_i2 ** #silent_i2 #final_not_io #REL
    529 | #REL
    530   cut(bool_to_Prop (as_initial … s2)∧L_label … t=None ?)
    531       [ lapply(L_init_ok … t) >EQpre normalize nodelta * #H1 #H2 % [2: //]
    532         @(initial_is_initial … good … H1) assumption ] * #initial_s2 #init_label
    533 ]
    534 cases(simulates_pre_mesurable … good … (pre_meas … t) … REL) //
    535 #fin_s2 * #t' ** #pre_meas_t' #EQcost #REL' inversion(R_post_state … t)
    536 [2,4: #post_s2] #EQpost normalize nodelta
    537 [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
    539  |Some (l:ActionLabel)⇒
    540   (is_costlabelled_act l∨is_unlabelled_ret_act l)
    541   ∧(is_call_act l→is_call_post_label … fin_s2)
    542   ∧(∃s'.None S2=Some … s'∧as_execute … l fin_s2 s')])
    543   [1,3: lapply(R_fin_ok … t) cases(R_label … t) normalize nodelta
    544       [1,3: * #H1 #H2 % [2,4: //] @(final_is_final … good … H1) assumption
    545       |*: #a ** #_ #_ * #x * >EQpost #EQ destruct
    546       ]
    547   ] #R_label_fin
    548 |*: cut(∃l.(R_label … t) = Some ? l)
    549     [1,3:  lapply(R_fin_ok … t) cases(R_label… t) normalize nodelta [1,3: >EQpost * #_ #EQ destruct]
    550           #a #_ %{a} % ] * #final_label #EQfinal_label
    551      cut
    552       (∃middle_state.
    553        ∃tr : raw_trace … fin_s2 middle_state. silent_trace … tr ∧
    554        ∃post_state.
    555        as_execute … final_label middle_state post_state ∧
    556        (is_call_act final_label → bool_to_Prop (is_call_post_label … middle_state)) ∧
    557        ∃final_state.
    558        ∃tr_f2: raw_trace … post_state final_state. silent_trace … tr_f2 ∧
    559        Srel … rel post_s2 final_state)
    560      [1,3: lapply(R_fin_ok … t) >EQfinal_label normalize nodelta ** #H1 #H2 * #sfin
    561          * >EQpost #EQ destruct #exe
    562           cases(instr_execute_commute … good … final_label … exe … REL')
    563           [2,5: % #EQ destruct cases H1 [1,3,5,7: * |*: normalize #EQ destruct]
    564           |3,6: %1 @tail_of_premeasurable_is_not_io //
    565           ]
    566           #s2' * #t1 * #sil_t1 * #s2'' * #exe * #s2''' * #t3 *** #sil_t3 #REL'
    567           #Hcall #Hclass %{s2'} %{t1} %{sil_t1} %{s2''} % [2,4: %{s2'''} %{t3} % //]
    568           % // #H @Hcall // @H2 // ] * #middle_state' * #tr' * #sil_tr' * #post_state' ** #exe'
    569      #Hcall * #final_state' * #tr_f2 * #sil_tr_f2 #fin_rel
    570 ]
    571 [2: %{(mk_measurable_trace … (L_label … t) (R_label … t) … (None ?) … (None ?) … pre_meas_t' …)}
    572      normalize nodelta /5 by conj/
    573 |3: %{(mk_measurable_trace … (L_label … t) (R_label … t) … (Some ? pre_state) … (Some ? post_state') … (tr_i2 @ t' @ tr') …)}
    574     normalize nodelta [2: %{l'} % // % // lapply(L_init_ok … t) >EQpre normalize nodelta * #l'' ** >EQl'
    575       #EQ destruct //
    576     |3: /3 by append_silent_premeasurable, append_premeasurable_silent/
    577     |4: % [2: %{final_state'} /5 by ex_intro, conj/ ] % /8 by ex_intro, conj/ % [ /3 by conj/]
    578         >get_cost_label_append >get_cost_label_silent_is_empty in ⊢ (???%); [2: //]
    579         >get_cost_label_append >get_cost_label_silent_is_empty in ⊢ (???(???(???%)));
    580         /2 by refl, pair_destruct_1/
    581     | lapply(R_fin_ok … t) >EQfinal_label normalize nodelta ** #H #_ #_
    582       % [2: /3 by ex_intro, conj/ ] % [2: @Hcall ] //
    583     ]
    584 | %{(mk_measurable_trace … (L_label … t) (R_label … t) … (Some ? pre_state) … (None ?) … (tr_i2 @ t') …)}
    585   normalize nodelta
    586   [ assumption
    587   | %{l'} % // % // lapply(L_init_ok … t) >EQpre normalize nodelta * #l'' ** >EQl' #EQ destruct //
    588   | /4 by append_premeasurable_silent/
    589   | % // % [2: %{pre_state} /3/ ] % [ /2/] >get_cost_label_append
    590     >get_cost_label_silent_is_empty in ⊢ (???%); [2: //] /2 by refl, pair_destruct_1/
    591   ]
    592 | %{(mk_measurable_trace … (L_label … t) (R_label … t) … (None ?) … (Some ? post_state') … (t' @ tr') …)}
    593   normalize nodelta
    594  [ lapply(R_fin_ok … t) >EQfinal_label normalize nodelta ** #H #_ #_
    595       % [2: /3 by ex_intro, conj/ ] % [2: @Hcall ] //
    596  | /2/
    597  | /3 by append_silent_premeasurable/
    598  | % [2: %{final_state'} /5 by ex_intro, conj/
    599  | % [2: % ] % [ /2/] >get_cost_label_append >get_cost_label_silent_is_empty in ⊢ (???(???%));
    600    // ]
    601  ]   
    602 ]
    603 qed.   
    604 (*
    605 xxxxxxxxxxxxxxxxxxxx
    606  
    607 theorem simulate_LR_trace :
    608 ∀S : abstract_status.
    609 ∀t : measurable_trace S.
    610 ∀rel : relations S.
    611 simulation_conditions … rel →
    612 ∀s2 : S.
    613 match L_pre_state … t with
    614 [ None ⇒ as_classify … s2 ≠ cl_io → Srel … rel (L_s1 … t) s2 → 
    615          ∃t' : measurable_trace S.L_s1 … t' = s2 ∧
    616          L_label … t = L_label … t' ∧ R_label … t = R_label … t' ∧
    617          get_costlabels_of_trace … (trace … t) =
    618                       get_costlabels_of_trace … (trace … t') ∧
    619          match R_post_state … t with
    620          [ None ⇒  Srel … rel (R_s2 … t) (R_s2 … t')
    621          | Some s2' ⇒ ∃prf : (R_post_state … t' ≠ None ?).
    622                       ∃post_state : S.
    623                       ∃tr : raw_trace S (opt_safe … prf) post_state.
    624                       silent_trace … tr ∧ Srel … rel s2' post_state
    625          ]
    626 | Some s1 ⇒ Srel … rel s1 s2 →
    627             ∃ pre_state : S.∃tr_i : raw_trace S s2 pre_state.
    628             silent_trace … tr_i ∧
    629             ∃t' : measurable_trace S.L_pre_state … t' = Some ? pre_state ∧
    630             L_label … t = L_label … t' ∧ R_label … t = R_label … t' ∧
    631             get_costlabels_of_trace … (trace … t) =
    632                       get_costlabels_of_trace … (trace … t') ∧
    633             match R_post_state … t with         
    634             [ None ⇒ Srel … rel (R_s2 … t) (R_s2 … t')
    635             | Some s2' ⇒ ∃prf : (R_post_state … t' ≠ None ?).
    636                          ∃post_state : S.
    637                          ∃tr : raw_trace S (opt_safe … prf) post_state.
    638                          silent_trace … tr ∧ Srel … rel s2' post_state
    639             ]
    640 ].
    641 #S #t #rel #good #s2 inversion(L_pre_state … t) [| #pre_s1] #EQpre normalize nodelta [ #Hclass_s2 ]
    642 #REL inversion(R_post_state … t) [2,4: #post_s2 ] #EQpost normalize nodelta
    643 [1,3: cases(simulates_pre_mesurable … good … (pre_meas … t) … REL) [2,4: assumption]
    644      #fin_s2 * #t' ** #pre_meas_t' #EQcost #REL
    645      [2: %{(mk_measurable_trace … (L_label … t) (R_label … t) (None ?) … (None ?) … pre_meas_t' …)}
    646          [ inversion(R_label … t) normalize nodelta
    647            [ #EQnone % // cases(final_is_final … good … REL) #H #_ @H lapply(R_fin_ok … t)
    648              >EQnone normalize nodelta * //
    649            | #r_lab #EQr_lab lapply(R_fin_ok … t) >EQr_lab normalize nodelta * #_ * #x *
    650              >EQpost #EQ destruct
    651            ]
    652          | normalize nodelta %
    653            [ -REL cases(initial_is_initial … good … REL) #H #_ @H ] lapply(L_init_ok … t)
    654            >EQpre normalize nodelta * //
    655          | /6 by conj/
    656          ]
    657      | lapply(R_fin_ok … t) inversion(R_label … t) [ #_ normalize nodelta * #_ >EQpost #EQ destruct]
    658        #post_lab #EQpost_lab normalize nodelta *** #Hfin #Hpost_lab1 #Hpost_lab2 *
    659        #s2_post * >EQpost #EQ destruct(EQ) #exe cases(case_cl_io … (as_classify … s2_post))
    660        [ #Hio lapply(io_entering … Hio … exe) [ /3 by pre_meas, tail_of_premeasurable_is_not_io/ ]
    661          * #c #EQ destruct(EQ) cases(simulate_io_in … good … exe … REL) //
    662          [2: /3 by pre_meas, tail_of_premeasurable_is_not_io/] #x1 * #x2 * #t1 *
    663          ** #sil_t1 #exe' #Hx2 #REL1
    664          %{(mk_measurable_trace … (L_label … t) (Some ? (cost_act (Some ? c))) (None ?) … (Some ? x2) … (t'@t1) …)}
    665          [ normalize nodelta % [2: %{x2} % //] % [2: * #x3 * #x4 #EQ destruct] % [2: % %]
    666            @notb_Prop % #ABS @(as_final_ok … ABS exe')
    667          | normalize nodelta lapply(L_init_ok … t) >EQpre normalize nodelta * #H1 #H2 % [2: // ]
    668            -REL cases(initial_is_initial … good … REL) #H3 #_ @H3 assumption
    669          | /3 by append_silent_premeasurable/
    670          | % [2: % [ % #EQ destruct] whd in match (opt_safe ???); assumption] %
    671            [% // % // ] >get_cost_label_invariant_for_append_silent_trace_r assumption
    672          ]
    673        | (*go by cases on the instruction executed TODO *) cases daemon
    674        ]
    675     ]
    676 |*: cases daemon (*TODO*)
    677 ]
    678 qed.
    679 
    680 
    681 
    682 
    683 #L_label * [| #R_label] * [2,4: #pre_s1] #L_s1 #R_s2 * [2,4,6,8: #post_s2] #t #pre_meas_t
    684 normalize nodelta * [1,2,5,6: * ] #Hinitial [1,2,3,4: #Hcost #pre_exe |*: #EQ destruct(EQ) ]
    685 * [2,4,6,8: ** ] #Hfinal [5,6,7,8: #EQ destruct(EQ) |*:
    686 
    687 
    688 whd in ⊢ (% → ?);
    689 
    690 
    691 
    692 
    693 (*CSC: oppure fare il merge di L_raw_trace e measurable in un'unico record se
    694   non c'e' nulla di interessante sulle L_raw_trace non measurabili. Per esempio
    695   il teorema sotto sembra suggerire il merge *)
    696 
    697 definition unmovable_entry_label ≝
    698 λS : abstract_status.λl.
    699 match l with
    700 [ call_act _ _ ⇒ false
    701 | ret_act _ ⇒ false
    702 | cost_act x ⇒ match x with [Some c ⇒ is_io_exiting S c
    703                             | None ⇒ false
    704                             ]
    705 ].
    706  
    707 definition unmovable_exit_label ≝
    708 λS : abstract_status.λl.
    709 match l with
    710 [ call_act _ _ ⇒ false
    711 | ret_act _ ⇒ false
    712 | cost_act x ⇒ match x with [Some c ⇒ is_io_entering S c
    713                             | None ⇒ false
    714                             ]
    715 ].
    716 
    717 theorem simulates_LR_raw_trace :
    718 ∀S : abstract_status.
    719 ∀t : LR_raw_trace S.
    720 ∀rel : relations S.
    721 simulation_conditions … rel →
    722 measurable S t →
    723 ∀s1' : S.as_classify … s1' ≠ cl_io → Srel … rel (LR_s1 … t) s1' →
    724 ∃ t' : LR_raw_trace S.
    725 measurable S t' ∧
    726 if as_initial … (LR_s1 … t) ∨ unmovable_entry_label  S (L_label … t) then
    727    LR_s1 … t' = s1'
    728 else
    729    ∃pre : raw_trace … (LR_s1 … t') s1'.trace_prefix … pre (LR_t … t')
    730 ∧ ∃s1''.Srel … rel (LR_s2 … t) s1'' ∧
    731 if as_final … (LR_s2 … t) ∨ unmovable_exit_label S (R_label … t) then
    732    LR_s2 … t' = s1''
    733 else
    734   ∃suff : raw_trace … s1'' (LR_s2 … t'). trace_suffix … suff (LR_t … t')
    735 
    736 get_costlabels_of_trace … (LR_t … t) = get_costlabels_of_trace … (LR_t … t').
    737 #S #t #rel #good * #pre_t #wf_t #s1' #Hs1' #REL
    738 cases(simulates_pre_mesurable … (LR_t … t) … REL)
    739 [2: @good |3: @pre_t |4: @wf_t |5: @Hs1' ]
    740 #s2 * #t2 *** #pre_t2 #wf_t2 #EQcost #REL1
    741 inversion(as_initial … (LR_s1 … t)) #Has_initial
    742 inversion(unmovable_entry_label S (L_label … t)) #Hunmov_entry
    743 inversion(as_final … (LR_s2 … t)) #Has_final
    744 inversion(unmovable_exit_label S (R_label … t)) #Hunmov_exit
    745 normalize nodelta
    746 [ %{(mk_LR_raw_trace ? ?? s1' ? t2 ???)} [2: % [2:
    747 
    748 
    749 
    750 qed.
    751 
    752 xxxx
    753 
    754 theorem simulates_L_raw_trace:
    755  ∀t: L_raw_trace.
    756   pre_measurable_trace … (L_t t1) →
    757   well_formed_trace … (L_t t1) →
    758  ∀s1'.
    759    S (L_s1 t) s1' →
    760    s1' -flat-→ (L_s1 t2) →
    761    ∃s2',t2: L_raw_trace.
    762     pre_mesurable_trace … (L_t t2) ∧
    763     well_formed_trace … (L_t t2) ∧
    764     |t1| = |t2| ∧
    765     S (L_s2 t1) s2' ∧
    766     (L_s2 t2) -flat-→ s2'.
    767  (* o, nel caso in cui (L_label t1) e' unmovable_entry_label nessuna coda prefissa e
    768        nel caso in cui ??? e' unmovable_exit_label, nessuna coda suffissa *)
    769 
    770 
    771 (*********************************************************************)
    772 
    773 (* quello che segue tentava di permettere di evitare l'emissione di label
    774    associate a codice morto *)
    775 
    776 replace_last x : weak_trace → weak_trace
    777    [] ⇒ [], Some x
    778  | l::t ⇒
    779      let 〈t',x'〉 ≝ replace_last x t in
    780      match x' with
    781      [ None ⇒ l::t', None
    782      | Some x'' ⇒ [], Some x''
    783 
    784 theorem simulates:
    785  ∀s1,s2. ∀τ1: raw_trace … s1 s2.
    786   pre_measurable_trace … t1 →
    787   well_formed_trace … t1.
    788  ∀l1: option NonFunctionalLabel.
    789  ∀s1'.
    790    S s1 s1' →
    791    ∃dead_labels.
    792    ∃s2'. ∃t2: raw_trace … s1' s2'.
    793     pre_mesurable_trace … t2 ∧
    794     well_formed_trace … t2.
    795    ∃l2: option NonFunctionalLabel.
    796     match l1 with
    797     [ None ⇒
    798        match l2 with
    799        [ None ⇒ |t1| = |t2|
    800        | Some l2' ⇒ |t1| = l2'::|t2| ]
    801     | Some l1' ⇒
    802        match l2 with
    803        [ None ⇒ |t1| = replace_last l1' |t2| ∧ ends_with l1' t1
    804        | Some l2' ⇒
    805           if |t2| = [] then |t1| = [l1'] ∧ l2' = l1'
    806           else |t1| = l2' :: replace_last l1' |t2| ∧ ends_with l1' t1
    807        ]
    808     ]
    809     *)
     447*)
Note: See TracChangeset for help on using the changeset viewer.