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

Line  

1  

2  include "RTLabs/semantics.ma". 

3  include "common/StructuredTraces.ma". 

4  

5  discriminator status_class. 

6  

7  (* NB: we do not consider jumps in the traces of RTLabs programs. *) 

8  

9  inductive 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  

15  inductive RTLabs_stmt_cost : statement → Prop ≝ 

16   stmt_cost : ∀c,l. RTLabs_stmt_cost (St_cost c l). 

17  

18  inductive 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  

23  definition RTLabs_status : genv → abstract_status ≝ 

24  λge. 

25  mk_abstract_status 

26  state 

27  (λs,s'. ∃t. eval_statement ge s = Value ??? 〈t,s'〉) 

28  RTLabs_classify 

29  RTLabs_cost 

30  (λs,s'. match s with 

31  [ dp s p ⇒ 

32  match s return λs. RTLabs_classify s cl_call → ? with 

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  ]). 

42  inversion H try #a try #b try #c try #d try #e try #f destruct 

43  qed. 

Note: See
TracBrowser
for help on using the repository browser.