Changeset 2914 for src/RTLabs/MeasurableToStructured.ma
 Timestamp:
 Mar 20, 2013, 8:39:37 AM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/RTLabs/MeasurableToStructured.ma
r2897 r2914 130 130 (λg,s. RTLabs_classify (Ras_state … s)) 131 131 (λ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)).139 132 140 133 lemma will_return_equiv : ∀ge,trace,depth,n,s,s',EX. … … 731 724 ] qed. 732 725 726 definition 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 733 730 734 731 … … 743 740 measurable RTLabs_pcsys p m n stack_cost max → 744 741 observables RTLabs_pcsys p m n = return 〈prefix,interesting〉 → 745 let midstack ≝ \fst (measure_stack stack_cost 0 prefix)in742 let midstack ≝ measure_stack stack_cost (mk_stacksize_info 0 0) prefix in 746 743 ∃sm,sn,fn.∃tlr:trace_label_return (RTLabs_status (make_global p)) sm sn. 747 744 state_at RTLabs_ext_pcsys p m = return sm ∧ 748 745 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 ∧ 750 747 pi1 … (observables_trace_label_return (RTLabs_status (make_global p)) sm sn tlr fn) = interesting. 751 748 #p #m #n #stack_cost #max #prefix #interesting
Note: See TracChangeset
for help on using the changeset viewer.