Changeset 2795 for src


Ignore:
Timestamp:
Mar 7, 2013, 9:31:40 AM (7 years ago)
Author:
sacerdot
Message:

Added new function Measurable.observe_all_in_measurable to be used to
debug the extracted code. It takes a classified system, a state, a number s
(that in the extracted code can be a lazy infinite value) and it computes
the stream of intensional observables from that state.

Location:
src/common
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/common/ErrorMessages.ma

    r2751 r2795  
    6969 | TerminatedEarly : ErrorMessage
    7070 | BadCostLabelling : ErrorMessage
    71  | RepeatedCostLabel : ErrorMessage.
     71 | RepeatedCostLabel : ErrorMessage
     72 | NotTerminated : ErrorMessage.
  • src/common/Measurable.ma

    r2756 r2795  
    400400  return 〈prefix', \snd (intensional_trace_of_trace C' cs interesting)〉.
    401401
     402(* CSC: Main debug function for the extracted code.
     403   It returns the list of all observed states and their observables,
     404   the last state and the reason for stopping execution. If the last
     405   state is final, it also returns the exit value. *)
     406let rec observe_all_in_measurable (n:nat) (fx:classified_system)
     407 (observe: intensional_event → unit) (callstack: list ident)
     408 (s:state … fx (cs_global fx)) :
     409 list intensional_event × (res int) ≝
     410match n with
     411[ O ⇒
     412  let res ≝
     413   match is_final … fx (cs_global … fx) s with
     414   [ Some r ⇒ OK … r
     415   | None ⇒ Error … (msg NotTerminated) ]
     416  in
     417   〈[ ],res〉
     418| S m ⇒
     419  match is_final … fx (cs_global … fx) s with
     420  [ Some r ⇒ 〈[ ],OK … r〉
     421  | None ⇒
     422    match step … fx (cs_global … fx) s with
     423    [ Value trs ⇒
     424        let costevents ≝ flatten ? (map … intensional_event_of_event (\fst trs)) in
     425        let 〈callstack,callevent〉 ≝
     426         match cs_classify fx s
     427         return λy. (match y with [cl_call ⇒ True | _ ⇒ False] → ident) →
     428                 list ident × (list intensional_event)
     429         with
     430         [ cl_call ⇒
     431            λcallee. let id ≝ callee I in
     432            〈id::callstack,[IEVcall id]〉
     433         | cl_return ⇒ λ_.
     434            match callstack with
     435            [ nil ⇒ 〈[ ],[ ]〉
     436            | cons id tl ⇒ 〈tl,[IEVret id]〉]
     437         | _ ⇒ λ_. 〈callstack, [ ]〉
     438         ] (cs_callee fx s) in
     439        let events ≝ costevents@callevent in
     440        let dummy : list unit ≝ map ?? observe events in
     441        let 〈tl,res〉 ≝
     442         observe_all_in_measurable m fx observe callstack (\snd trs) in
     443         〈events@tl,res〉
     444    | Interact _ _ ⇒ 〈[ ],Error … (msg UnexpectedIO)〉
     445    | Wrong m ⇒ 〈[ ],Error … m〉
     446    ]
     447  ]
     448].
Note: See TracChangeset for help on using the changeset viewer.