Ignore:
Timestamp:
Feb 23, 2013, 5:05:03 PM (7 years ago)
Author:
campbell
Message:

It's easier to keep the real function identifier in front-end Callstates
than mucking around with the function pointer.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/Measurable.ma

    r2685 r2722  
    394394 *)
    395395
    396 definition observables : ∀FE:fullexec io_out io_in. program … FE → nat → nat → option ((list trace) × (list trace)) ≝
    397 λFE,p,m,n.
    398   let trace ≝ exec_inf … FE p in
    399   match split_trace … trace m with
    400   [ Some x ⇒
    401     let 〈prefix,suffix〉 ≝ x in
    402     match split_trace … suffix n with
    403     [ Some y ⇒
    404       let interesting ≝ \fst y in
    405       Some ? 〈map … (fst ??) prefix, map … (fst ??) interesting〉
    406     | _ ⇒ None ?
    407     ]
    408   | _ ⇒ None ?
    409   ].
    410 
    411 definition state_at : ∀FE:fullexec io_out io_in. ∀p:program … FE. nat → option (state … FE (make_global … p)) ≝
    412 λFE,p,m.
    413   let trace ≝ exec_inf … FE p in
    414   match split_trace … trace m with
    415   [ Some x ⇒
    416     match \snd x with
    417     [ e_step _ s _ ⇒ Some ? s
    418     | e_stop _ _ s ⇒ Some ? s
    419     | _ ⇒ None ?
    420     ]
    421   | _ ⇒ None ?
    422   ].
     396definition observables : ∀C:preclassified_system. program ?? C → nat → nat → res ((list intensional_event) × (list intensional_event)) ≝
     397λC,p,m,n.
     398  let g ≝ make_global … (pcs_exec … C) p in
     399  let C' ≝ pcs_to_cs C g in
     400  ! s0 ← make_initial_state … p;
     401  ! 〈prefix,s1〉 ← exec_steps m ?? (cs_exec … C') g s0;
     402  ! 〈interesting,s2〉 ← exec_steps m ?? (cs_exec … C') g s1;
     403  let 〈cs,prefix'〉 ≝ intensional_trace_of_trace C' [ ] prefix in
     404  return 〈prefix', \snd (intensional_trace_of_trace C' cs interesting)〉.
     405
Note: See TracChangeset for help on using the changeset viewer.