 Timestamp:
 Feb 1, 2012, 4:16:05 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/RTLabs/Traces.ma
r1670 r1671 818 818 819 819 definition termination_oracle ≝ ∀ge,depth,s,trace. 820 inhabited (will_return ge depth s trace) ⊎¬ inhabited (will_return ge depth s trace).820 inhabited (will_return ge depth s trace) ∨ ¬ inhabited (will_return ge depth s trace). 821 821 822 822 let rec finite_segment ge s n trace … … 826 826 (NO_TERMINATION: Not (∃depth. inhabited (will_return ge depth s trace))) 827 827 (LABEL_LIMIT: ∃s'. And (nth_state ge s trace (S n) = Some ? s') (RTLabs_cost s' = true)) 828 : finite_prefix ge s ≝828 on n : finite_prefix ge s ≝ 829 829 match n return λn. well_cost_labelled_state s → (Not (∃depth. inhabited (will_return ge depth s trace))) → (∃s'. nth_state ge s trace (S n) = Some ? s' ∧ RTLabs_cost s' = true) → finite_prefix ge s with 830 830 [ O ⇒ λSTATE_COSTLABELLED,NO_TERMINATION,LABEL_LIMIT. ? … … 845 845 fp_tal ge start next (tal_base_not_return (RTLabs_status ge) start next ?? ?) trace' 846 846  cl_call ⇒ λCL. 847 match ORACLE ge O next trace' with 848 [ inl TERMINATES ⇒ 849 let tlr ≝ make_label_return' ge O next trace' ENV_COSTLABELLED ??? in 850 ? 851  inr NO_TERMINATION ⇒ ? 847 match ORACLE ge O next trace' return λ_. finite_prefix ge start with 848 [ or_introl TERMINATES ⇒ 849 match TERMINATES with [ witness TERMINATES ⇒ 850 let tlr ≝ make_label_return' ge O next trace' ENV_COSTLABELLED ?? TERMINATES in 851 match RTLabs_cost (new_state … tlr) return λx. RTLabs_cost (new_state … tlr) = x → finite_prefix ge start with 852 [ true ⇒ λCS. fp_tal ge start (new_state … tlr) (tal_base_call (RTLabs_status ge) start next (new_state … tlr) ? CL ? (new_trace … tlr) CS) (remainder … tlr) 853  false ⇒ λCS. ? (* broken  we don't know the new value of n *) 854 (*let fs ≝ finite_segment ge (new_status … tlr) ?????????????? 855 fp_add_terminating_call … (new_trace … tlr) ? CS*) 856 ] (refl ??) 857 ] 858  or_intror NO_TERMINATION ⇒ 859 fp_tac ??? (tac_base (RTLabs_status ge) start CL) (ft_step io_out io_in ge start tr next EV trace') 852 860 ] 853 861  cl_return ⇒ λCL. ⊥ … … 856 864 ] 857 865 ] STATE_COSTLABELLED NO_TERMINATION LABEL_LIMIT. 858 [ 2,17: cases LABEL_LIMIT #s' * #NTH #_ whd in NTH:(??%?); destruct 859  3: @(absurd ?? NO_TERMINATION) 866 [ 867  2,17: cases LABEL_LIMIT #s' * #NTH #_ whd in NTH:(??%?); destruct 868  @(absurd ?? NO_TERMINATION) 860 869 %{0} % @wr_base // 861  4: @(well_cost_labelled_jump … EV) // 862  5,6: /2/ 863  8: @(well_cost_labelled_state_step … EV) // 864  9: @(well_cost_labelled_call … EV) // 865  10: cases TERMINATES // 870  @(well_cost_labelled_jump … EV) // 871  5,6,8: /2/ 872  873  874  @(well_cost_labelled_state_step … EV) // 875  @(well_cost_labelled_call … EV) // 866 876  12,13,14: /2/ 867  15:@(well_cost_labelled_state_step … EV) //868  16:@(not_to_not … NO_TERMINATION)869 877  @(well_cost_labelled_state_step … EV) // 878  @(not_to_not … NO_TERMINATION) 879 * #depth * #TERM %{depth} % @wr_step /2/ 870 880 ] cases daemon qed. 871 881
Note: See TracChangeset
for help on using the changeset viewer.