Changeset 3535 for LTS/Traces.ma


Ignore:
Timestamp:
Mar 16, 2015, 4:30:28 PM (5 years ago)
Author:
piccolo
Message:

final statement of cerco with the first pass integrated in place

File:
1 edited

Legend:

Unmodified
Added
Removed
  • LTS/Traces.ma

    r3531 r3535  
    274274λS,st1,st2,st3,t1,t2.∃t3 : raw_trace … st1 st2.t2 = t3 @ t1.
    275275
    276 let rec get_costlabels_of_trace (S : abstract_status) (st1 : S) (st2 : S)
    277 (t : raw_trace S st1 st2) on t : list CostLabel ≝
    278 match t with
    279 [ t_base st ⇒ [ ]
    280 | t_ind st1' st2' st3' l prf t' ⇒
    281     let tl ≝ get_costlabels_of_trace … t' in
    282     match l with
     276definition actionlabel_to_costlabel ≝
     277λl : ActionLabel.match l with
    283278    [ call_act f c ⇒ [ c ]
    284279    | ret_act x ⇒ match x with
     
    290285                  | None ⇒ []
    291286                  ]
    292    ] @ tl
     287   ].
     288
     289let rec get_costlabels_of_trace (S : abstract_status) (st1 : S) (st2 : S)
     290(t : raw_trace S st1 st2) on t : list CostLabel ≝
     291match t with
     292[ t_base st ⇒ [ ]
     293| t_ind st1' st2' st3' l prf t' ⇒
     294    let tl ≝ get_costlabels_of_trace … t' in
     295    actionlabel_to_costlabel l  @ tl
    293296].
    294297
     
    636639
    637640definition measurable :
    638  ∀S: abstract_status. ∀si,s1,s3,sn : S. raw_trace … si sn → Prop ≝
     641 ∀S: abstract_status. ∀si,s1,s3,sn : S. raw_trace … si sn →  Prop ≝
    639642λS,si,s1,s3,sn,t.
    640643 ∃s0,s2:S. ∃ti0 : raw_trace … si s0.∃t12 : raw_trace … s1 s2.∃t3n : raw_trace … s3 sn.
Note: See TracChangeset for help on using the changeset viewer.