Changeset 3387 for LTS/Traces.ma


Ignore:
Timestamp:
Jul 23, 2013, 4:33:51 PM (6 years ago)
Author:
piccolo
Message:

unified notation

File:
1 edited

Legend:

Unmodified
Added
Removed
  • LTS/Traces.ma

    r3380 r3387  
    4545coercion ret_act_label_to_cost_label.
    4646
     47definition call_act_label_to_cost_label :
     48(CallCostLabel + NonFunctionalLabel) → CostLabel ≝
     49λx.match x with [inl a ⇒ a_call a | inr b ⇒ a_non_functional_label b].
     50
     51coercion call_act_label_to_cost_label.
     52
    4753inductive ActionLabel : Type[0] ≝
    4854 | call_act : FunctionName → (CallCostLabel + NonFunctionalLabel) → ActionLabel
    4955 | ret_act : option(ReturnPostCostLabel + NonFunctionalLabel) → ActionLabel
    50  | cost_act : list NonFunctionalLabel → ActionLabel.
     56 | cost_act : option NonFunctionalLabel → ActionLabel
     57 | init_act : ActionLabel.
    5158 
    5259definition is_cost_label : ActionLabel → Prop ≝
     
    6471 ; as_classify : as_status → status_class
    6572 ; is_call_post_label : as_status → bool
     73 ; as_initial : as_status → bool
     74 ; as_final : as_status → bool
     75 ; is_io_entering : NonFunctionalLabel → bool
     76 ; is_io_exiting : NonFunctionalLabel → bool
    6677 }.
    6778 
     79definition is_act_io_entering : abstract_status → ActionLabel → bool ≝
     80λS,l.match l with
     81[ call_act f c ⇒ match c with [ inl _ ⇒ false | inr c' ⇒ is_io_entering S c' ]
     82| ret_act x ⇒ match x with [ Some c ⇒ match c with [inl _ ⇒ false
     83                                                   | inr c' ⇒ is_io_entering S c']
     84                           | None ⇒ false
     85                           ]
     86| cost_act x ⇒ match x with [ Some c ⇒ is_io_entering S c | None ⇒ false ]
     87| init_act ⇒ false
     88].
     89
     90definition is_act_io_exiting : abstract_status → ActionLabel → bool ≝
     91λS,l.match l with
     92[ call_act f c ⇒ match c with [ inl _ ⇒ false | inr c' ⇒ is_io_exiting S c' ]
     93| ret_act x ⇒ match x with [ Some c ⇒ match c with [inl _ ⇒ false
     94                                                   | inr c' ⇒ is_io_exiting S c']
     95                           | None ⇒ false
     96                           ]
     97| cost_act x ⇒ match x with [ Some c ⇒ is_io_exiting S c | None ⇒ false ]
     98| init_act ⇒ false
     99].
     100
     101
    68102inductive raw_trace (S : abstract_status) : S → S → Type[0] ≝
    69103  | t_base : ∀st : S.raw_trace S st st
     
    81115λact.∃l.act = ret_act (Some ? l).
    82116
     117definition is_unlabelled_ret_act : ActionLabel → Prop ≝
     118λact.act = ret_act (None ?).
     119
    83120definition is_non_silent_cost_act : ActionLabel → Prop ≝
    84 λact. ∃hd,tl. act = cost_act (hd::tl).
     121λact. ∃l. act = cost_act (Some ? l).
     122
     123definition is_costlabelled_act : ActionLabel → Prop ≝
     124λact.match act with [ call_act _ _ ⇒ True
     125                    | ret_act x ⇒ match x with [ Some _ ⇒ True | None ⇒ False ]
     126                    | cost_act x ⇒ match x with [ Some _ ⇒ True | None ⇒ False ]
     127                    | init_act ⇒ False
     128                    ].
    85129
    86130inductive well_formed_trace (S : abstract_status) :
     
    113157[ #st #t2 #t3 %] #st1' #st2' #st3' #l #prf #tl #IH #t2 #t3 whd in ⊢ (??%%); >IH %
    114158qed.
    115 (*
    116 inductive balanced_trace (S : abstract_status) :
     159
     160definition trace_prefix: ∀S : abstract_status.∀st1,st2,st3 : S.raw_trace … st1 st2 →
     161raw_trace … st1 st3 → Prop≝
     162λS,st1,st2,st3,t1,t2.∃t3 : raw_trace … st2 st3.t2 = t1 @ t3.
     163
     164definition trace_suffix : ∀S : abstract_status.∀st1,st2,st3 : S.raw_trace … st2 st3 →
     165raw_trace … st1 st3 → Prop≝
     166λS,st1,st2,st3,t1,t2.∃t3 : raw_trace … st1 st2.t2 = t3 @ t1.
     167
     168inductive silent_trace (S : abstract_status) :
    117169∀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 *)
     170| silent_empty : ∀st : S.silent_trace … (t_base S st)
     171| 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).
     174
    132175inductive pre_measurable_trace (S : abstract_status) :
    133176∀st1,st2 : S.raw_trace ? st1 st2 → Prop ≝
    134  | pm_empty : ∀st : S. pre_measurable_trace … (t_base ? st)
     177 | pm_empty : ∀st : S. as_classify … st ≠ cl_io → pre_measurable_trace … (t_base ? st)
    135178 | pm_cons_cost_act : ∀st1,st2,st3 : S.∀l : ActionLabel.
    136179                      ∀prf : as_execute S l st1 st2.∀tl : raw_trace S st2 st3.
    137                       is_cost_act l → pre_measurable_trace … tl →
     180                      as_classify … st1 ≠ cl_io → is_cost_act l → pre_measurable_trace … tl →
    138181                      pre_measurable_trace … (t_ind … prf … tl)
    139182 | pm_cons_lab_ret : ∀st1,st2,st3 : S.∀l : ActionLabel.
     183                      as_classify … st1 ≠ cl_io →
    140184                      ∀prf : as_execute S l st1 st2.∀tl : raw_trace S st2 st3.
    141185                      is_labelled_ret_act l → pre_measurable_trace … tl →
     
    143187 | pm_cons_post_call : ∀st1,st2,st3 : S.∀l : ActionLabel.
    144188                      ∀prf : as_execute S l st1 st2.∀tl : raw_trace S st2 st3.
    145                       is_call_act l → is_call_post_label … st1 →
     189                      as_classify … st1 ≠ cl_io → is_call_act l → is_call_post_label … st1 →
    146190                      pre_measurable_trace … tl →
    147191                      pre_measurable_trace … (t_ind … prf … tl)
     
    149193                      ∀prf : as_execute S l1 st1 st2.∀t1 : raw_trace S st2 st3.
    150194                      ∀t2 : raw_trace S st4 st5.∀prf' : as_execute S l2 st3 st4.
    151                       is_call_act l1 → ¬ is_call_post_label … st1 →
     195                      as_classify … st1 ≠ cl_io → as_classify … st3 ≠ cl_io
     196                      →  is_call_act l1 → ¬ is_call_post_label … st1 →
    152197                      pre_measurable_trace … t1 → pre_measurable_trace … t2 →
    153198                      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 
    161 definition 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 
    167 inductive 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 
    180  
    181 
    182 
    183 
     199                      is_unlabelled_ret_act l2 →
     200                      pre_measurable_trace … (t_ind … prf … (t1 @ (t_ind … prf' … t2))).
Note: See TracChangeset for help on using the changeset viewer.