Changeset 3380


Ignore:
Timestamp:
Jul 2, 2013, 7:25:14 PM (4 years ago)
Author:
piccolo
Message:

Added definition of measurable trace

File:
1 edited

Legend:

Unmodified
Added
Removed
  • LTS/Traces.ma

    r3374 r3380  
    4646
    4747inductive ActionLabel : Type[0] ≝
    48  | call_act : FunctionName → CallCostLabel → ActionLabel
     48 | call_act : FunctionName → (CallCostLabel + NonFunctionalLabel) → ActionLabel
    4949 | ret_act : option(ReturnPostCostLabel + NonFunctionalLabel) → ActionLabel
    50  | cost_act : NonFunctionalLabel → ActionLabel
    51  | tau_act : ActionLabel.
     50 | cost_act : list NonFunctionalLabel → ActionLabel.
    5251 
    5352definition is_cost_label : ActionLabel → Prop ≝
    5453λact.match act with [ cost_act nf ⇒ True | _ ⇒ False ].
    5554
    56 record program_counter_type : Type[1] ≝
    57   { pc_type : DeqSet
    58   ; succ_pc : pc_type → pc_type
    59   }.
     55inductive status_class : Type[0] ≝
     56 | cl_jump : status_class
     57 | cl_io : status_class
     58 | cl_other : status_class.
    6059
    6160record abstract_status : Type[2] ≝
    6261 { as_status :> Type[0]
    6362 ; as_execute : ActionLabel → relation as_status
    64  ; as_pc : program_counter_type
    65  ; as_pc_of : as_status → (pc_type as_pc)
    66  ; is_jump : as_status → bool
     63 ; as_syntactical_succ : relation as_status
     64 ; as_classify : as_status → status_class
     65 ; is_call_post_label : as_status → bool
    6766 }.
    6867 
    69 inductive raw_trace (S : abstract_status) : option(ActionLabel) → S → S → Type[0] ≝
    70   | t_base : ∀st : S.raw_trace S (None ?) st st
    71   | t_ind : ∀st1,st2,st3 : S.∀m.∀l : ActionLabel.
    72              as_execute S l st1 st2 → raw_trace S m st2 st3 →
    73              raw_trace S (Some ? l) st1 st3.
    74              
     68inductive raw_trace (S : abstract_status) : S → S → Type[0] ≝
     69  | t_base : ∀st : S.raw_trace S st st
     70  | t_ind : ∀st1,st2,st3 : S.∀l : ActionLabel.
     71             as_execute S l st1 st2 → raw_trace S st2 st3 →
     72             raw_trace S st1 st3.
     73
     74definition is_cost_act : ActionLabel → Prop ≝
     75λact.∃l.act = cost_act l.
     76
     77definition is_call_act : ActionLabel → Prop ≝
     78λact.∃f,l.act = call_act f l.
     79
     80definition is_labelled_ret_act : ActionLabel → Prop ≝
     81λact.∃l.act = ret_act (Some ? l).
     82
     83definition is_non_silent_cost_act : ActionLabel → Prop ≝
     84λact. ∃hd,tl. act = cost_act (hd::tl).
     85
    7586inductive well_formed_trace (S : abstract_status) :
    7687   ∀st1,st2 : S.raw_trace S st1 st2 → Prop ≝
    77   | t_empty : ∀st: S.well_formed_trace … (t_base S st)
    78   | t_cons_uncosted :  ∀st1,st2 : .
     88  | wf_empty : ∀st: S.well_formed_trace … (t_base S st)
     89  | wf_cons_no_jump :  ∀st1,st2,st3 : S.∀l : ActionLabel.
     90                       ∀prf: as_execute S l st1 st2.∀ tl: raw_trace S st2 st3.
     91                       well_formed_trace … tl → as_classify … st1 ≠ cl_jump →
     92                       well_formed_trace … (t_ind … prf … tl)
     93  | wf_cons_jump : ∀st1,st2,st3 : S.∀ l : ActionLabel.
     94                  ∀prf : as_execute S l st1 st2.∀tl : raw_trace S st2 st3.
     95                  well_formed_trace … tl → is_non_silent_cost_act l →
     96                  well_formed_trace … (t_ind … prf … tl).
     97
     98let rec append_on_trace (S : abstract_status) (st1 : S) (st2 : S) (st3 : S)
     99(t1 : raw_trace S st1 st2) on t1 : raw_trace S st2 st3 → raw_trace S st1 st3 ≝
     100match t1
     101return λst1,st2,tr.raw_trace S st2 st3 → raw_trace S st1 st3
     102with
     103[ t_base st ⇒ λt2.t2
     104| t_ind st1' st2' st3' l prf tl ⇒ λt2.t_ind … prf … (append_on_trace … tl t2)
     105].
     106
     107interpretation "trace_append" 'append t1 t2 = (append_on_trace ???? t1 t2).
     108
     109lemma append_associative : ∀S,st1,st2,st3,st4.
     110∀t1 : raw_trace S st1 st2.∀t2 : raw_trace S st2 st3.
     111∀t3 : raw_trace S st3 st4.(t1 @ t2) @ t3 = t1 @ (t2 @ t3).
     112#S #st1 #st2 #st3 #st4 #t1 elim t1 -t1
     113[ #st #t2 #t3 %] #st1' #st2' #st3' #l #prf #tl #IH #t2 #t3 whd in ⊢ (??%%); >IH %
     114qed.
     115(*
     116inductive balanced_trace (S : abstract_status) :
     117∀st1,st2 : S.raw_trace S st1 st2 → Prop ≝
     118 | bal_empty : ∀ st : S.balanced_trace … (t_base S st)
     119 | bal_cons_cost : ∀st1,st2,st3 : S.∀l : ActionLabel.
     120                   ∀prf : as_execute S l st1 st2.∀tl : raw_trace S st2 st3.
     121                   balanced_trace … tl → is_cost_act l →
     122                   balanced_trace … (t_ind … prf … tl)
     123 | bal_cons_call : ∀s,st1,st2,st3,st4,f,l1,l2.
     124                   ∀prf1 : as_execute S (call_act f l1) s st1.
     125                   ∀t1 : raw_trace S st1 st2.∀t2 : raw_trace S st3 st4.
     126                   ∀prf2 : as_execute S (ret_act l2) st2 st3.
     127                   (bool_to_Prop (is_call_post_label … s) → l2 ≠ None ?) →
     128                   as_syntactical_succ S s st3 →
     129                   balanced_trace … t1 → balanced_trace … t2 →
     130                   balanced_trace … (t_ind … prf1 … (t1 @ (t_ind … prf2 … t2))).
     131*)
     132inductive pre_measurable_trace (S : abstract_status) :
     133∀st1,st2 : S.raw_trace ? st1 st2 → Prop ≝
     134 | pm_empty : ∀st : S. pre_measurable_trace … (t_base ? st)
     135 | pm_cons_cost_act : ∀st1,st2,st3 : S.∀l : ActionLabel.
     136                      ∀prf : as_execute S l st1 st2.∀tl : raw_trace S st2 st3.
     137                      is_cost_act l → pre_measurable_trace … tl →
     138                      pre_measurable_trace … (t_ind … prf … tl)
     139 | pm_cons_lab_ret : ∀st1,st2,st3 : S.∀l : ActionLabel.
     140                      ∀prf : as_execute S l st1 st2.∀tl : raw_trace S st2 st3.
     141                      is_labelled_ret_act l → pre_measurable_trace … tl →
     142                      pre_measurable_trace … (t_ind … prf … tl)
     143 | pm_cons_post_call : ∀st1,st2,st3 : S.∀l : ActionLabel.
     144                      ∀prf : as_execute S l st1 st2.∀tl : raw_trace S st2 st3.
     145                      is_call_act l → is_call_post_label … st1 →
     146                      pre_measurable_trace … tl →
     147                      pre_measurable_trace … (t_ind … prf … tl)
     148 | pm_balanced_call : ∀st1,st2,st3,st4,st5.∀l1,l2.
     149                      ∀prf : as_execute S l1 st1 st2.∀t1 : raw_trace S st2 st3.
     150                      ∀t2 : raw_trace S st4 st5.∀prf' : as_execute S l2 st3 st4.
     151                      is_call_act l1 → ¬ is_call_post_label … st1 →
     152                      pre_measurable_trace … t1 → pre_measurable_trace … t2 →
     153                      as_syntactical_succ S st1 st4 →
     154                      match l2 with
     155                      [ call_act _ _ ⇒ bool_to_Prop(is_call_post_label ? st3)
     156                      | ret_act _ ⇒ True
     157                      | cost_act x ⇒ match x with [ nil ⇒ False | _ ⇒ True ]
     158                      ]
     159                      → pre_measurable_trace … (t_ind … prf … (t1 @ (t_ind … prf' … t2))).
     160
     161definition starts_with_label_trace : ∀S : abstract_status.∀st1,st2 : S.raw_trace S st1 st2 → Prop ≝
     162λS,st1,st2,t.match t with
     163[ t_base st ⇒ False
     164| t_ind st1 st2 st3 l _ _ ⇒ is_call_act l ∨ is_labelled_ret_act l ∨ is_non_silent_cost_act l
     165].
     166
     167inductive ends_with_label_trace (S : abstract_status) :
     168∀st1,st2 : S.raw_trace S st1 st2 → Prop ≝
     169| call_base : ∀st1,st2 : S.∀l : ActionLabel.∀prf : as_execute S l st1 st2.
     170               is_call_act l → ends_with_label_trace … (t_ind … prf … (t_base S st2))
     171| lab_ret_base : ∀st1,st2 : S.∀l : ActionLabel.∀prf : as_execute S l st1 st2.
     172               is_labelled_ret_act l → ends_with_label_trace … (t_ind … prf … (t_base S st2))
     173| non_silent_cost_act_base : ∀st1,st2 : S.∀l : ActionLabel.∀prf : as_execute S l st1 st2.
     174               is_non_silent_cost_act l → ends_with_label_trace … (t_ind … prf … (t_base S st2))
     175| cons : ∀st1,st2,st3 : S.∀l : ActionLabel.∀prf : as_execute S l st1 st2.
     176               ∀t : raw_trace S st2 st3. ends_with_label_trace … t →
     177               ends_with_label_trace … (t_ind … prf … t).
     178                     
     179
    79180 
    80181
    81182
     183
Note: See TracChangeset for help on using the changeset viewer.