Ignore:
Timestamp:
Mar 20, 2013, 8:39:37 AM (7 years ago)
Author:
campbell
Message:

Use single definition for stack measurement.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/MeasurableToStructured.ma

    r2897 r2914  
    130130  (λg,s. RTLabs_classify (Ras_state … s))
    131131  (λg,s,H. RTLabs_stack_ident g (Ras_state … s) H).
    132 
    133 definition lift_some : ∀A,B:Type[0]. (A → B) → A → option B ≝
    134 λA,B,f,a. Some B (f a).
    135 
    136 definition max_stack_of_tlr : ∀S,s1,s2. trace_label_return S s1 s2 → (ident → option nat) → ident → nat → nat ≝
    137 λS,s1,s2,tlr,stack_cost,currentfn,initial.
    138   maximum (update_stacksize_info stack_cost (mk_stacksize_info initial 0) (extract_call_ud_from_tlr S s1 s2 tlr currentfn)).
    139132
    140133lemma will_return_equiv : ∀ge,trace,depth,n,s,s',EX.
     
    731724] qed.
    732725
     726definition max_stack_of_tlr : ∀S,s1,s2. trace_label_return S s1 s2 → (ident → option nat) → ident → stacksize_info → stacksize_info ≝
     727λS,s1,s2,tlr,stack_cost,currentfn,initial.
     728  update_stacksize_info stack_cost initial (extract_call_ud_from_tlr S s1 s2 tlr currentfn).
     729
    733730
    734731
     
    743740  measurable RTLabs_pcsys p m n stack_cost max →
    744741  observables RTLabs_pcsys p m n = return 〈prefix,interesting〉 →
    745   let midstack ≝ \fst (measure_stack stack_cost 0 prefix) in
     742  let midstack ≝ measure_stack stack_cost (mk_stacksize_info 0 0) prefix in
    746743  ∃sm,sn,fn.∃tlr:trace_label_return (RTLabs_status (make_global p)) sm sn.
    747744  state_at RTLabs_ext_pcsys p m = return sm ∧
    748745  tlr_unrepeating (RTLabs_status (make_global p)) … tlr ∧
    749   le (max_stack_of_tlr ??? tlr (lift_some … stack_cost) fn midstack) max ∧
     746  le (maximum (max_stack_of_tlr ??? tlr stack_cost fn midstack)) max ∧
    750747  pi1 … (observables_trace_label_return (RTLabs_status (make_global p)) sm sn tlr fn) = interesting.
    751748#p #m #n #stack_cost #max #prefix #interesting
Note: See TracChangeset for help on using the changeset viewer.