Changeset 3504 for LTS/Simulation.ma


Ignore:
Timestamp:
Sep 26, 2014, 3:44:01 PM (5 years ago)
Author:
sacerdot
Message:

Last commit destroyed my changes: undone.

File:
1 edited

Legend:

Unmodified
Added
Removed

  • LTS/Simulation.ma

    r3486 r3504  
    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''
    9494 }.
    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 with
    99 [ t_base st ⇒ [ ]
    100 | t_ind st1' st2' st3' l prf t' ⇒
    101     let tl ≝ get_costlabels_of_trace … t' in
    102     match l with
    103     [ call_act f c ⇒ [ c ]
    104     | ret_act x ⇒ match x with
    105                   [ Some c ⇒ [ a_return_post c ]
    106                   | None ⇒ []
    107                   ]
    108     | cost_act x ⇒ match x with
    109                   [ Some c ⇒ [ a_non_functional_label c ]
    110                   | None ⇒ []
    111                   ]
    112 
    113    ] @ tl
    114 ].
    115 
    11695
    11796lemma append_premeasurable_silent : ∀S : abstract_status.
    … …  
    235214qed.
    236215
    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 @IH
    243 qed.
    244  
    245216(*
    246217lemma raw_trace_ind_r : ∀S : abstract_status.
    … …  
    261232qed.
    262233
    263 
    264234theorem 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 →
     235 ∀S1,S2 : abstract_status.∀rel : relations S1 S2.
     236 ∀s1,s1' : S1. ∀t1: raw_trace S1 s1 s1'.
     237  simulation_conditions … rel →
    268238  pre_measurable_trace … t1 →
    269   ∀s2 : S.
     239  ∀s2 : S2.
    270240 as_classify … s2 ≠ cl_io →   Srel … rel s1 s2 →
    271241  ∃s2'. ∃t2: raw_trace … s2 s2'.
    … …  
    273243    get_costlabels_of_trace … t1 = get_costlabels_of_trace … t2 ∧
    274244    Srel … rel s1' s2'.
    275 #S #rel #s1 #s1' #t1 #good #pre_measurable elim pre_measurable
     245#S1 #S2 #rel #s1 #s1' #t1 #good #pre_measurable elim pre_measurable
    276246[ #st #H1 #s2 #REL #Hs2 %{s2} %{(t_base …)}
    277247  /8 by refl, silent_empty, conj, pre_silent_is_premeasurable/
    … …  
    388358qed.
    389359
    390 
    391360(* IDEA: aggiungere stati di I/O e cambiare la semantica del linguaggio
    392361   sorgente; aggiungere nella pre_measurable il vincolo nessuno stato e' di I/O;
    393362   cambiare la definizione di traccia tornando a una sola etichetta sugli archi *)
    394 
     363(*
    395364(* measurable fattorizzata sotto come measurable'
    396365definition measurable ≝
    … …  
    402371
    403372record 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
    405377 ; R_s2: S
     378 ; R_post_state : option S
    406379 ; trace : raw_trace S L_s1 R_s2
    407380 ; 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}.
    409393
    410394lemma cl_io_case : ∀P : status_class → Prop. P cl_io → (∀x.x≠cl_io → P x) → ∀s.P s.
    … …  
    418402as_classify … st2 ≠ cl_io.
    419403#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 H
    426 [#s #cl #EQ1 #EQ2 #EQ3 destruct] #s1' #s2' #s3' #prf' #tl' #cl' #Htl #_ #EQ1 #EQ2 #EQ3
    427 destruct #_ @IH % assumption
    428404qed.
    429405
    … …  
    436412qed.
    437413
    438 lemma instr_execute_commute : ∀S :abstract_status.
    439 ∀rel : relations S.
     414lemma instr_execute_commute : ∀S1,S2 :abstract_status.
     415∀rel : relations S1 S2.
    440416simulation_conditions … rel →
    441 ∀s1,s1': S.∀l.l ≠ cost_act (None ?) →  as_execute S l s1 s1' →
     417∀s1,s1': S1.∀l.l ≠ cost_act (None ?) →  as_execute … l s1 s1' →
    442418(as_classify … s1 ≠ cl_io ∨ as_classify … s1' ≠ cl_io) →
    443419∀s2.
    444420Srel … 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''' ∧
     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''' ∧
    448424(is_call_act l → is_call_post_label … s1 → is_call_post_label … s2') ∧
    449425(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))
    451427[ #EQs1_io cases(io_exiting … EQs1_io … prf) #lab #EQ destruct(EQ)
    452428  cases HIO [ >EQs1_io * #EQ @⊥ @EQ % ] #Hio_s1'
    … …  
    499475qed.
    500476
    501 (*
    502477theorem 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.
    506481simulation_conditions … rel →
    507 ∀s2 : S.
     482∀s2 : S2.
    508483match L_pre_state … t with
    509484[ None ⇒
    … …  
    511486   Srel … rel (L_s1 … t) s2 
    512487| Some s1 ⇒ Srel … rel s1 s2 ] →
    513 ∃t' : measurable_trace S.
     488∃t' : measurable_trace S2.
    514489 L_label … t = L_label … t' ∧ R_label … t = R_label … t' ∧
    515490 get_costlabels_of_trace … (trace … t) =
    … …  
    518493[ None ⇒ L_s1 … t' = s2
    519494| Some s1 ⇒
    520          ∃ pre_state : S.
     495         ∃ pre_state : S2.
    521496         L_pre_state … t' = Some ? pre_state ∧
    522          ∃tr_i : raw_trace S s2 pre_state. silent_trace … tr_i
     497         ∃tr_i : raw_trace … s2 pre_state. silent_trace … tr_i
    523498] ∧
    524499match R_post_state … t with         
    525500[ None ⇒ Srel … rel (R_s2 … t) (R_s2 … t')
    526501| Some s1' ⇒
    527           ∃s2' : S. Srel … rel s1' s2' ∧
    528           ∃ post_state : S.
     502          ∃s2' : S2. Srel … rel s1' s2' ∧
     503          ∃ post_state : S2.
    529504          R_post_state … t' = Some ? post_state ∧
    530           ∃tr : raw_trace S post_state s2'. silent_trace … tr
     505          ∃tr : raw_trace … post_state s2'. silent_trace … tr
    531506].
    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 ]
    533508[2: #REL_pre
    534509    cut
    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 ∧
     510     (∃pre_state.∃ l.
     511      ∃tr_i : raw_trace … s2 pre_state. silent_trace … tr_i ∧
     512      ∃middle_state.L_label … t = Some ? l ∧
    538513       as_execute … l pre_state middle_state ∧
    539       ∃final_state: S.
    540       ∃tr_i2: raw_trace S middle_state final_state. silent_trace … tr_i2 ∧
     514      ∃final_state.
     515      ∃tr_i2: raw_trace … middle_state final_state. silent_trace … tr_i2 ∧
    541516       as_classify … final_state ≠ cl_io ∧
    542517       Srel … rel (L_s1 … t) final_state)
    … …  
    553528    * #final_state * #tr_i2 ** #silent_i2 #final_not_io #REL
    554529| #REL
    555   cut(bool_to_Prop (as_initial S s2)∧L_label S t=None ?)
     530  cut(bool_to_Prop (as_initial … s2)∧L_label … t=None ?)
    556531      [ lapply(L_init_ok … t) >EQpre normalize nodelta * #H1 #H2 % [2: //]
    557532        @(initial_is_initial … good … H1) assumption ] * #initial_s2 #init_label
    … …  
    560535#fin_s2 * #t' ** #pre_meas_t' #EQcost #REL' inversion(R_post_state … t)
    561536[2,4: #post_s2] #EQpost normalize nodelta
    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
     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
    564539 |Some (l:ActionLabel)⇒
    565540  (is_costlabelled_act l∨is_unlabelled_ret_act l)
    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')])
     541  ∧(is_call_act l→is_call_post_label … fin_s2)
     542  ∧(∃s'.None S2=Some … s'∧as_execute … l fin_s2 s')])
    568543  [1,3: lapply(R_fin_ok … t) cases(R_label … t) normalize nodelta
    569544      [1,3: * #H1 #H2 % [2,4: //] @(final_is_final … good … H1) assumption
    … …  
    575550          #a #_ %{a} % ] * #final_label #EQfinal_label
    576551     cut
    577       (∃middle_state: S.
    578        ∃tr : raw_trace S fin_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.
    580555       as_execute … final_label middle_state post_state ∧
    581556       (is_call_act final_label → bool_to_Prop (is_call_post_label … middle_state)) ∧
    582        ∃final_state: S.
    583        ∃tr_f2: raw_trace S post_state final_state. silent_trace … tr_f2 ∧
     557       ∃final_state.
     558       ∃tr_f2: raw_trace … post_state final_state. silent_trace … tr_f2 ∧
    584559       Srel … rel post_s2 final_state)
    585560     [1,3: lapply(R_fin_ok … t) >EQfinal_label normalize nodelta ** #H1 #H2 * #sfin
    … …  
    833808    ]
    834809    *)
    835 *)
Note: See TracChangeset for help on using the changeset viewer.