Changeset 3478 for LTS/Simulation.ma


Ignore:
Timestamp:
Sep 22, 2014, 4:50:21 PM (5 years ago)
Author:
piccolo
Message:

fixed costlabels

File:
1 edited

Legend:

Unmodified
Added
Removed
  • LTS/Simulation.ma

    r3449 r3478  
    110110                  | None ⇒ []
    111111                  ]
    112     | init_act ⇒ []
    113     ] @ tl
     112
     113   ] @ tl
    114114].
    115115
     
    240240 append … (get_costlabels_of_trace … t1) (get_costlabels_of_trace … t2).
    241241#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
     242[#f * #l | * [| * #l] | *  [| #l] ] #prf #tl #IH #t2 normalize try @eq_f @IH
    243243qed.
    244244 
     
    402402
    403403record measurable_trace (S : abstract_status) : Type[0] ≝
    404  { L_label: ActionLabel
     404 { L_label: option ActionLabel
    405405 ; R_label : option ActionLabel
    406406 ; L_pre_state : option S
     
    411411 ; pre_meas : pre_measurable_trace … trace
    412412 ; L_init_ok : match L_pre_state with
    413                [ None ⇒ bool_to_Prop(as_initial … L_s1) ∧ L_label = init_act
    414                | Some s ⇒ is_costlabelled_act L_label ∧
    415                           as_execute … L_label s L_s1
     413               [ None ⇒ bool_to_Prop(as_initial … L_s1) ∧ L_label = None ?
     414               | Some s ⇒ ∃l. L_label = Some ? l ∧ is_costlabelled_act l ∧
     415                          as_execute … l s L_s1
    416416               ]
    417417 ; R_fin_ok : match R_label with
     
    454454∀rel : relations S.
    455455simulation_conditions … rel →
    456 ∀s1,s1': S.∀l.l ≠ init_act → l ≠ cost_act (None ?) →  as_execute S l s1 s1' →
     456∀s1,s1': S.∀l.l ≠ cost_act (None ?) →  as_execute S l s1 s1' →
    457457(as_classify … s1 ≠ cl_io ∨ as_classify … s1' ≠ cl_io) →
    458458∀s2.
     
    463463(is_call_act l → is_call_post_label … s1 → is_call_post_label … s2') ∧
    464464(as_classify … s1' ≠ cl_io → as_classify … s2'' ≠ cl_io).
    465 #S #rel #good #s1 #s1' #l #l_noinit #l_notau #prf #HIO #s2 #REL cases(case_cl_io … (as_classify … s1))
     465#S #rel #good #s1 #s1' #l #l_notau #prf #HIO #s2 #REL cases(case_cl_io … (as_classify … s1))
    466466[ #EQs1_io cases(io_exiting … EQs1_io … prf) #lab #EQ destruct(EQ)
    467467  cases HIO [ >EQs1_io * #EQ @⊥ @EQ % ] #Hio_s1'
     
    477477    %{exe} %{s2''} %{(t_base …)} % [2: >EQs1' * #H @⊥ @H % ] %
    478478     [ /4 by or_intror, conj, nmk/] * #f * #l #EQ destruct
    479   | #Hclass_s1' cases l in prf l_noinit l_notau;
    480     [ #f #l #prf #_ #_ inversion(is_call_post_label … s1)
     479  | #Hclass_s1' cases l in prf l_notau;
     480    [ #f #l #prf #_ inversion(is_call_post_label … s1)
    481481      [ #Hpost cases(simulate_call_pl … good … prf … REL)
    482482        [2: >Hpost % |3,4: assumption]
     
    492492     ]
    493493   | *
    494      [ #prf #_ #_ cases(simulate_ret_n … good … prf … REL) [2,3: //] #s2' * #s2''
     494     [ #prf #_ cases(simulate_ret_n … good … prf … REL) [2,3: //] #s2' * #s2''
    495495       * #s2''' * #t1 * #exe * #t3 *** #REL' #sil_t1 #sil_t3 #_ %{s2'}
    496496       %{t1} %{(or_introl … sil_t1)} %{s2''} %{exe} %{s2'''} %{t3} %
    497497       [2: #_ @(head_of_premeasurable_is_not_io … t3) /2 by pre_silent_is_premeasurable/ ]
    498498       % [ % // % // ] * #f * #l #EQ destruct
    499      | #l #prf #_ #_ cases(simulate_ret_l … good … prf … REL) [2,3: //]
     499     | #l #prf #_ cases(simulate_ret_l … good … prf … REL) [2,3: //]
    500500       #s2' * #s2'' * #s2''' * #t1 * #exe * #t3 ** #REL' #sil_t1 #sil_t3
    501501       %{s2'} %{t1} %{sil_t1} %{s2''} %{exe} %{s2'''} %{t3} %
     
    503503       % [ % // % //] * #f * #l #EQ destruct
    504504    ]
    505   | * [ #_ #_ * #H @⊥ @H % ] #lab #prf #_ #_
     505  | * [ #_ * #H @⊥ @H % ] #lab #prf #_
    506506    cases(simulate_label … prf … REL) [2,3,4: // ] #s2' * #s2'' * #s2''' * #t1
    507507    * #exe * #t3 ** #REL' #sil_t1 #sil_t3 %{s2'} %{t1} %{sil_t1} %{s2''} %{exe}
     
    509509    [2: #_ @(head_of_premeasurable_is_not_io … t3) /2 by pre_silent_is_premeasurable/ ]
    510510    % [% // % //] * #f * #l #EQ destruct
    511   | #_ * #H @⊥ @H %
    512511  ]
    513512  % //
     
    549548[2: #REL_pre
    550549    cut
    551      (∃pre_state: S.
     550     (∃pre_state: S.∃ l.
    552551      ∃tr_i : raw_trace S s2 pre_state. silent_trace … tr_i ∧
    553       ∃middle_state: S.
    554        as_execute … (L_label … t) pre_state middle_state ∧
     552      ∃middle_state: S.L_label … t = Some ? l ∧
     553       as_execute … l pre_state middle_state ∧
    555554      ∃final_state: S.
    556555      ∃tr_i2: raw_trace S middle_state final_state. silent_trace … tr_i2 ∧
    557556       as_classify … final_state ≠ cl_io ∧
    558557       Srel … rel (L_s1 … t) final_state)
    559     [ lapply(L_init_ok … t) >EQpre normalize nodelta * #Hcost #exe   
    560       cases(instr_execute_commute … good … (L_label … t) … exe … REL_pre)
    561       [2,3: % #EQ >EQ in Hcost; * |4: %2 @(head_of_premeasurable_is_not_io … (pre_meas … t)) ]
     558      [ lapply(L_init_ok … t) >EQpre normalize nodelta * #l ** #EQllabe #Hcost #exe   
     559      cases(instr_execute_commute … good … l … exe … REL_pre)
     560      [2: % #EQ >EQ in Hcost; * |3: %2 @(head_of_premeasurable_is_not_io … (pre_meas … t)) ]
    562561      #s2' * #t1 * #sil_t1 * #s2'' * #exe * #s2''' * #t3 *** #sil_t3 #REL' #Hcall
    563       #Hclass %{s2'} %{t1} %{sil_t1} %{s2''} %{exe} %{s2'''} %{t3} % // % //
     562      #Hclass %{s2'} %{l} %{t1} %{sil_t1} %{s2''} % [% //] %{s2'''} %{t3} % // % //
    564563      cases sil_t3 [/2 by pre_silent_io/ ] inversion t3
    565564      [ #H109 #H110 #H111 #H112 #H113 destruct @Hclass @(head_of_premeasurable_is_not_io … (pre_meas … t)) ]
    566565      #H115 #H116 #H117 #H118 #H119 #H120 #H121 #H122 #H123 #H124 #H125 cases H125
    567566      #H @⊥ @H %]
    568     * #pre_state * #tr_i * #silent_i * #middle_state * #step_pre_middle
     567    * #pre_state * #l' * #tr_i * #silent_i * #middle_state ** #EQl' #step_pre_middle
    569568    * #final_state * #tr_i2 ** #silent_i2 #final_not_io #REL
    570569| #REL
    571   cut(bool_to_Prop (as_initial S s2)∧L_label S t=init_act)
     570  cut(bool_to_Prop (as_initial S s2)∧L_label S t=None ?)
    572571      [ lapply(L_init_ok … t) >EQpre normalize nodelta * #H1 #H2 % [2: //]
    573572        @(initial_is_initial … good … H1) assumption ] * #initial_s2 #init_label
     
    602601         * >EQpost #EQ destruct #exe
    603602          cases(instr_execute_commute … good … final_label … exe … REL')
    604           [2,3,6,7: % #EQ destruct cases H1 [1,3,5,7: * |*: normalize #EQ destruct]
    605           |4,8: %1 @tail_of_premeasurable_is_not_io //
     603          [2,5: % #EQ destruct cases H1 [1,3,5,7: * |*: normalize #EQ destruct]
     604          |3,6: %1 @tail_of_premeasurable_is_not_io //
    606605          ]
    607606          #s2' * #t1 * #sil_t1 * #s2'' * #exe * #s2''' * #t3 *** #sil_t3 #REL'
     
    613612     normalize nodelta /5 by conj/
    614613|3: %{(mk_measurable_trace … (L_label … t) (R_label … t) … (Some ? pre_state) … (Some ? post_state') … (tr_i2 @ t' @ tr') …)}
    615     normalize nodelta [2: % // lapply(L_init_ok … t) >EQpre normalize nodelta * //
     614    normalize nodelta [2: %{l'} % // % // lapply(L_init_ok … t) >EQpre normalize nodelta * #l'' ** >EQl'
     615      #EQ destruct //
    616616    |3: /3 by append_silent_premeasurable, append_premeasurable_silent/
    617617    |4: % [2: %{final_state'} /5 by ex_intro, conj/ ] % /8 by ex_intro, conj/ % [ /3 by conj/]
     
    625625  normalize nodelta
    626626  [ assumption
    627   | % // lapply(L_init_ok … t) >EQpre normalize nodelta * //
     627  | %{l'} % // % // lapply(L_init_ok … t) >EQpre normalize nodelta * #l'' ** >EQl' #EQ destruct //
    628628  | /4 by append_premeasurable_silent/
    629629  | % // % [2: %{pre_state} /3/ ] % [ /2/] >get_cost_label_append
Note: See TracChangeset for help on using the changeset viewer.