 Timestamp:
 Mar 24, 2013, 9:17:42 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/RTLabs/MeasurableToStructured.ma
r2947 r2948 280 280 ] 281 281 ] qed. 282 283 282 283 lemma callee_ext : ∀ge,s,S,M. 284 cs_callee (pcs_to_cs RTLabs_pcsys ge) s = cs_callee (pcs_to_cs RTLabs_ext_pcsys ge) (mk_RTLabs_ext_state ge s S M). 285 #ge * // 286 qed. 287 288 lemma int_state_change_ext : ∀ge,cs,s,S,M. 289 intensional_state_change (pcs_to_cs RTLabs_pcsys ge) cs s = 290 intensional_state_change (pcs_to_cs RTLabs_ext_pcsys ge) cs (mk_RTLabs_ext_state ge s S M). 291 #ge #cs #s #S #M 292 whd in ⊢ (??%%); 293 <callee_ext % 294 qed. 295 284 296 lemma extend_RTLabs_exec_steps : ∀ge,n. ∀s:RTLabs_ext_state ge. ∀trace,s'.∀cs,cs',itrace. 285 297 exec_steps n … RTLabs_fullexec ge (Ras_state … s) = return 〈trace,s'〉 → … … 288 300 ∃trace',S,M. 289 301 exec_steps n … RTLabs_ext_fullexec ge s = return 〈trace',mk_RTLabs_ext_state … s' S M〉 ∧ 302 intensional_trace_of_trace (pcs_to_cs … RTLabs_ext_pcsys ge) cs trace' = 〈cs',itrace〉 ∧ 290 303 All2 ?? (λb,id. symbol_for_block ? ge b = Some ? id) S (\fst (intensional_state_change (pcs_to_cs … RTLabs_pcsys ge) cs' s')). 291 304 #ge #n0 elim n0 … … 293 306 #E whd in E:(??%%); destruct 294 307 #CS %{[ ]} 295 %{S} %{M} % [ %  @CS ]308 %{S} %{M} % [ % [ %  % ]  @CS ] 296 309  #n #IH * #s #S #M #trace #s' #cs #cs' #itrace #EX 297 310 cases (exec_steps_S … EX) #NF * #tr * #s1 * #tl * * #E #STEP #EX' … … 302 315 #S' * #M' * #STEP' #STACK' 303 316 cases (IH (mk_RTLabs_ext_state ge s1 S' M') … EX' ITOT2 STACK') 304 #tl' * #S'' * #M'' * #EX'' #STACK''317 #tl' * #S'' * #M'' * * #EX'' #ITOT'' #STACK'' 305 318 %{(〈mk_RTLabs_ext_state … s S M,tr〉::tl')} %{S''} %{M''} 306 % 319 % [ % 307 320 [ whd in ⊢ (??%?); 308 321 change with (RTLabs_is_final s) in match (is_final ?????); … … 312 325 >STEP' whd in ⊢ (??%?); 313 326 >EX'' % 314  @STACK'' 327  whd in ⊢ (??%?); <int_state_change_ext >ITOT1 328 whd in ⊢ (??%?); >ITOT'' % 329 ] @STACK'' 315 330 ] 316 331 ] qed. … … 322 337 ∃trace',S,M. 323 338 exec_steps n … RTLabs_ext_fullexec ge s = return 〈trace',mk_RTLabs_ext_state … s' S M〉 ∧ 339 intensional_trace_of_trace (pcs_to_cs … RTLabs_ext_pcsys ge) [ ] trace' = 〈cs',itrace〉 ∧ 324 340 All2 ?? (λb,id. symbol_for_block ? ge b = Some ? id) S (\fst (intensional_state_change (pcs_to_cs … RTLabs_pcsys ge) cs' s')). 325 341 #p #n #s #trace #s' #cs' #itrace #EXEC #ITOT #INIT … … 724 740 ] qed. 725 741 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 742 (* TODO: move to somewhere common *) 743 definition exec_steps_with_obs : ∀C:preclassified_system. ∀p:program ?? C. nat → res ((state … C (make_global … C p)) × (list intensional_event)) ≝ 744 λC,p,m. 745 let g ≝ make_global … (pcs_exec … C) p in 746 let C' ≝ pcs_to_cs C g in 747 ! s0 ← make_initial_state … p; 748 ! 〈prefix,s1〉 ← exec_steps m ?? (cs_exec … C') g s0; 749 return 〈s1, \snd (intensional_trace_of_trace C' [ ] prefix)〉. 730 750 731 751 … … 740 760 measurable RTLabs_pcsys p m n stack_cost max → 741 761 observables RTLabs_pcsys p m n = return 〈prefix,interesting〉 → 742 let midstack ≝ measure_stack stack_cost (mk_stacksize_info 0 0) prefix in743 762 ∃sm,sn,fn.∃tlr:trace_label_return (RTLabs_status (make_global p)) sm sn. 744 state_at RTLabs_ext_pcsys p m = return sm∧763 exec_steps_with_obs RTLabs_ext_pcsys p m = return 〈sm, prefix〉 ∧ 745 764 tlr_unrepeating (RTLabs_status (make_global p)) … tlr ∧ 746 le (maximum ( max_stack_of_tlr ??? tlr stack_cost fn midstack)) max ∧765 le (maximum (update_stacksize_info stack_cost (mk_stacksize_info 0 0) (extract_call_ud_from_observables (prefix@interesting)))) max ∧ 747 766 pi1 … (observables_trace_label_return (RTLabs_status (make_global p)) sm sn tlr fn) = interesting. 748 767 #p #m #n #stack_cost #max #prefix #interesting … … 752 771 * #s0 * #prefix' * #s1 * #interesting' * #s2 753 772 letin ge ≝ (make_global … RTLabs_fullexec p) 754 * * * * * #INIT #EXEC1 #EXEC2 #LABEL_TO_RETURN #RETURNS # STACK773 * * * * * #INIT #EXEC1 #EXEC2 #LABEL_TO_RETURN #RETURNS #MAXSTACK 755 774 whd in ⊢ (??%? → ?); >INIT 756 775 whd in ⊢ (??%? → ?); >EXEC1 … … 764 783 cases (initial_states_OK' … INIT) #S * #M #INIT' 765 784 cases (extend_initial_RTLabs_exec_steps ?? (mk_RTLabs_ext_state (make_global p) s0 S M) … EXEC1 ITOT1 INIT') 766 #prefix'' * #S1 * #M1 * 785 #prefix'' * #S1 * #M1 * * 767 786 lapply (label_to_return_state_labelled … LABEL_TO_RETURN EXEC2) #CS1 768 787 lapply (cost_state_is_in_function ge s1 S1 M1 CS1) * #fnb * #S1' * #fn * #ES1 #FN destruct 769 letin s1' ≝ (mk_RTLabs_ext_state ? s1 (fnb::S1') M1) #EXEC1' # CALLSTACK1788 letin s1' ≝ (mk_RTLabs_ext_state ? s1 (fnb::S1') M1) #EXEC1' #ITOT1' #CALLSTACK1 770 789 cut (∃cs1'. cs1 = fn::cs1') 771 790 [ >(cost_state_intensional_state_change … CS1) in CALLSTACK1; … … 788 807 change with (make_ext_initial_state p) in match (make_initial_state ????); 789 808 >INIT' whd in ⊢ (??%?); 790 >EXEC1' %809 >EXEC1' whd in ⊢ (??%?); >ITOT1' % 791 810  @tlr_sound_unrepeating 792 811 [ @SLge … … 796 815 ] 797 816 ] 798 ] 817 ] >int_trace_append' in MAXSTACK; >ITOT1 normalize nodelta >ITOT2 @(λx.x) 799 818 ] cut (length_tlr … tlr = n) 800 819 [ lapply (make_flat_trace_length ????? EXEC2) <LEN … … 804 823 * // 805 824 ] 806 ] 807 825 ] qed. 826
Note: See TracChangeset
for help on using the changeset viewer.