Changeset 3390 for LTS/Traces.ma


Ignore:
Timestamp:
Oct 10, 2013, 2:53:31 PM (6 years ago)
Author:
piccolo
Message:

Patched simulation proof, changed definition of silent trace

File:
1 edited

Legend:

Unmodified
Added
Removed
  • LTS/Traces.ma

    r3388 r3390  
    198198| silent_empty : ∀st : S.pre_silent_trace … (t_base S st)
    199199| silent_cons : ∀st1,st2,st3 : S.∀prf : as_execute S (cost_act (None ?)) st1 st2.
    200                 ∀tl : raw_trace S st2 st3. as_classify … st2 = cl_other → pre_silent_trace … tl →
     200                ∀tl : raw_trace S st2 st3. as_classify … st2 ≠ cl_io → pre_silent_trace … tl →
    201201                pre_silent_trace … (t_ind … prf … tl).
    202202
     
    208208[ #st' #EQ1 #EQ2 destruct #EQ destruct]
    209209#st1' #st2' #st3' #prf' #tl' #Hclass #silent_tl' #_ #EQ1 #EQ2 destruct
    210 #EQ destruct #_ #Hclass' @IH [ assumption ] >Hclass % #EQ destruct
     210#EQ destruct #_ #Hclass' @IH [ assumption ] assumption
    211211qed.
    212212
     
    217217definition silent_trace : ∀S : abstract_status.∀st1,st2 : S.
    218218raw_trace S st1 st2 → Prop ≝ λS,st1,st2,t.pre_silent_trace … t ∧
    219 (is_trace_non_empty … t → as_classify … st1 = cl_other).
     219(is_trace_non_empty … t → as_classify … st1 ≠ cl_io) ∧
     220well_formed_trace … t.
    220221
    221222lemma silent_is_well_formed : ∀S : abstract_status.∀st1,st2 : S.
    222223∀t : raw_trace S st1 st2. silent_trace … t → well_formed_trace … t.
    223 #S #st1 #st2 #t elim t -t
     224#S #st1 #st2 #t * //
     225qed.
     226(* elim t -t
    224227[ #st #_ %]
    225228#st1' #st2' #st3' #l #prf #tl #IH * #H #cl %2
     
    228231#st1'' #st2'' #st3'' #prf' #tl' #H1 #Htl' #_ #EQ1 #EQ2 #EQ3 destruct #_
    229232% [ assumption | #_ assumption]
    230 qed.
     233qed.*)
    231234
    232235inductive pre_measurable_trace (S : abstract_status) :
Note: See TracChangeset for help on using the changeset viewer.