Changeset 3531 for LTS/Simulation.ma


Ignore:
Timestamp:
Mar 13, 2015, 6:42:58 PM (5 years ago)
Author:
piccolo
Message:

new notion of measurable: some lemmas are still broken

File:
1 edited

Legend:

Unmodified
Added
Removed
  • LTS/Simulation.ma

    r3524 r3531  
    1717 ; final_is_final :
    1818   ∀s1,s2.Srel … rel s1 s2 → (bool_to_Prop(as_final … s1) → bool_to_Prop (as_final … s2))
     19 ; io_is_io :
     20   ∀s1,s2.Srel … rel s1 s2 → as_classify … s2 = cl_io → as_classify … s1 = cl_io
    1921 ; simulate_tau:
    2022     ∀s1:S1.∀s2:S2.∀s1':S1.
     
    9698   as_classify … s2 = cl_io ∧ Srel … rel s1' s2''
    9799 }.
     100 
     101lemma io_state_case : ∀P : status_class → Prop.∀s.
     102(s = cl_io → P s) → (s ≠ cl_io → P s) → P s.
     103#P * #H1 #H2 [2: @H1 %] @H2 % #EQ destruct
     104qed.
     105
     106lemma simulate_labelled_action : ∀S1,S2 : abstract_status.
     107∀rel : relations S1 S2.
     108∀s1,s2 : S1.∀s1' : S2.
     109∀l : ActionLabel.
     110simulation_conditions … rel →
     111is_costlabelled_act l →
     112(is_call_act l → is_call_post_label … s1) →
     113as_execute … l s1 s2 →
     114Srel … rel s1 s1' →
     115¬ (as_classify … s1 = cl_io ∧ as_classify … s2 = cl_io) →
     116∃pre_em,post_em,s2' : S2.
     117∃t_pre : raw_trace … s1' pre_em.
     118∃t_post : raw_trace … post_em s2'.
     119silent_trace … t_pre ∧ silent_trace … t_post ∧
     120as_execute … l pre_em post_em ∧
     121(is_call_act l → is_call_post_label … pre_em) ∧
     122Srel … rel s2 s2'.
     123#S1 #S2 #rel #s1 #s2 #s1' *
     124[ #f #c | * [|#lbl] | * [|#lbl]]
     125#sim * #Hcall #prf #REL * #Hio
     126[ cases(simulate_call_pl … sim … prf … REL)
     127  [2: @Hcall %{f} %{c} %
     128  |3: % #ABS lapply(io_exiting … S1 … ABS … prf) * #lbl #EQ destruct
     129  |4: % #ABS lapply(io_entering … S1 … ABS … prf) * #lbl #EQ destruct
     130  ]
     131  #pre_em * #post_em * #s2' * #t_pre ** #prf' #call * #t_post ** #REL' #sil_tpre #sil_tpost
     132  %{pre_em} %{post_em} %{s2'} %{t_pre} %{t_post} % // % // % // % // %1 //
     133| cases(simulate_ret_l … sim … prf … REL)
     134  [2: % #ABS lapply(io_exiting … S1 … ABS … prf) * #lbl #EQ destruct
     135  |3: % #ABS lapply(io_entering … S1 … ABS … prf) * #lbl #EQ destruct
     136  ]
     137  #pre_em * #post_em * #s2' * #t_pre * #prf' * #t_post ** #REL' #sil_tpre #sil_tpost
     138  %{pre_em} %{post_em} %{s2'} %{t_pre} %{t_post} % // % [2: * #f * #c #EQ destruct]
     139  % // % // %1 //
     140| @(io_state_case … (as_classify … s1)) @(io_state_case … (as_classify … s2))
     141  #class_s2 #class_s1
     142  [ cases(Hio ?) /2/
     143  | cases(simulate_io_out … sim … prf … REL) //
     144    #post_em * #s2' * #t_post *** #sil_tpost #prf' #Hclass #REL'
     145    %{s1'} %{post_em} %{s2'} %{(t_base …)} %{t_post} % // % [2: * #f * #c #EQ destruct]
     146    % // % [%2 %*] % assumption
     147  | cases(simulate_io_in … sim … prf … REL) //
     148    #pre_em * #s2' * #t_pre *** #sil_tpre #prf' #Hclass #REL'
     149    %{pre_em} %{s2'} %{s2'} %{t_pre} %{(t_base …)} % // % [2: * #f * #c #EQ destruct]
     150    % // % [% assumption]  %2 % *
     151  | cases(simulate_label … sim … prf … REL) //
     152    #pre_em * #post_em * #s2' * #t_pre * #prf' * #t_post ** #REL' #sil_tpre #sil_tpost
     153    %{pre_em} %{post_em} %{s2'} %{t_pre} %{t_post} % // % [2: * #f * #c #EQ destruct]
     154    % // % // %1 //
     155  ]
     156]
     157qed. 
     158   
     159 
     160 
     161(* silente simula in silente *)
    98162
    99163
     
    339403qed.
    340404
     405lemma silent_in_silent : ∀S1,S2 : abstract_status.∀rel : relations S1 S2.
     406 ∀s1,s1' : S1. ∀t1: raw_trace S1 s1 s1'.
     407  simulation_conditions … rel →
     408  ∀s2 : S2.Srel … rel s1 s2 →
     409  silent_trace … t1 →
     410  ∃s2'. ∃t2: raw_trace … s2 s2'.
     411    silent_trace … t2 ∧
     412    Srel … rel s1' s2'.
     413#S1 #S2 #rel #s1 #s1' #t1 #sim #s2 #REL *
     414[ #pre_sil_ti0 cases(simulates_pre_mesurable … sim … (pre_silent_is_premeasurable … pre_sil_ti0) … REL)
     415  [2: % #H
     416      lapply(head_of_premeasurable_is_not_io … (pre_silent_is_premeasurable … pre_sil_ti0))
     417      >(io_is_io … sim … H) // * /2/
     418  ]
     419  #s2' * #t2 *** * #H1 #H2 #H3 #H4 #H5 %{s2'} %{t2} % /3 by or_introl/
     420| cases t1 in REL; [ #st #H #_ %{s2} %{(t_base …)} % [%2 % * ] // ]
     421  #H7 #H8 #H9 #H10 #H11 #H12 #H13 #H14 cases H14 #H cases(H I)
     422]
     423qed.
     424
     425lemma tail_of_premeasurable_is_not_io : ∀S : abstract_status.
     426∀s1,s2 : S.∀t : raw_trace … s1 s2.
     427pre_measurable_trace … t →
     428as_classify … s2 ≠ cl_io.
     429#S #s1 #s2 #t #H elim H //
     430qed.
     431
    341432theorem simulates_measurable:
    342433 ∀S1,S2: abstract_status.
     
    348439 ∀s1,s2. measurable … s1 s2 … t →
    349440 
    350  ∀si': S2. as_classify … si' ≠ cl_io →
     441 ∀si': S2.
     442 (as_classify … si' = cl_io →  as_classify … si = cl_io) → 
    351443 
    352444 Srel … rel si si' →
     
    359451 
    360452 ∃s1',s2'. measurable … s1' s2' … t'.
    361 #S1 #S2 #rel #sim_rel #si #sn #t #s1 #s2 #Hmeas #s1' #Hclass #Rsi_si'
    362 cases(simulates_pre_mesurable … rel … t … Rsi_si') //
    363 [2: cases Hmeas //] #sn' * #t2 **** #pre_meas_t2 #EQcost #R_sn_sn'
    364 #Hmeas1 #_ %{sn'} %{t2} % [% //] @(measurable_suffix_is_measurable … t2) /4 by measurable_is_measurable_suffix/
    365 <EQcost cases Hmeas #_ * #s1 * #s2 * #t_pre * #t_mid * #t_last * #l1 * #l2 * #prf1 * #prf2 ***** #EQ destruct
    366 #H1 #H2 #_ #_ #_ >get_cost_label_append >length_append >get_costlabelled_is_costlabelled //
    367  >get_cost_label_append >length_append >get_costlabelled_is_costlabelled // /2 by le_plus_a/
    368 qed.
     453#S1 #S2 #rel #sim_rel #si #sn #t #s1 #s3 #Hmeas #s1' #Hclass #Rsi_si'
     454cases Hmeas -Hmeas #s0 * #s2 * #ti0 * #t12 * #t3n * #l1 * #l2 * #prf1 * #prf2 *******
     455#pre_t12 #EQ destruct #Hl1 #Hl2 #Hcall_fin #sil_ti0 #sil_t3n #Hcall_init
     456cases(silent_in_silent … sim_rel … Rsi_si' sil_ti0)
     457#s0' * #ti0' * #sil_ti0' #Rs0_s0'
     458cases(simulate_labelled_action … prf1 … Rs0_s0') /2/
     459     [2: % * #H1 #H2 lapply(head_of_premeasurable_is_not_io … pre_t12) >H2 * /2/ ]
     460#s0'' * #s1'' * #s1' * #t_s0'' * #t_s1'' **** #sil_ts0'' #sil_ts1'' #prf1' #Hcall_init'
     461#Rs1_s1'
     462cases(simulates_pre_mesurable … sim_rel … pre_t12 … Rs1_s1')
     463[2: % #H lapply(head_of_premeasurable_is_not_io … pre_t12) >(io_is_io … sim_rel … H) // * /2/ ]
     464#s2' * #t12' **** #pre_t12' #EQcost #Rs2_s2' #_ #_
     465cases(simulate_labelled_action … prf2 … Rs2_s2') /2/
     466  [2: % * #H1 #H2 lapply(tail_of_premeasurable_is_not_io … pre_t12) >H1 * /2/]
     467#s2'' * #s3'' * #s3' * #t_s2'' * #t_s3'' **** #sil_ts2'' #sil_ts3'' #prf2' #Hcall_fin' #Rs3_s3'
     468cases(silent_in_silent … sim_rel … Rs3_s3' sil_t3n)
     469#sn' * #t_3n' * #sil_t3n' #Rsn_sn' %{sn'}
     470%{(ti0'@ t_s0'' @ (t_ind … prf1' (t_s1''@t12' @ t_s2'' @ (t_ind … prf2' (t_s3'' @ t_3n')))))}
     471% [ % // cases daemon (*TODO*) ]
     472%{s1''} %{s3''} whd %{s0''} %{s2''} %{(ti0' @t_s0'')} %{(t_s1'' @ t12' @ t_s2'')}
     473%{(t_s3'' @ t_3n')} %{l1} %{l2} %{prf1'} %{prf2'} % [2: /2/]
     474% [2: /2 by append_silent/] % [2: /2 by append_silent/] % [2: /2/] % // % // % //
     475@append_premeasurable_silent /2/
     476qed.
     477
     478
Note: See TracChangeset for help on using the changeset viewer.