Changeset 1552 for src/RTLabs/Traces.ma


Ignore:
Timestamp:
Nov 24, 2011, 12:12:32 PM (8 years ago)
Author:
campbell
Message:

Update RTLabs structured trace definition.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/Traces.ma

    r1537 r1552  
    33include "common/StructuredTraces.ma".
    44
    5 definition RTLabs_classify ≝
    6     (λs. match s with
    7          [ State f fs m ⇒
    8              match lookup_present ?? (f_graph (func f)) (next f) ? with
    9              [ St_cost _ _ ⇒ cl_cost
    10              | _ ⇒ cl_nocost
    11              ]
    12          | Callstate _ _ _ _ _ ⇒ cl_call
    13          | Returnstate _ _ _ _ ⇒ cl_return
    14          ]).
    15 @(next_ok f)
    16 qed.
     5discriminator status_class.
     6
     7(* NB: we do not consider jumps in the traces of RTLabs programs. *)
     8
     9inductive RTLabs_classify : state → status_class → Prop ≝
     10| rtla_other : ∀f,fs,m.    RTLabs_classify (State f fs m)        cl_other
     11| rtla_call  : ∀a,b,c,d,e. RTLabs_classify (Callstate a b c d e) cl_call
     12| rtla_ret   : ∀a,b,c,d.   RTLabs_classify (Returnstate a b c d) cl_return
     13.
     14
     15inductive RTLabs_stmt_cost : statement → Prop ≝
     16| stmt_cost : ∀c,l. RTLabs_stmt_cost (St_cost c l).
     17
     18inductive RTLabs_cost : state → Prop ≝
     19| cost_instr : ∀f,fs,m.
     20    RTLabs_stmt_cost (lookup_present ?? (f_graph (func f)) (next f) (next_ok f)) →
     21    RTLabs_cost (State f fs m).
    1722
    1823definition RTLabs_status : genv → abstract_status ≝
     
    2126    state
    2227    (λs,s'. ∃t. eval_statement ge s = Value ??? 〈t,s'〉)
    23     (λs,c. RTLabs_classify s = c)
     28    RTLabs_classify
     29    RTLabs_cost
    2430    (λs,s'. match s with
    2531      [ dp s p ⇒
    26         match s return λs. RTLabs_classify s = cl_call → ? with
     32        match s return λs. RTLabs_classify s cl_call → ? with
    2733        [ Callstate fd args dst stk m ⇒
    2834          λ_. match s' with
     
    3440        ] p
    3541      ]).
    36 [ normalize in H; destruct
    37 | cases f * #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 #H13 #H14 #H15
    38   whd in H:(??%?); cases (lookup_present LabelTag statement (f_graph (func f)) (next f) ?) in H;
    39   normalize try #a try #b try #c try #d try #e try #g try #h
    40   destruct
    41 ] qed.
     42inversion H try #a try #b try #c try #d try #e try #f destruct
     43qed.
Note: See TracChangeset for help on using the changeset viewer.