Changeset 3388 for LTS/Traces.ma


Ignore:
Timestamp:
Aug 27, 2013, 6:11:57 PM (6 years ago)
Author:
piccolo
Message:

partial commit

File:
1 edited

Legend:

Unmodified
Added
Removed
  • LTS/Traces.ma

    r3387 r3388  
    139139                  well_formed_trace … tl → is_non_silent_cost_act l →
    140140                  well_formed_trace … (t_ind … prf … tl).
     141(*  | wf_cons_io : ∀st1,st2,st3 : S.∀l : ActionLabel.
     142                 ∀prf : as_execute S l st1 st2.∀tl : raw_trace S st2 st3.
     143                 well_formed_trace … tl → as_classify … st1 = cl_io →
     144                 is_non_silent_cost_act l → well_formed_trace … (t_ind … prf … tl).*)
     145
     146lemma well_formed_trace_inv :
     147∀S : abstract_status.∀st1,st2 : S.∀t : raw_trace S st1 st2.
     148well_formed_trace … t →
     149(st1 = st2 ∧ t ≃ t_base S st1) ∨
     150(∃st1'.∃l.∃prf : as_execute S l st1 st1'.∃tl : raw_trace S st1' st2.
     151well_formed_trace … tl ∧ as_classify … st1 ≠ cl_jump ∧
     152t ≃ t_ind … prf … tl) ∨
     153(∃st1'.∃l.∃ prf : as_execute S l st1 st1'.∃ tl : raw_trace S st1' st2.
     154 well_formed_trace … tl ∧ is_non_silent_cost_act l ∧ t ≃ t_ind … prf … tl). (* ∨
     155(∃st1'.∃l.∃prf : as_execute S l st1 st1'.∃tl : raw_trace S st1' st2.
     156 well_formed_trace … tl ∧ as_classify … st1 = cl_io ∧
     157 is_non_silent_cost_act l ∧ t ≃ t_ind … prf … tl).*)
     158#S #st1 #st2 #t #H inversion H
     159[ #st #EQ1 #EQ2 destruct(EQ1 EQ2) #EQ destruct(EQ) #_ /5 by refl_jmeq, or_introl, conj/
     160| #st1' #st2' #st3' #l #prf' #tl' #Htl #Hclass #_ #EQ2 #EQ3 #EQ4 destruct #_
     161  %  %2 %{st2'} %{l} %{prf'} %{tl'} /4 by conj/
     162| #st1' #st2' #st3' #l #prf #tl #Htl #Hl #_ #EQ2 #EQ3 #EQ4 destruct #_ %2 %{st2'}
     163  %{l} %{prf} %{tl} % // % //
     164(*| #st1' #st2' #st3' #l #prf #tl #Htl #Hclass #is_non_silent #_ #EQ1 #EQ2 #EQ3
     165  destruct #_ %2 %{st2'} %{l} %{prf} %{tl} /5 by conj/ *)
     166]
     167qed.
     168
    141169
    142170let rec append_on_trace (S : abstract_status) (st1 : S) (st2 : S) (st3 : S)
     
    166194λS,st1,st2,st3,t1,t2.∃t3 : raw_trace … st1 st2.t2 = t3 @ t1.
    167195
    168 inductive silent_trace (S : abstract_status) :
     196inductive pre_silent_trace (S : abstract_status) :
    169197∀st1,st2 : S.raw_trace S st1 st2 → Prop ≝
    170 | silent_empty : ∀st : S.silent_trace … (t_base S st)
     198| silent_empty : ∀st : S.pre_silent_trace … (t_base S st)
    171199| silent_cons : ∀st1,st2,st3 : S.∀prf : as_execute S (cost_act (None ?)) st1 st2.
    172                 ∀tl : raw_trace S st2 st3. silent_trace … tl →
    173                 silent_trace … (t_ind … prf … tl).
     200                ∀tl : raw_trace S st2 st3. as_classify … st2 = cl_other → pre_silent_trace … tl →
     201                pre_silent_trace … (t_ind … prf … tl).
     202
     203lemma silent_io : ∀S : abstract_status.
     204∀s1,s2 : S. ∀t : raw_trace … s1 s2. pre_silent_trace … t → as_classify … s1 ≠ cl_io →
     205as_classify … s2 ≠ cl_io.
     206#S #s1 #s2 #t elim t [ #st #_ #Hclass @Hclass]
     207#st1 #st2 #st3 #l #prf #tl #IH #H inversion H
     208[ #st' #EQ1 #EQ2 destruct #EQ destruct]
     209#st1' #st2' #st3' #prf' #tl' #Hclass #silent_tl' #_ #EQ1 #EQ2 destruct
     210#EQ destruct #_ #Hclass' @IH [ assumption ] >Hclass % #EQ destruct
     211qed.
     212
     213definition is_trace_non_empty : ∀S : abstract_status.∀st1,st2.
     214raw_trace S st1 st2 → bool ≝
     215λS,st1,st2,t.match t with [ t_base _ ⇒ false | _ ⇒ true ].
     216
     217definition silent_trace : ∀S : abstract_status.∀st1,st2 : S.
     218raw_trace S st1 st2 → Prop ≝ λS,st1,st2,t.pre_silent_trace … t ∧
     219(is_trace_non_empty … t → as_classify … st1 = cl_other).
     220
     221lemma silent_is_well_formed : ∀S : abstract_status.∀st1,st2 : S.
     222∀t : raw_trace S st1 st2. silent_trace … t → well_formed_trace … t.
     223#S #st1 #st2 #t elim t -t
     224[ #st #_ %]
     225#st1' #st2' #st3' #l #prf #tl #IH * #H #cl %2
     226[2: >cl % #EQ destruct]
     227@IH inversion H in ⊢ ?; [ #st #EQ1 #EQ2 #EQ3 destruct]
     228#st1'' #st2'' #st3'' #prf' #tl' #H1 #Htl' #_ #EQ1 #EQ2 #EQ3 destruct #_
     229% [ assumption | #_ assumption]
     230qed.
    174231
    175232inductive pre_measurable_trace (S : abstract_status) :
     
    199256                      is_unlabelled_ret_act l2 →
    200257                      pre_measurable_trace … (t_ind … prf … (t1 @ (t_ind … prf' … t2))).
     258                     
     259lemma pre_measurable_trace_inv : ∀S : abstract_status.
     260∀st1,st2 : S.∀t : raw_trace … st1 st2. pre_measurable_trace … t →
     261(st1 = st2 ∧ as_classify … st1 ≠ cl_io ∧ t ≃ t_base … st1) ∨
     262(∃st1' : S.∃l.∃prf : as_execute S l st1 st1'.∃tl.
     263 t = t_ind … prf … tl ∧ as_classify … st1 ≠ cl_io ∧ is_cost_act l ∧
     264 pre_measurable_trace … tl) ∨
     265(∃st1' : S.∃l.∃prf : as_execute S l st1 st1'.∃tl.
     266 t = t_ind … prf … tl ∧
     267 as_classify … st1 ≠ cl_io ∧ is_labelled_ret_act l ∧ pre_measurable_trace … tl) ∨
     268(∃st1' : S .∃l.∃prf : as_execute S l st1 st1'.∃tl.
     269 t = t_ind … prf … tl ∧ as_classify … st1 ≠ cl_io ∧ is_call_act l ∧
     270 (bool_to_Prop (is_call_post_label … st1)) ∧ pre_measurable_trace … tl) ∨
     271(∃st1',st1'',st1''' : S.∃l1,l2.∃prf : as_execute S l1 st1 st1'.
     272 ∃t1 : raw_trace S st1' st1''.∃t2 : raw_trace S st1''' st2.
     273 ∃prf' : as_execute S l2 st1'' st1'''.
     274 t = t_ind … prf … (t1 @ (t_ind … prf' … t2)) ∧ as_classify … st1 ≠cl_io ∧
     275 as_classify … st1'' ≠ cl_io ∧ is_call_act l1 ∧
     276 bool_to_Prop (¬ is_call_post_label … st1) ∧
     277 pre_measurable_trace … t1 ∧ pre_measurable_trace … t2 ∧
     278 as_syntactical_succ S st1 st1''' ∧ is_unlabelled_ret_act l2).
     279#S #st1 #st2 #t #H inversion H
     280[ #st #Hclass #EQ1 #EQ2 destruct #EQ destruct #_ %%%%% // % //
     281| #st1' #st2' #st3' #l #prf #tl #Hst1' #Hl #Htl #_ #EQ1 #EQ2 #EQ3 destruct #_
     282  %%%%2 %{st2'} %{l} %{prf} %{tl} % // % // % //
     283| #st1' #st2' #st3' #l #Hst1 #prf #tl #Hl #Htl #_ #EQ1 #EQ2 #EQ3 destruct #_
     284  %%%2 %{st2'} %{l} %{prf} %{tl} % // % // % //
     285| #st1' #st2' #st3' #l #prf #tl #Hst1 #Hl #H1st1 #Htl #_ #EQ1 #EQ2 #EQ3 destruct #_
     286  % %2 %{st2'} %{l} %{prf} %{tl} % // % // % // % //
     287| #st1' #st2' #st3' #st4' #st5' #l1 #l2 #prf #t1 #t2 #prf' #Hst1' #Hst3' #Hl1
     288  #H1st1'  #Ht1 #Ht2 #succ #Hl2 #_ #_ #EQ1 #EQ2 #EQ3 destruct #_ %2
     289  %{st2'} %{st3'} %{st4'} %{l1} %{(ret_act (None ?))} %{prf} %{t1} %{t2}
     290  %{prf'} /12 by conj/
     291]
     292qed.
     293                     
Note: See TracChangeset for help on using the changeset viewer.