Changeset 3391 for LTS/Traces.ma


Ignore:
Timestamp:
Oct 10, 2013, 5:28:33 PM (6 years ago)
Author:
piccolo
Message:

Definition of well formed trace is in the operational semantics

File:
1 edited

Legend:

Unmodified
Added
Removed
  • LTS/Traces.ma

    r3390 r3391  
    6565 | cl_other : status_class.
    6666
     67definition is_non_silent_cost_act : ActionLabel → Prop ≝
     68λact. ∃l. act = cost_act (Some ? l).
     69
    6770record abstract_status : Type[2] ≝
    6871 { as_status :> Type[0]
     
    7578 ; is_io_entering : NonFunctionalLabel → bool
    7679 ; is_io_exiting : NonFunctionalLabel → bool
     80 ; jump_emits : ∀s1,s2,l.
     81      as_classify … s1 = cl_jump →
     82      as_execute l s1 s2 → is_non_silent_cost_act l
    7783 }.
    7884 
     
    118124λact.act = ret_act (None ?).
    119125
    120 definition is_non_silent_cost_act : ActionLabel → Prop ≝
    121 λact. ∃l. act = cost_act (Some ? l).
    122 
    123126definition is_costlabelled_act : ActionLabel → Prop ≝
    124127λact.match act with [ call_act _ _ ⇒ True
     
    127130                    | init_act ⇒ False
    128131                    ].
    129 
    130 inductive well_formed_trace (S : abstract_status) :
    131    ∀st1,st2 : S.raw_trace S st1 st2 → Prop ≝
    132   | wf_empty : ∀st: S.well_formed_trace … (t_base S st)
    133   | wf_cons_no_jump :  ∀st1,st2,st3 : S.∀l : ActionLabel.
    134                        ∀prf: as_execute S l st1 st2.∀ tl: raw_trace S st2 st3.
    135                        well_formed_trace … tl → as_classify … st1 ≠ cl_jump →
    136                        well_formed_trace … (t_ind … prf … tl)
    137   | wf_cons_jump : ∀st1,st2,st3 : S.∀ l : ActionLabel.
    138                   ∀prf : as_execute S l st1 st2.∀tl : raw_trace S st2 st3.
    139                   well_formed_trace … tl → is_non_silent_cost_act l →
    140                   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 
     132(*
    146133lemma well_formed_trace_inv :
    147134∀S : abstract_status.∀st1,st2 : S.∀t : raw_trace S st1 st2.
     
    167154qed.
    168155
     156*)
    169157
    170158let rec append_on_trace (S : abstract_status) (st1 : S) (st2 : S) (st3 : S)
     
    194182λS,st1,st2,st3,t1,t2.∃t3 : raw_trace … st1 st2.t2 = t3 @ t1.
    195183
    196 inductive pre_silent_trace (S : abstract_status) :
     184inductive silent_trace (S : abstract_status) :
    197185∀st1,st2 : S.raw_trace S st1 st2 → Prop ≝
    198 | silent_empty : ∀st : S.pre_silent_trace … (t_base S st)
     186| silent_empty : ∀st : S.as_classify … st ≠ cl_io → silent_trace … (t_base S st)
    199187| 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_io → pre_silent_trace … tl →
    201                 pre_silent_trace … (t_ind … prf … tl).
     188                ∀tl : raw_trace S st2 st3. as_classify … st1 ≠ cl_io → silent_trace … tl →
     189                silent_trace … (t_ind … prf … tl).
    202190
    203191lemma silent_io : ∀S : abstract_status.
    204 ∀s1,s2 : S. ∀t : raw_trace … s1 s2. pre_silent_trace … t → as_classify … s1 ≠ cl_io
     192∀s1,s2 : S. ∀t : raw_trace … s1 s2. silent_trace … t
    205193as_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]
     194#S #s1 #s2 #t elim t [ #st #H inversion H // #st1 #st2 #st3 #prf #tl #H1 #sil_tl #_ #EQ1 #EQ2 #EQ3 destruct]
     195#st1 #st2 #st3 #l #prf #tl #IH #H inversion H //
    209196#st1' #st2' #st3' #prf' #tl' #Hclass #silent_tl' #_ #EQ1 #EQ2 destruct
    210 #EQ destruct #_ #Hclass' @IH [ assumption ] assumption
     197#EQ destruct #_ @IH assumption
    211198qed.
    212199
     
    214201raw_trace S st1 st2 → bool ≝
    215202λS,st1,st2,t.match t with [ t_base _ ⇒ false | _ ⇒ true ].
    216 
     203(*
    217204definition silent_trace : ∀S : abstract_status.∀st1,st2 : S.
    218205raw_trace S st1 st2 → Prop ≝ λS,st1,st2,t.pre_silent_trace … t ∧
    219 (is_trace_non_empty … t → as_classify … st1 ≠ cl_io) ∧
    220206well_formed_trace … t.
    221207
     
    223209∀t : raw_trace S st1 st2. silent_trace … t → well_formed_trace … t.
    224210#S #st1 #st2 #t * //
    225 qed.
     211qed. *)
    226212(* elim t -t
    227213[ #st #_ %]
Note: See TracChangeset for help on using the changeset viewer.