 Timestamp:
 Nov 24, 2011, 12:12:32 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/RTLabs/Traces.ma
r1537 r1552 3 3 include "common/StructuredTraces.ma". 4 4 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. 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). 17 22 18 23 definition RTLabs_status : genv → abstract_status ≝ … … 21 26 state 22 27 (λs,s'. ∃t. eval_statement ge s = Value ??? 〈t,s'〉) 23 (λs,c. RTLabs_classify s = c) 28 RTLabs_classify 29 RTLabs_cost 24 30 (λs,s'. match s with 25 31 [ dp s p ⇒ 26 match s return λs. RTLabs_classify s =cl_call → ? with32 match s return λs. RTLabs_classify s cl_call → ? with 27 33 [ Callstate fd args dst stk m ⇒ 28 34 λ_. match s' with … … 34 40 ] p 35 41 ]). 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. 42 inversion H try #a try #b try #c try #d try #e try #f destruct 43 qed.
Note: See TracChangeset
for help on using the changeset viewer.