Changeset 1671


Ignore:
Timestamp:
Feb 1, 2012, 4:16:05 PM (6 years ago)
Author:
campbell
Message:

A little more on RTLabs infinite traces.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/Traces.ma

    r1670 r1671  
    818818
    819819definition 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).
    821821
    822822let rec finite_segment ge s n trace
     
    826826  (NO_TERMINATION: Not (∃depth. inhabited (will_return ge depth s trace)))
    827827  (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 ≝
    829829match 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
    830830[ O ⇒ λSTATE_COSTLABELLED,NO_TERMINATION,LABEL_LIMIT. ?
     
    845845            fp_tal ge start next (tal_base_not_return (RTLabs_status ge) start next ?? ?) trace'
    846846        | 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')
    852860            ]
    853861        | cl_return ⇒ λCL. ⊥
     
    856864    ]
    857865] 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)
    860869     %{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) //
    866876| 12,13,14: /2/
    867 | 15: @(well_cost_labelled_state_step … EV) //
    868 | 16: @(not_to_not … NO_TERMINATION)
    869      * #depth * #TERM %{depth} % @wr_step /2/
     877| @(well_cost_labelled_state_step … EV) //
     878| @(not_to_not … NO_TERMINATION)
     879  * #depth * #TERM %{depth} % @wr_step /2/
    870880] cases daemon qed.
    871881
Note: See TracChangeset for help on using the changeset viewer.