source: src/common/Measurable.ma @ 2511

Last change on this file since 2511 was 2511, checked in by campbell, 7 years ago

Conjecture main Cminor/RTLabs simulation results.
Add a few notes about measurable traces.

File size: 4.6 KB
Line 
1include "common/Executions.ma".
2include "common/StructuredTraces.ma".  (* just for status_class *)
3
4record classified_system : Type[2] ≝ {
5  cs_exec :> fullexec io_out io_in;
6  cs_global : global … cs_exec;
7  cs_labelled : state … cs_exec cs_global → bool;
8  cs_classify : state … cs_exec cs_global → status_class;
9  cs_stack : ∀s. match cs_classify … s with [ cl_call ⇒ True | cl_return ⇒ True | _ ⇒ False ] → nat
10}.
11
12definition cs_state : classified_system → Type[0] ≝
13λC. state … C (cs_global … C).
14
15definition execution_prefix : Type[0] → Type[0] ≝ λstate. list (trace × state).
16
17let rec split_trace FE (g:global io_out io_in FE) (x:execution (state ?? FE g) io_out io_in) (n:nat) on n : option (execution_prefix (state … FE g) × (execution (state ?? FE g) io_out io_in)) ≝
18match n with
19[ O ⇒ Some ? 〈[ ], x〉
20| S n' ⇒
21  match x with
22  [ e_step tr s x' ⇒
23    ! 〈pre,x''〉 ← split_trace FE g x' n';
24    Some ? 〈〈tr,s〉::pre,x''〉
25  | _ ⇒ None ?
26  ]
27].
28
29definition trace_labelled : ∀C. execution_prefix (cs_state … C) → Prop ≝
30λC,x. ∃tr1,s1,x',tr2,s2. x = 〈tr1,s1〉::(x'@[〈tr2,s2〉]) ∧ bool_to_Prop (cs_labelled C s1) ∧ bool_to_Prop (cs_labelled C s2).
31
32definition measure_stack : ∀C. execution_prefix (cs_state … C) → nat × nat ≝
33λC.
34  foldl … (λx, trs.
35    let 〈current,max_stack〉 ≝ x in
36    let 〈tr,s〉 ≝ trs in
37    let new ≝
38      match cs_classify C s return λcl. (match cl in status_class with [_⇒?] → ?) → ?  with
39      [ cl_call ⇒ λsc. current + sc I
40      | cl_return ⇒ λsc. current - sc I
41      | _ ⇒ λ_. current
42      ] (cs_stack C s) in
43    〈new, max max_stack new〉) 〈0,0〉.
44
45definition stack_after : ∀C. execution_prefix (cs_state … C) → nat ≝
46λC,x. \fst (measure_stack C x).
47
48definition max_stack : ∀C. execution_prefix (cs_state … C) → nat ≝
49λC,x. \snd (measure_stack C x).
50
51let rec will_return_aux C (depth:nat)
52                        (trace:execution_prefix (cs_state … C)) on trace : bool ≝
53match trace with
54[ nil ⇒ match depth with [ O ⇒ true | _ ⇒ false ]
55| cons h tl ⇒
56  let 〈tr,s〉 ≝ h in
57  match cs_classify C s with
58  [ cl_call ⇒ will_return_aux C (S depth) tl
59  | cl_return ⇒
60      match depth with
61      [ O ⇒ false
62      | S d ⇒ will_return_aux C d tl
63      ]
64  | _ ⇒ will_return_aux C depth tl
65  ]
66].
67definition will_return' : ∀C. execution_prefix (cs_state … C) → bool ≝ λC. will_return_aux C O.
68
69record preclassified_system : Type[2] ≝ {
70  pcs_exec :> fullexec io_out io_in;
71  pcs_labelled : ∀g. state … pcs_exec g → bool;
72  pcs_classify : ∀g. state … pcs_exec g → status_class
73}.
74
75(* FIXME: this definition is unreasonable because it presumes we can easily
76   identify the change in stack usage from return states, but that information
77   is rather implicit (we only really record the function called in the
78   extended RTLabs states when building the structured traces). *)
79
80definition measurable : ∀C:preclassified_system.
81  ∀p:program ?? C. nat → nat →
82  (∀s. match pcs_classify … (make_global … p) s with  [ cl_call ⇒ True | cl_return ⇒ True | _ ⇒ False ] → nat) →
83  nat → Prop ≝
84λC,p,m,n,stack_cost,max_allowed_stack.  ∀prefix,suffix,interesting,remainder.
85  let C' ≝ mk_classified_system (pcs_exec C) (make_global … p) (pcs_labelled C ?) (pcs_classify C ?) stack_cost in
86  let cl_trace ≝ exec_inf … (cs_exec … C') p in
87  split_trace C' ? cl_trace m = Some ? 〈prefix,suffix〉 ∧
88  split_trace C' ? suffix n = Some ? 〈interesting,remainder〉 ∧
89  trace_labelled C' interesting ∧
90  bool_to_Prop (will_return' C' interesting) ∧
91  le (max_stack C' (prefix@interesting)) max_allowed_stack.
92
93(* TODO: probably ought to be elsewhere
94
95   Note that this does not include stack space
96 *)
97
98definition observables : ∀FE:fullexec io_out io_in. program … FE → nat → nat → option ((list trace) × (list trace)) ≝
99λFE,p,m,n.
100  let trace ≝ exec_inf … FE p in
101  match split_trace FE ? trace m with
102  [ Some x ⇒
103    let 〈prefix,suffix〉 ≝ x in
104    match split_trace FE ? suffix n with
105    [ Some y ⇒
106      let interesting ≝ \fst y in
107      Some ? 〈map … (fst ??) prefix, map … (fst ??) interesting〉
108    | _ ⇒ None ?
109    ]
110  | _ ⇒ None ?
111  ].
112
113definition state_at : ∀FE:fullexec io_out io_in. ∀p:program … FE. nat → option (state … FE (make_global … p)) ≝
114λFE,p,m.
115  let trace ≝ exec_inf … FE p in
116  match split_trace FE ? trace m with
117  [ Some x ⇒
118    match \snd x with
119    [ e_step _ s _ ⇒ Some ? s
120    | e_stop _ _ s ⇒ Some ? s
121    | _ ⇒ None ?
122    ]
123  | _ ⇒ None ?
124  ].
Note: See TracBrowser for help on using the repository browser.