Changeset 2502 for src/common


Ignore:
Timestamp:
Nov 29, 2012, 11:59:34 AM (7 years ago)
Author:
campbell
Message:

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

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/Measurable.ma

    r2486 r2502  
    1313λC. state … C (cs_global … C).
    1414
    15 definition execution_prefix : classified_system → Type[0] ≝ λC. list (trace × (cs_state C)).
     15definition execution_prefix : Type[0] → Type[0] ≝ λstate. list (trace × state).
    1616
    17 let rec split_trace C (x:execution (cs_state C) io_out io_in) (n:nat) on n : option (execution_prefix C × (execution (cs_state C) io_out io_in)) ≝
     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)) ≝
    1818match n with
    1919[ O ⇒ Some ? 〈[ ], x〉
     
    2121  match x with
    2222  [ e_step tr s x' ⇒
    23     ! 〈pre,x''〉 ← split_trace C x' n';
     23    ! 〈pre,x''〉 ← split_trace FE g x' n';
    2424    Some ? 〈〈tr,s〉::pre,x''〉
    2525  | _ ⇒ None ?
     
    2727].
    2828
    29 definition trace_labelled : ∀C. execution_prefix C → Prop ≝
     29definition trace_labelled : ∀C. execution_prefix (cs_state … C) → Prop ≝
    3030λ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).
    3131
    32 definition measure_stack : ∀C. execution_prefix C → nat × nat ≝
     32definition measure_stack : ∀C. execution_prefix (cs_state … C) → nat × nat ≝
    3333λC.
    3434  foldl … (λx, trs.
     
    4343    〈new, max max_stack new〉) 〈0,0〉.
    4444
    45 definition stack_after : ∀C. execution_prefix C → nat ≝
     45definition stack_after : ∀C. execution_prefix (cs_state … C) → nat ≝
    4646λC,x. \fst (measure_stack C x).
    4747
    48 definition max_stack : ∀C. execution_prefix C → nat ≝
     48definition max_stack : ∀C. execution_prefix (cs_state … C) → nat ≝
    4949λC,x. \snd (measure_stack C x).
    5050
    5151let rec will_return_aux C (depth:nat)
    52                         (trace:execution_prefix C) on trace : bool ≝
     52                        (trace:execution_prefix (cs_state … C)) on trace : bool ≝
    5353match trace with
    5454[ nil ⇒ match depth with [ O ⇒ true | _ ⇒ false ]
     
    6565  ]
    6666].
    67 definition will_return' : ∀C. execution_prefix C → bool ≝ λC. will_return_aux C O.
     67definition will_return' : ∀C. execution_prefix (cs_state … C) → bool ≝ λC. will_return_aux C O.
    6868
    6969record preclassified_system : Type[2] ≝ {
     
    8080  let C' ≝ mk_classified_system (pcs_exec C) (make_global … p) (pcs_labelled C ?) (pcs_classify C ?) stack_cost in
    8181  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〉 ∧
     82  split_trace C' ? cl_trace m = Some ? 〈prefix,suffix〉 ∧
     83  split_trace C' ? suffix n = Some ? 〈interesting,remainder〉 ∧
    8484  trace_labelled C' interesting ∧
    8585  bool_to_Prop (will_return' C' interesting) ∧
    8686  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 TracChangeset for help on using the changeset viewer.