source: src/common/Measurable.ma @ 2502

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

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

File size: 4.3 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
75definition measurable : ∀C:preclassified_system.
76  ∀p:program ?? C. nat → nat →
77  (∀s. match pcs_classify … (make_global … p) s with  [ cl_call ⇒ True | cl_return ⇒ True | _ ⇒ False ] → nat) →
78  nat → Prop ≝
79λC,p,m,n,stack_cost,max_allowed_stack.  ∀prefix,suffix,interesting,remainder.
80  let C' ≝ mk_classified_system (pcs_exec C) (make_global … p) (pcs_labelled C ?) (pcs_classify C ?) stack_cost in
81  let cl_trace ≝ exec_inf … (cs_exec … C') p in
82  split_trace C' ? cl_trace m = Some ? 〈prefix,suffix〉 ∧
83  split_trace C' ? suffix n = Some ? 〈interesting,remainder〉 ∧
84  trace_labelled C' interesting ∧
85  bool_to_Prop (will_return' C' interesting) ∧
86  le (max_stack C' (prefix@interesting)) max_allowed_stack.
87
88(* TODO: probably ought to be elsewhere
89
90   Note that this does not include stack space
91 *)
92
93definition observables : ∀FE:fullexec io_out io_in. program … FE → nat → nat → option ((list trace) × (list trace)) ≝
94λFE,p,m,n.
95  let trace ≝ exec_inf … FE p in
96  match split_trace FE ? trace m with
97  [ Some x ⇒
98    let 〈prefix,suffix〉 ≝ x in
99    match split_trace FE ? suffix n with
100    [ Some y ⇒
101      let interesting ≝ \fst y in
102      Some ? 〈map … (fst ??) prefix, map … (fst ??) interesting〉
103    | _ ⇒ None ?
104    ]
105  | _ ⇒ None ?
106  ].
107
108definition state_at : ∀FE:fullexec io_out io_in. ∀p:program … FE. nat → option (state … FE (make_global … p)) ≝
109λFE,p,m.
110  let trace ≝ exec_inf … FE p in
111  match split_trace FE ? trace m with
112  [ Some x ⇒
113    match \snd x with
114    [ e_step _ s _ ⇒ Some ? s
115    | e_stop _ _ s ⇒ Some ? s
116    | _ ⇒ None ?
117    ]
118  | _ ⇒ None ?
119  ].
Note: See TracBrowser for help on using the repository browser.