source: src/RTLabs/MeasurableTraces.ma @ 2502

Last change on this file since 2502 was 2502, checked in by campbell, 8 years ago

Sketch a little about how measurable traces might work with RTLabs and
structured traces.

File size: 1.6 KB
Line 
1include "common/Measurable.ma".
2include "RTLabs/Traces.ma".
3
4definition RTLabs_system : preclassified_system ≝
5mk_preclassified_system
6  RTLabs_fullexec
7  (λ_.RTLabs_cost)
8  (λ_. RTLabs_classify).
9
10notation "hbox(‘ ident i ’)" non associative with precedence 90 for @{ (let (${ident i} : unit) ≝ it in ?) }.
11notation "hbox(‘ ident i : t ’)" non associative with precedence 90 for @{ (let (${ident i} : unit) ≝ it in (? : $t)) }.
12
13(* The start and end states are existentially quantified because the states
14   need to be extended with the shadow stack of functions.  (I'm not sure that
15   was such a great idea now...) *)
16
17(* XXX: split of observables seem arbitrary *)
18
19theorem measurable_structured_trace : ∀p,m,n,stack_cost,max_stack,obs_pre,obs.
20  measurable RTLabs_system p m n stack_cost max_stack →
21  observables RTLabs_fullexec p m n = Some ? 〈obs_pre,obs〉 →
22  ∃start,end:RTLabs_ext_state (make_global … p).
23    state_at … RTLabs_system p m = Some state start →
24    state_at … RTLabs_system p n = Some state end →
25  ∃tlr:trace_label_return (RTLabs_status (make_global … p)) start end.
26    obs = ‘obs’ tlr.
27
28(* XXX: need some assumption on start to kick off further simulations, presumably
29   from the execution of the prefix? *)
30
31(*
32  There is no clock in the states of rtlabs, instead it's extracted from the
33  whole trace.  Might not match up well with asm?
34 
35  i.e., do we build the clock into the semantics so that it appears in the
36  structured trace (or equiv, use an instrumented semantics), or use the time
37  implict from the observables?
38*)
Note: See TracBrowser for help on using the repository browser.