Changeset 3506 for LTS/Traces.ma


Ignore:
Timestamp:
Sep 26, 2014, 5:00:57 PM (5 years ago)
Author:
sacerdot
Message:

Refactoring.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • LTS/Traces.ma

    r3487 r3506  
    418418]
    419419qed.
    420                      
     420
     421definition measurable :
     422 ∀S: abstract_status. ∀si,s1,s3,sn : S. raw_trace … si sn → Prop ≝
     423λS,si,s1,s3,sn,t.
     424 pre_measurable_trace … t ∧
     425 ∃s0,s2:S. ∃ti0 : raw_trace … si s0.∃t12 : raw_trace … s1 s2.∃t3n : raw_trace … s3 sn.
     426 ∃l1,l2,prf1,prf2.
     427  t = ti0 @  t_ind ? s0 s1 sn l1 prf1 … (t12 @ (t_ind ? s2 s3 sn l2 prf2 … t3n))
     428 ∧ is_costlabelled_act l1 ∧ is_costlabelled_act l2 ∧ silent_trace … ti0 ∧ silent_trace … t3n.
     429
     430let rec get_costlabels_of_trace (S : abstract_status) (st1 : S) (st2 : S)
     431(t : raw_trace S st1 st2) on t : list CostLabel ≝
     432match t with
     433[ t_base st ⇒ [ ]
     434| t_ind st1' st2' st3' l prf t' ⇒
     435    let tl ≝ get_costlabels_of_trace … t' in
     436    match l with
     437    [ call_act f c ⇒ [ c ]
     438    | ret_act x ⇒ match x with
     439                  [ Some c ⇒ [ a_return_post c ]
     440                  | None ⇒ []
     441                  ]
     442    | cost_act x ⇒ match x with
     443                  [ Some c ⇒ [ a_non_functional_label c ]
     444                  | None ⇒ []
     445                  ]
     446   ] @ tl
     447].
     448
     449lemma get_cost_label_silent_is_empty : ∀S : abstract_status.
     450∀st1,st2.∀t : raw_trace S st1 st2.silent_trace … t → get_costlabels_of_trace … t = [ ].
     451#S #st1 #st2 #t elim t [//] #s1 #s2 #s3 #l #prf #tl #IH * [2: * #ABS @⊥ @ABS % ]
     452#H inversion H
     453[#s #cl #EQ1 #EQ2 #EQ3 destruct] #s1' #s2' #s3' #prf' #tl' #cl' #Htl #_ #EQ1 #EQ2 #EQ3
     454destruct #_ @IH % assumption
     455qed.
     456
     457lemma get_cost_label_append : ∀S : abstract_status.∀st1,st2,st3 : S.
     458∀t1 : raw_trace … st1 st2. ∀t2 : raw_trace … st2 st3.
     459get_costlabels_of_trace … (t1 @ t2) =
     460 append … (get_costlabels_of_trace … t1) (get_costlabels_of_trace … t2).
     461#S #st1 #st2 #st3 #t1 elim t1 [ #st #t2 % ] #st1' #st2' #st3' *
     462[#f * #l | * [| * #l] | *  [| #l] ] #prf #tl #IH #t2 normalize try @eq_f @IH
     463qed.
     464 
Note: See TracChangeset for help on using the changeset viewer.