source: src/RTLabs/Traces.ma @ 1552

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

Update RTLabs structured trace definition.

File size: 1.4 KB
RevLine 
[1537]1
2include "RTLabs/semantics.ma".
3include "common/StructuredTraces.ma".
4
[1552]5discriminator status_class.
[1537]6
[1552]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).
22
[1537]23definition RTLabs_status : genv → abstract_status ≝
24λge.
25  mk_abstract_status
26    state
27    (λs,s'. ∃t. eval_statement ge s = Value ??? 〈t,s'〉)
[1552]28    RTLabs_classify
29    RTLabs_cost
[1537]30    (λs,s'. match s with
31      [ dp s p ⇒
[1552]32        match s return λs. RTLabs_classify s cl_call → ? with
[1537]33        [ Callstate fd args dst stk m ⇒
34          λ_. match s' with
35          [ State f fs m ⇒ match stk with [ nil ⇒ False | cons h t ⇒ next h = next f ]
36          | _ ⇒ False
37          ]
38        | State f fs m ⇒ λH.⊥
39        | _ ⇒ λH.⊥
40        ] p
41      ]).
[1552]42inversion H try #a try #b try #c try #d try #e try #f destruct
43qed.
Note: See TracBrowser for help on using the repository browser.