Changeset 3486 for LTS/Simulation.ma


Ignore:
Timestamp:
Sep 24, 2014, 2:49:14 PM (5 years ago)
Author:
piccolo
Message:
 
File:
1 edited

Legend:

Unmodified
Added
Removed
  • LTS/Simulation.ma

    r3484 r3486  
    11include "Traces.ma".
    22
    3 record relations (S1,S2 : abstract_status) : Type[0] ≝
    4  { Srel: S1 → S2 → Prop
    5  ; Crel: S1 → S2 → Prop
     3record relations (S : abstract_status) : Type[0] ≝
     4 { Srel: S → S → Prop
     5 ; Crel: S → S → Prop
    66 }.
    77
    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 ≝
     8definition 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 S s1' s'.
     10
     11record simulation_conditions (S : abstract_status) (rel : relations S) : Prop ≝
    1212 { initial_is_initial :
    13    ∀s1,s2.Srel … rel s1 s2 → (bool_to_Prop (as_initial … s1) →  bool_to_Prop (as_initial … s2))
     13   ∀s1,s2 : S.Srel … rel s1 s2 → (bool_to_Prop (as_initial … s1) →  bool_to_Prop (as_initial … s2))
    1414 ; final_is_final :
    15    ∀s1,s2.Srel … rel s1 s2 → (bool_to_Prop(as_final … s1) → bool_to_Prop (as_final … s2))
     15   ∀s1,s2 : S.Srel … rel s1 s2 → (bool_to_Prop(as_final … s1) → bool_to_Prop (as_final … s2))
    1616 ; simulate_tau:
    17      ∀s1:S1.∀s2:S2.∀s1':S1.
     17     ∀s1,s2,s1' : S.
    1818      as_execute … (cost_act (None ?))  s1 s1'→
    1919      Srel … rel s1 s2 → as_classify … s1 ≠ cl_io → as_classify … s1' ≠ cl_io →
    20       ∃s2'. ∃t: raw_trace S2 s2 s2'.
     20      ∃s2'. ∃t: raw_trace S s2 s2'.
    2121        Srel … rel s1' s2' ∧ silent_trace … t
    2222 ; simulate_label:
    23      ∀s1:S1.∀s2:S2.∀l.∀s1':S1.
    24       as_execute S1 (cost_act (Some ? l)) s1 s1' →
     23     ∀s1,s2,l,s1'.
     24      as_execute S (cost_act (Some ? l)) s1 s1' →
    2525      as_classify … s1 ≠ cl_io → as_classify … s1' ≠ cl_io →
    2626      Srel … rel s1 s2 →
    2727      ∃s2',s2'',s2'''.
    28        ∃t1: raw_trace S2 s2 s2'.
     28       ∃t1: raw_trace S s2 s2'.
    2929       as_execute … (cost_act (Some ? l)) s2' s2'' ∧
    30        ∃t3: raw_trace s2'' s2'''.
     30       ∃t3: raw_trace S s2'' s2'''.
    3131        Srel … rel  s1' s2''' ∧ silent_trace … t1 ∧ pre_silent_trace … t3
    3232 ; simulate_call_pl:
    33      ∀s1:S1.∀s2:S2.∀s1':S1.∀f,l.
     33     ∀s1,s2,s1' : S.∀f,l.
    3434      is_call_post_label … s1 →
    3535      as_execute … (call_act f l) s1 s1' →
     
    3737      Srel … rel s1 s2 →
    3838      ∃s2',s2'',s2'''.
    39        ∃t1: raw_trace S2 s2 s2'.
     39       ∃t1: raw_trace S s2 s2'.
    4040       as_execute … (call_act f l) s2' s2'' ∧
    4141       bool_to_Prop(is_call_post_label … s2') ∧
    42        ∃t3: raw_trace S2 s2'' s2'''.
     42       ∃t3: raw_trace S s2'' s2'''.
    4343        Srel … rel s1' s2''' ∧ silent_trace … t1 ∧ pre_silent_trace … t3
    4444 ; simulate_ret_l:
    45      ∀s1:S1.∀s2:S2.∀s1':S1.∀l.
    46       as_execute S1 (ret_act (Some ? l)) s1 s1' →
     45     ∀s1,s2,s1' : S.∀l.
     46      as_execute S (ret_act (Some ? l)) s1 s1' →
    4747      as_classify … s1 ≠ cl_io → as_classify … s1' ≠ cl_io →
    4848      Srel  … rel s1 s2 →
    4949      ∃s2',s2'',s2'''.
    50        ∃t1: raw_trace S2 s2 s2'.
     50       ∃t1: raw_trace S s2 s2'.
    5151       as_execute … (ret_act (Some ? l)) s2' s2'' ∧
    52        ∃t3: raw_trace S2 s2'' s2'''.
     52       ∃t3: raw_trace S s2'' s2'''.
    5353        Srel … rel s1' s2''' ∧ silent_trace … t1 ∧ pre_silent_trace … t3
    5454 ; simulate_call_n:
    55      ∀s1:S1.∀s2:S2.∀s1':S1.∀f,l.
     55     ∀s1,s2,s1' : S.∀f,l.
    5656      as_execute … (call_act f l) s1 s1' →
    5757      ¬ is_call_post_label … s1 →
     
    5959      Srel … rel s1 s2 →
    6060      ∃s2',s2'',s2'''.
    61        ∃t1: raw_trace S2 s2 s2'.
     61       ∃t1: raw_trace S s2 s2'.
    6262       bool_to_Prop (¬ is_call_post_label … s2') ∧
    6363       as_execute … (call_act f l) s2' s2'' ∧
    64        ∃t3: raw_trace S2 s2'' s2'''.
     64       ∃t3: raw_trace S s2'' s2'''.
    6565        Srel … rel s1' s2''' ∧ silent_trace … t1 ∧ pre_silent_trace … t3
    6666        ∧ Crel … rel s1 s2'
    6767 ; simulate_ret_n:
    68      ∀s1:S1.∀s2:S2.∀s1':S1.
     68     ∀s1,s2,s1' : S.
    6969      as_execute … (ret_act (None ?)) s1 s1' →
    7070      as_classify … s1 ≠ cl_io → as_classify … s1' ≠ cl_io →
    7171      Srel … rel s1 s2 →
    72       ∃s2',s2'',s2''': S2.
    73        ∃t1: raw_trace S2 s2 s2'.
     72      ∃s2',s2'',s2'''.
     73       ∃t1: raw_trace S s2 s2'.
    7474       as_execute … (ret_act (None ?)) s2' s2''  ∧
    75        ∃t3: raw_trace S2 s2'' s2'''.
     75       ∃t3: raw_trace S s2'' s2'''.
    7676        Srel … rel s1' s2''' ∧ pre_silent_trace … t1 ∧ pre_silent_trace … t3
    7777        ∧ Rrel … rel s1' s2''
    7878 ; simulate_io_in :
    79    ∀s1:S1.∀s2:S2.∀s1':S1.∀l.
     79   ∀s1,s2,s1' : S.∀l.
    8080   as_execute … (cost_act … (Some ? l)) s1 s1' →
    8181   as_classify … s1 ≠ cl_io → as_classify … s1' = cl_io →
    8282   Srel … rel s1 s2 →
    83    ∃s2',s2''.∃t: raw_trace … s2 s2'.
     83   ∃s2',s2'' : S.∃t: raw_trace … s2 s2'.
    8484   pre_silent_trace … t ∧ as_execute … (cost_act … (Some ? l)) s2' s2'' ∧
    8585   as_classify … s2'' = cl_io ∧ Srel … rel s1' s2''
    8686; simulate_io_out :
    87    ∀s1:S1.∀s2:S2.∀s1':S1.∀l.
     87  ∀s1,s2,s1' : S.∀l.
    8888   as_execute … (cost_act … (Some ? l)) s1 s1' →
    8989   as_classify … s1 = cl_io → as_classify … s1' ≠ cl_io →
    9090   Srel … rel s1 s2 →
    91    ∃s2',s2''.∃t : raw_trace … s2' s2''.
     91   ∃s2',s2'' : S.∃t : raw_trace … s2' s2''.
    9292   pre_silent_trace … t ∧ as_execute … (cost_act … (Some ? l)) s2 s2' ∧
    9393   as_classify … s2 = cl_io ∧ Srel … rel s1' s2''
     
    261261qed.
    262262
     263
    263264theorem simulates_pre_mesurable:
    264  ∀S1,S2 : abstract_status.∀rel : relations S1 S2.
    265  ∀s1,s1' : S1. ∀t1: raw_trace S1 s1 s1'.
    266   simulation_conditions rel →
     265 ∀S : abstract_status.∀rel : relations S.
     266 ∀s1,s1' : S. ∀t1: raw_trace S s1 s1'.
     267  simulation_conditions S rel →
    267268  pre_measurable_trace … t1 →
    268   ∀s2 : S2.
     269  ∀s2 : S.
    269270 as_classify … s2 ≠ cl_io →   Srel … rel s1 s2 →
    270271  ∃s2'. ∃t2: raw_trace … s2 s2'.
     
    272273    get_costlabels_of_trace … t1 = get_costlabels_of_trace … t2 ∧
    273274    Srel … rel s1' s2'.
    274 #S1 #S2 #rel #s1 #s1' #t1 #good #pre_measurable elim pre_measurable
     275#S #rel #s1 #s1' #t1 #good #pre_measurable elim pre_measurable
    275276[ #st #H1 #s2 #REL #Hs2 %{s2} %{(t_base …)}
    276277  /8 by refl, silent_empty, conj, pre_silent_is_premeasurable/
     
    401402
    402403record measurable_trace (S : abstract_status) : Type[0] ≝
    403  { L_label: option ActionLabel
    404  ; R_label : option ActionLabel
    405  ; L_pre_state : option S
    406  ; L_s1 : S
     404 { L_s1 : S
    407405 ; R_s2: S
    408  ; R_post_state : option S
    409406 ; trace : raw_trace S L_s1 R_s2
    410407 ; pre_meas : pre_measurable_trace … trace
    411  ; L_init_ok : match L_pre_state with
    412                [ None ⇒ bool_to_Prop(as_initial … L_s1) ∧ L_label = None ?
    413                | Some s ⇒ ∃l. L_label = Some ? l ∧ is_costlabelled_act l ∧
    414                           as_execute … l s L_s1
    415                ]
    416  ; R_fin_ok : match R_label with
    417                [ None ⇒ bool_to_Prop (as_final … R_s2) ∧ R_post_state = None ?
    418                | Some l ⇒ (is_costlabelled_act l ∨ is_unlabelled_ret_act l) ∧
    419                           (is_call_act l → bool_to_Prop (is_call_post_label … R_s2)) ∧
    420                           ∃ s'.R_post_state = Some ? s' ∧ as_execute … l R_s2 s'
    421                ]
    422 }.
     408 }.
    423409
    424410lemma cl_io_case : ∀P : status_class → Prop. P cl_io → (∀x.x≠cl_io → P x) → ∀s.P s.
     
    450436qed.
    451437
    452 lemma instr_execute_commute : ∀S1,S2 :abstract_status.
    453 ∀rel : relations S1 S2.
     438lemma instr_execute_commute : ∀S :abstract_status.
     439∀rel : relations S.
    454440simulation_conditions … rel →
    455 ∀s1,s1': S1.∀l.l ≠ cost_act (None ?) →  as_execute … l s1 s1' →
     441∀s1,s1': S.∀l.l ≠ cost_act (None ?) →  as_execute S l s1 s1' →
    456442(as_classify … s1 ≠ cl_io ∨ as_classify … s1' ≠ cl_io) →
    457443∀s2.
    458444Srel … rel s1 s2 →
    459 ∃s2' : S2.∃tr : raw_trace … s2 s2'.silent_trace … tr ∧
    460 ∃s2'' : S2.as_execute … l s2' s2'' ∧ ∃s2''' : S2.
    461 ∃tr' : raw_trace s2'' s2'''. silent_trace … tr' ∧ Srel … rel s1' s2''' ∧
     445∃s2' : S.∃tr : raw_trace S s2 s2'.silent_trace … tr ∧
     446∃s2'' : S.as_execute S l s2' s2'' ∧ ∃s2''' : S.
     447∃tr' : raw_trace S s2'' s2'''. silent_trace … tr' ∧ Srel … rel s1' s2''' ∧
    462448(is_call_act l → is_call_post_label … s1 → is_call_post_label … s2') ∧
    463449(as_classify … s1' ≠ cl_io → as_classify … s2'' ≠ cl_io).
    464 #S1 #S2 #rel #good #s1 #s1' #l #l_notau #prf #HIO #s2 #REL cases(case_cl_io … (as_classify … s1))
     450#S #rel #good #s1 #s1' #l #l_notau #prf #HIO #s2 #REL cases(case_cl_io … (as_classify … s1))
    465451[ #EQs1_io cases(io_exiting … EQs1_io … prf) #lab #EQ destruct(EQ)
    466452  cases HIO [ >EQs1_io * #EQ @⊥ @EQ % ] #Hio_s1'
     
    513499qed.
    514500
     501(*
    515502theorem simulate_LR_trace :
    516 ∀S1,S2 : abstract_status.
    517 ∀t : measurable_trace S1.
    518 ∀rel : relations S1 S2.
     503∀S : abstract_status.
     504∀t : measurable_trace S.
     505∀rel : relations S.
    519506simulation_conditions … rel →
    520 ∀s2 : S2.
     507∀s2 : S.
    521508match L_pre_state … t with
    522509[ None ⇒
     
    524511   Srel … rel (L_s1 … t) s2 
    525512| Some s1 ⇒ Srel … rel s1 s2 ] →
    526 ∃t' : measurable_trace S2.
     513∃t' : measurable_trace S.
    527514 L_label … t = L_label … t' ∧ R_label … t = R_label … t' ∧
    528515 get_costlabels_of_trace … (trace … t) =
     
    531518[ None ⇒ L_s1 … t' = s2
    532519| Some s1 ⇒
    533          ∃ pre_state : S2.
     520         ∃ pre_state : S.
    534521         L_pre_state … t' = Some ? pre_state ∧
    535          ∃tr_i : raw_trace s2 pre_state. silent_trace … tr_i
     522         ∃tr_i : raw_trace S s2 pre_state. silent_trace … tr_i
    536523] ∧
    537524match R_post_state … t with         
    538525[ None ⇒ Srel … rel (R_s2 … t) (R_s2 … t')
    539526| Some s1' ⇒
    540           ∃s2' : S2. Srel … rel s1' s2' ∧
    541           ∃ post_state : S2.
     527          ∃s2' : S. Srel … rel s1' s2' ∧
     528          ∃ post_state : S.
    542529          R_post_state … t' = Some ? post_state ∧
    543           ∃tr : raw_trace post_state s2'. silent_trace … tr
     530          ∃tr : raw_trace S post_state s2'. silent_trace … tr
    544531].
    545 #S1 #S2 #t #rel #good #s2 inversion(L_pre_state … t) [| #pre_s1] #EQpre normalize nodelta [* #Hclass_s2 ]
     532#S #t #rel #good #s2 inversion(L_pre_state … t) [| #pre_s1] #EQpre normalize nodelta [* #Hclass_s2 ]
    546533[2: #REL_pre
    547534    cut
    548      (∃pre_state.∃ l.
    549       ∃tr_i : raw_trace s2 pre_state. silent_trace … tr_i ∧
    550       ∃middle_state.L_label … t = Some ? l ∧
     535     (∃pre_state: S.∃ l.
     536      ∃tr_i : raw_trace S s2 pre_state. silent_trace … tr_i ∧
     537      ∃middle_state: S.L_label … t = Some ? l ∧
    551538       as_execute … l pre_state middle_state ∧
    552       ∃final_state.
    553       ∃tr_i2: raw_trace middle_state final_state. silent_trace … tr_i2 ∧
     539      ∃final_state: S.
     540      ∃tr_i2: raw_trace S middle_state final_state. silent_trace … tr_i2 ∧
    554541       as_classify … final_state ≠ cl_io ∧
    555542       Srel … rel (L_s1 … t) final_state)
     
    566553    * #final_state * #tr_i2 ** #silent_i2 #final_not_io #REL
    567554| #REL
    568   cut(bool_to_Prop (as_initial … s2)∧L_label … t=None ?)
     555  cut(bool_to_Prop (as_initial S s2)∧L_label S t=None ?)
    569556      [ lapply(L_init_ok … t) >EQpre normalize nodelta * #H1 #H2 % [2: //]
    570557        @(initial_is_initial … good … H1) assumption ] * #initial_s2 #init_label
     
    573560#fin_s2 * #t' ** #pre_meas_t' #EQcost #REL' inversion(R_post_state … t)
    574561[2,4: #post_s2] #EQpost normalize nodelta
    575 [3,4: cut (match R_label t in option return λ_:(option ActionLabel).Prop with 
    576  [None⇒bool_to_Prop (as_final … fin_s2)∧None S2=None S2
     562[3,4: cut (match R_label S t in option return λ_:(option ActionLabel).Prop with 
     563 [None⇒bool_to_Prop (as_final S fin_s2)∧None S=None S
    577564 |Some (l:ActionLabel)⇒
    578565  (is_costlabelled_act l∨is_unlabelled_ret_act l)
    579   ∧(is_call_act l→is_call_post_label fin_s2)
    580   ∧(∃s'.None S2=Some … s'∧as_execute … l fin_s2 s')])
     566  ∧(is_call_act l→is_call_post_label S fin_s2)
     567  ∧(∃s':S.None S=Some S s'∧as_execute S l fin_s2 s')])
    581568  [1,3: lapply(R_fin_ok … t) cases(R_label … t) normalize nodelta
    582569      [1,3: * #H1 #H2 % [2,4: //] @(final_is_final … good … H1) assumption
     
    588575          #a #_ %{a} % ] * #final_label #EQfinal_label
    589576     cut
    590       (∃middle_state.
    591        ∃tr : raw_trace fin_s2 middle_state. silent_trace … tr ∧
    592        ∃post_state.
     577      (∃middle_state: S.
     578       ∃tr : raw_trace S fin_s2 middle_state. silent_trace … tr ∧
     579       ∃post_state : S.
    593580       as_execute … final_label middle_state post_state ∧
    594581       (is_call_act final_label → bool_to_Prop (is_call_post_label … middle_state)) ∧
    595        ∃final_state.
    596        ∃tr_f2: raw_trace post_state final_state. silent_trace … tr_f2 ∧
     582       ∃final_state: S.
     583       ∃tr_f2: raw_trace S post_state final_state. silent_trace … tr_f2 ∧
    597584       Srel … rel post_s2 final_state)
    598585     [1,3: lapply(R_fin_ok … t) >EQfinal_label normalize nodelta ** #H1 #H2 * #sfin
     
    846833    ]
    847834    *)
     835*)
Note: See TracChangeset for help on using the changeset viewer.