Changeset 3484


Ignore:
Timestamp:
Sep 23, 2014, 1:58:43 PM (5 years ago)
Author:
sacerdot
Message:

Simulation generalized to two different abstract_status.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • LTS/Simulation.ma

    r3479 r3484  
    11include "Traces.ma".
    22
    3 record relations (S : abstract_status) : Type[0] ≝
    4  { Srel: S → S → Prop
    5  ; Crel: S → S → Prop
     3record relations (S1,S2 : abstract_status) : Type[0] ≝
     4 { Srel: S1 → S2 → Prop
     5 ; Crel: S1 → S2 → Prop
    66 }.
    77
    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 S s1' s'.
    10 
    11 record simulation_conditions (S : abstract_status) (rel : relations S) : Prop ≝
     8definition 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
     11record simulation_conditions (S1,S2 : abstract_status) (rel : relations S1 S2) : Prop ≝
    1212 { 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))
    1414 ; 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))
    1616 ; simulate_tau:
    17      ∀s1,s2,s1' : S.
     17     ∀s1:S1.∀s2:S2.∀s1':S1.
    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 S s2 s2'.
     20      ∃s2'. ∃t: raw_trace S2 s2 s2'.
    2121        Srel … rel s1' s2' ∧ silent_trace … t
    2222 ; 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' →
    2525      as_classify … s1 ≠ cl_io → as_classify … s1' ≠ cl_io →
    2626      Srel … rel s1 s2 →
    2727      ∃s2',s2'',s2'''.
    28        ∃t1: raw_trace S s2 s2'.
     28       ∃t1: raw_trace S2 s2 s2'.
    2929       as_execute … (cost_act (Some ? l)) s2' s2'' ∧
    30        ∃t3: raw_trace S s2'' s2'''.
     30       ∃t3: raw_trace s2'' s2'''.
    3131        Srel … rel  s1' s2''' ∧ silent_trace … t1 ∧ pre_silent_trace … t3
    3232 ; simulate_call_pl:
    33      ∀s1,s2,s1' : S.∀f,l.
     33     ∀s1:S1.∀s2:S2.∀s1':S1.∀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 S s2 s2'.
     39       ∃t1: raw_trace S2 s2 s2'.
    4040       as_execute … (call_act f l) s2' s2'' ∧
    4141       bool_to_Prop(is_call_post_label … s2') ∧
    42        ∃t3: raw_trace S s2'' s2'''.
     42       ∃t3: raw_trace S2 s2'' s2'''.
    4343        Srel … rel s1' s2''' ∧ silent_trace … t1 ∧ pre_silent_trace … t3
    4444 ; 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' →
    4747      as_classify … s1 ≠ cl_io → as_classify … s1' ≠ cl_io →
    4848      Srel  … rel s1 s2 →
    4949      ∃s2',s2'',s2'''.
    50        ∃t1: raw_trace S s2 s2'.
     50       ∃t1: raw_trace S2 s2 s2'.
    5151       as_execute … (ret_act (Some ? l)) s2' s2'' ∧
    52        ∃t3: raw_trace S s2'' s2'''.
     52       ∃t3: raw_trace S2 s2'' s2'''.
    5353        Srel … rel s1' s2''' ∧ silent_trace … t1 ∧ pre_silent_trace … t3
    5454 ; simulate_call_n:
    55      ∀s1,s2,s1' : S.∀f,l.
     55     ∀s1:S1.∀s2:S2.∀s1':S1.∀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 S s2 s2'.
     61       ∃t1: raw_trace S2 s2 s2'.
    6262       bool_to_Prop (¬ is_call_post_label … s2') ∧
    6363       as_execute … (call_act f l) s2' s2'' ∧
    64        ∃t3: raw_trace S s2'' s2'''.
     64       ∃t3: raw_trace S2 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,s2,s1' : S.
     68     ∀s1:S1.∀s2:S2.∀s1':S1.
    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'''.
    73        ∃t1: raw_trace S s2 s2'.
     72      ∃s2',s2'',s2''': S2.
     73       ∃t1: raw_trace S2 s2 s2'.
    7474       as_execute … (ret_act (None ?)) s2' s2''  ∧
    75        ∃t3: raw_trace S s2'' s2'''.
     75       ∃t3: raw_trace S2 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,s2,s1' : S.∀l.
     79   ∀s1:S1.∀s2:S2.∀s1':S1.∀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'' : S.∃t: raw_trace … s2 s2'.
     83   ∃s2',s2''.∃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,s2,s1' : S.∀l.
     87   ∀s1:S1.∀s2:S2.∀s1':S1.∀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'' : S.∃t : raw_trace … s2' s2''.
     91   ∃s2',s2''.∃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 
    264263theorem simulates_pre_mesurable:
    265  ∀S : abstract_status.∀rel : relations S.
    266  ∀s1,s1' : S. ∀t1: raw_trace S s1 s1'.
    267   simulation_conditions S rel →
     264 ∀S1,S2 : abstract_status.∀rel : relations S1 S2.
     265 ∀s1,s1' : S1. ∀t1: raw_trace S1 s1 s1'.
     266  simulation_conditions rel →
    268267  pre_measurable_trace … t1 →
    269   ∀s2 : S.
     268  ∀s2 : S2.
    270269 as_classify … s2 ≠ cl_io →   Srel … rel s1 s2 →
    271270  ∃s2'. ∃t2: raw_trace … s2 s2'.
     
    273272    get_costlabels_of_trace … t1 = get_costlabels_of_trace … t2 ∧
    274273    Srel … rel s1' s2'.
    275 #S #rel #s1 #s1' #t1 #good #pre_measurable elim pre_measurable
     274#S1 #S2 #rel #s1 #s1' #t1 #good #pre_measurable elim pre_measurable
    276275[ #st #H1 #s2 #REL #Hs2 %{s2} %{(t_base …)}
    277276  /8 by refl, silent_empty, conj, pre_silent_is_premeasurable/
     
    451450qed.
    452451
    453 lemma instr_execute_commute : ∀S :abstract_status.
    454 ∀rel : relations S.
     452lemma instr_execute_commute : ∀S1,S2 :abstract_status.
     453∀rel : relations S1 S2.
    455454simulation_conditions … rel →
    456 ∀s1,s1': S.∀l.l ≠ cost_act (None ?) →  as_execute S l s1 s1' →
     455∀s1,s1': S1.∀l.l ≠ cost_act (None ?) →  as_execute … l s1 s1' →
    457456(as_classify … s1 ≠ cl_io ∨ as_classify … s1' ≠ cl_io) →
    458457∀s2.
    459458Srel … rel s1 s2 →
    460 ∃s2' : S.∃tr : raw_trace S s2 s2'.silent_trace … tr ∧
    461 ∃s2'' : S.as_execute S l s2' s2'' ∧ ∃s2''' : S.
    462 ∃tr' : raw_trace S s2'' s2'''. silent_trace … tr' ∧ Srel … 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''' ∧
    463462(is_call_act l → is_call_post_label … s1 → is_call_post_label … s2') ∧
    464463(as_classify … s1' ≠ cl_io → as_classify … s2'' ≠ cl_io).
    465 #S #rel #good #s1 #s1' #l #l_notau #prf #HIO #s2 #REL cases(case_cl_io … (as_classify … s1))
     464#S1 #S2 #rel #good #s1 #s1' #l #l_notau #prf #HIO #s2 #REL cases(case_cl_io … (as_classify … s1))
    466465[ #EQs1_io cases(io_exiting … EQs1_io … prf) #lab #EQ destruct(EQ)
    467466  cases HIO [ >EQs1_io * #EQ @⊥ @EQ % ] #Hio_s1'
     
    514513qed.
    515514
    516 
    517515theorem simulate_LR_trace :
    518 ∀S : abstract_status.
    519 ∀t : measurable_trace S.
    520 ∀rel : relations S.
     516∀S1,S2 : abstract_status.
     517∀t : measurable_trace S1.
     518∀rel : relations S1 S2.
    521519simulation_conditions … rel →
    522 ∀s2 : S.
     520∀s2 : S2.
    523521match L_pre_state … t with
    524522[ None ⇒
     
    526524   Srel … rel (L_s1 … t) s2 
    527525| Some s1 ⇒ Srel … rel s1 s2 ] →
    528 ∃t' : measurable_trace S.
     526∃t' : measurable_trace S2.
    529527 L_label … t = L_label … t' ∧ R_label … t = R_label … t' ∧
    530528 get_costlabels_of_trace … (trace … t) =
     
    533531[ None ⇒ L_s1 … t' = s2
    534532| Some s1 ⇒
    535          ∃ pre_state : S.
     533         ∃ pre_state : S2.
    536534         L_pre_state … t' = Some ? pre_state ∧
    537          ∃tr_i : raw_trace S s2 pre_state. silent_trace … tr_i
     535         ∃tr_i : raw_trace s2 pre_state. silent_trace … tr_i
    538536] ∧
    539537match R_post_state … t with         
    540538[ None ⇒ Srel … rel (R_s2 … t) (R_s2 … t')
    541539| Some s1' ⇒
    542           ∃s2' : S. Srel … rel s1' s2' ∧
    543           ∃ post_state : S.
     540          ∃s2' : S2. Srel … rel s1' s2' ∧
     541          ∃ post_state : S2.
    544542          R_post_state … t' = Some ? post_state ∧
    545           ∃tr : raw_trace S post_state s2'. silent_trace … tr
     543          ∃tr : raw_trace post_state s2'. silent_trace … tr
    546544].
    547 #S #t #rel #good #s2 inversion(L_pre_state … t) [| #pre_s1] #EQpre normalize nodelta [* #Hclass_s2 ]
     545#S1 #S2 #t #rel #good #s2 inversion(L_pre_state … t) [| #pre_s1] #EQpre normalize nodelta [* #Hclass_s2 ]
    548546[2: #REL_pre
    549547    cut
    550      (∃pre_state: S.∃ l.
    551       ∃tr_i : raw_trace S s2 pre_state. silent_trace … tr_i ∧
    552       ∃middle_state: S.L_label … t = Some ? l ∧
     548     (∃pre_state.∃ l.
     549      ∃tr_i : raw_trace s2 pre_state. silent_trace … tr_i ∧
     550      ∃middle_state.L_label … t = Some ? l ∧
    553551       as_execute … l pre_state middle_state ∧
    554       ∃final_state: S.
    555       ∃tr_i2: raw_trace S middle_state final_state. silent_trace … tr_i2 ∧
     552      ∃final_state.
     553      ∃tr_i2: raw_trace middle_state final_state. silent_trace … tr_i2 ∧
    556554       as_classify … final_state ≠ cl_io ∧
    557555       Srel … rel (L_s1 … t) final_state)
     
    568566    * #final_state * #tr_i2 ** #silent_i2 #final_not_io #REL
    569567| #REL
    570   cut(bool_to_Prop (as_initial S s2)∧L_label S t=None ?)
     568  cut(bool_to_Prop (as_initial … s2)∧L_label … t=None ?)
    571569      [ lapply(L_init_ok … t) >EQpre normalize nodelta * #H1 #H2 % [2: //]
    572570        @(initial_is_initial … good … H1) assumption ] * #initial_s2 #init_label
     
    575573#fin_s2 * #t' ** #pre_meas_t' #EQcost #REL' inversion(R_post_state … t)
    576574[2,4: #post_s2] #EQpost normalize nodelta
    577 [3,4: cut (match R_label S t in option return λ_:(option ActionLabel).Prop with 
    578  [None⇒bool_to_Prop (as_final S fin_s2)∧None S=None S
     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
    579577 |Some (l:ActionLabel)⇒
    580578  (is_costlabelled_act l∨is_unlabelled_ret_act l)
    581   ∧(is_call_act l→is_call_post_label S fin_s2)
    582   ∧(∃s':S.None S=Some S s'∧as_execute S l fin_s2 s')])
     579  ∧(is_call_act l→is_call_post_label fin_s2)
     580  ∧(∃s'.None S2=Some … s'∧as_execute … l fin_s2 s')])
    583581  [1,3: lapply(R_fin_ok … t) cases(R_label … t) normalize nodelta
    584582      [1,3: * #H1 #H2 % [2,4: //] @(final_is_final … good … H1) assumption
     
    590588          #a #_ %{a} % ] * #final_label #EQfinal_label
    591589     cut
    592       (∃middle_state: S.
    593        ∃tr : raw_trace S fin_s2 middle_state. silent_trace … tr ∧
    594        ∃post_state : S.
     590      (∃middle_state.
     591       ∃tr : raw_trace fin_s2 middle_state. silent_trace … tr ∧
     592       ∃post_state.
    595593       as_execute … final_label middle_state post_state ∧
    596594       (is_call_act final_label → bool_to_Prop (is_call_post_label … middle_state)) ∧
    597        ∃final_state: S.
    598        ∃tr_f2: raw_trace S post_state final_state. silent_trace … tr_f2 ∧
     595       ∃final_state.
     596       ∃tr_f2: raw_trace post_state final_state. silent_trace … tr_f2 ∧
    599597       Srel … rel post_s2 final_state)
    600598     [1,3: lapply(R_fin_ok … t) >EQfinal_label normalize nodelta ** #H1 #H2 * #sfin
Note: See TracChangeset for help on using the changeset viewer.