Context Navigation

source: LTS/Traces.ma @ 3380

Last change on this file since 3380 was 3380, checked in by piccolo, 6 years ago
Added definition of measurable trace
File size: 8.7 KB

Line
1	(**************************************************************************)
2	(* ___ *)
3	(* \|\|M\|\| *)
4	(* \|\|A\|\| A project by Andrea Asperti *)
5	(* \|\|T\|\| *)
6	(* \|\|I\|\| Developers: *)
7	(* \|\|T\|\| The HELM team. *)
8	(* \|\|A\|\| http://helm.cs.unibo.it *)
9	(* \ / *)
10	(* \ / This file is distributed under the terms of the *)
11	(* v GNU General Public License Version 2 *)
12	(* *)
13	(**************************************************************************)
14
15	include "arithmetics/nat.ma".
16	include "basics/types.ma".
17	include "basics/deqsets.ma".
18	include "../src/ASM/Util.ma".
19
20	inductive FunctionName : Type[0] ≝
21	\| a_function_id : ℕ → FunctionName.
22
23	inductive CallCostLabel : Type[0] ≝
24	\| a_call_label : ℕ → CallCostLabel.
25
26	inductive ReturnPostCostLabel : Type[0] ≝
27	\| a_return_cost_label : ℕ → ReturnPostCostLabel.
28
29	inductive NonFunctionalLabel : Type[0] ≝
30	\| a_non_functional_label : ℕ → NonFunctionalLabel.
31
32	inductive CostLabel : Type[0] ≝
33	\| a_call : CallCostLabel → CostLabel
34	\| a_return_post : ReturnPostCostLabel → CostLabel
35	\| a_non_functional_label : NonFunctionalLabel → CostLabel.
36
37	coercion a_call.
38	coercion a_return_post.
39	coercion a_non_functional_label.
40
41	definition ret_act_label_to_cost_label :
42	(ReturnPostCostLabel + NonFunctionalLabel) → CostLabel ≝
43	λx.match x with [inl a ⇒ a_return_post a \| inr b ⇒ a_non_functional_label b].
44
45	coercion ret_act_label_to_cost_label.
46
47	inductive ActionLabel : Type[0] ≝
48	\| call_act : FunctionName → (CallCostLabel + NonFunctionalLabel) → ActionLabel
49	\| ret_act : option(ReturnPostCostLabel + NonFunctionalLabel) → ActionLabel
50	\| cost_act : list NonFunctionalLabel → ActionLabel.
51
52	definition is_cost_label : ActionLabel → Prop ≝
53	λact.match act with [ cost_act nf ⇒ True \| _ ⇒ False ].
54
55	inductive status_class : Type[0] ≝
56	\| cl_jump : status_class
57	\| cl_io : status_class
58	\| cl_other : status_class.
59
60	record abstract_status : Type[2] ≝
61	{ as_status :> Type[0]
62	; as_execute : ActionLabel → relation as_status
63	; as_syntactical_succ : relation as_status
64	; as_classify : as_status → status_class
65	; is_call_post_label : as_status → bool
66	}.
67
68	inductive raw_trace (S : abstract_status) : S → S → Type[0] ≝
69	\| t_base : ∀st : S.raw_trace S st st
70	\| t_ind : ∀st1,st2,st3 : S.∀l : ActionLabel.
71	as_execute S l st1 st2 → raw_trace S st2 st3 →
72	raw_trace S st1 st3.
73
74	definition is_cost_act : ActionLabel → Prop ≝
75	λact.∃l.act = cost_act l.
76
77	definition is_call_act : ActionLabel → Prop ≝
78	λact.∃f,l.act = call_act f l.
79
80	definition is_labelled_ret_act : ActionLabel → Prop ≝
81	λact.∃l.act = ret_act (Some ? l).
82
83	definition is_non_silent_cost_act : ActionLabel → Prop ≝
84	λact. ∃hd,tl. act = cost_act (hd::tl).
85
86	inductive well_formed_trace (S : abstract_status) :
87	∀st1,st2 : S.raw_trace S st1 st2 → Prop ≝
88	\| wf_empty : ∀st: S.well_formed_trace … (t_base S st)
89	\| wf_cons_no_jump : ∀st1,st2,st3 : S.∀l : ActionLabel.
90	∀prf: as_execute S l st1 st2.∀ tl: raw_trace S st2 st3.
91	well_formed_trace … tl → as_classify … st1 ≠ cl_jump →
92	well_formed_trace … (t_ind … prf … tl)
93	\| wf_cons_jump : ∀st1,st2,st3 : S.∀ l : ActionLabel.
94	∀prf : as_execute S l st1 st2.∀tl : raw_trace S st2 st3.
95	well_formed_trace … tl → is_non_silent_cost_act l →
96	well_formed_trace … (t_ind … prf … tl).
97
98	let rec append_on_trace (S : abstract_status) (st1 : S) (st2 : S) (st3 : S)
99	(t1 : raw_trace S st1 st2) on t1 : raw_trace S st2 st3 → raw_trace S st1 st3 ≝
100	match t1
101	return λst1,st2,tr.raw_trace S st2 st3 → raw_trace S st1 st3
102	with
103	[ t_base st ⇒ λt2.t2
104	\| t_ind st1' st2' st3' l prf tl ⇒ λt2.t_ind … prf … (append_on_trace … tl t2)
105	].
106
107	interpretation "trace_append" 'append t1 t2 = (append_on_trace ???? t1 t2).
108
109	lemma append_associative : ∀S,st1,st2,st3,st4.
110	∀t1 : raw_trace S st1 st2.∀t2 : raw_trace S st2 st3.
111	∀t3 : raw_trace S st3 st4.(t1 @ t2) @ t3 = t1 @ (t2 @ t3).
112	#S #st1 #st2 #st3 #st4 #t1 elim t1 -t1
113	[ #st #t2 #t3 %] #st1' #st2' #st3' #l #prf #tl #IH #t2 #t3 whd in ⊢ (??%%); >IH %
114	qed.
115	(*
116	inductive balanced_trace (S : abstract_status) :
117	∀st1,st2 : S.raw_trace S st1 st2 → Prop ≝
118	\| bal_empty : ∀ st : S.balanced_trace … (t_base S st)
119	\| bal_cons_cost : ∀st1,st2,st3 : S.∀l : ActionLabel.
120	∀prf : as_execute S l st1 st2.∀tl : raw_trace S st2 st3.
121	balanced_trace … tl → is_cost_act l →
122	balanced_trace … (t_ind … prf … tl)
123	\| bal_cons_call : ∀s,st1,st2,st3,st4,f,l1,l2.
124	∀prf1 : as_execute S (call_act f l1) s st1.
125	∀t1 : raw_trace S st1 st2.∀t2 : raw_trace S st3 st4.
126	∀prf2 : as_execute S (ret_act l2) st2 st3.
127	(bool_to_Prop (is_call_post_label … s) → l2 ≠ None ?) →
128	as_syntactical_succ S s st3 →
129	balanced_trace … t1 → balanced_trace … t2 →
130	balanced_trace … (t_ind … prf1 … (t1 @ (t_ind … prf2 … t2))).
131	*)
132	inductive pre_measurable_trace (S : abstract_status) :
133	∀st1,st2 : S.raw_trace ? st1 st2 → Prop ≝
134	\| pm_empty : ∀st : S. pre_measurable_trace … (t_base ? st)
135	\| pm_cons_cost_act : ∀st1,st2,st3 : S.∀l : ActionLabel.
136	∀prf : as_execute S l st1 st2.∀tl : raw_trace S st2 st3.
137	is_cost_act l → pre_measurable_trace … tl →
138	pre_measurable_trace … (t_ind … prf … tl)
139	\| pm_cons_lab_ret : ∀st1,st2,st3 : S.∀l : ActionLabel.
140	∀prf : as_execute S l st1 st2.∀tl : raw_trace S st2 st3.
141	is_labelled_ret_act l → pre_measurable_trace … tl →
142	pre_measurable_trace … (t_ind … prf … tl)
143	\| pm_cons_post_call : ∀st1,st2,st3 : S.∀l : ActionLabel.
144	∀prf : as_execute S l st1 st2.∀tl : raw_trace S st2 st3.
145	is_call_act l → is_call_post_label … st1 →
146	pre_measurable_trace … tl →
147	pre_measurable_trace … (t_ind … prf … tl)
148	\| pm_balanced_call : ∀st1,st2,st3,st4,st5.∀l1,l2.
149	∀prf : as_execute S l1 st1 st2.∀t1 : raw_trace S st2 st3.
150	∀t2 : raw_trace S st4 st5.∀prf' : as_execute S l2 st3 st4.
151	is_call_act l1 → ¬ is_call_post_label … st1 →
152	pre_measurable_trace … t1 → pre_measurable_trace … t2 →
153	as_syntactical_succ S st1 st4 →
154	match l2 with
155	[ call_act _ _ ⇒ bool_to_Prop(is_call_post_label ? st3)
156	\| ret_act _ ⇒ True
157	\| cost_act x ⇒ match x with [ nil ⇒ False \| _ ⇒ True ]
158	]
159	→ pre_measurable_trace … (t_ind … prf … (t1 @ (t_ind … prf' … t2))).
160
161	definition starts_with_label_trace : ∀S : abstract_status.∀st1,st2 : S.raw_trace S st1 st2 → Prop ≝
162	λS,st1,st2,t.match t with
163	[ t_base st ⇒ False
164	\| t_ind st1 st2 st3 l _ _ ⇒ is_call_act l ∨ is_labelled_ret_act l ∨ is_non_silent_cost_act l
165	].
166
167	inductive ends_with_label_trace (S : abstract_status) :
168	∀st1,st2 : S.raw_trace S st1 st2 → Prop ≝
169	\| call_base : ∀st1,st2 : S.∀l : ActionLabel.∀prf : as_execute S l st1 st2.
170	is_call_act l → ends_with_label_trace … (t_ind … prf … (t_base S st2))
171	\| lab_ret_base : ∀st1,st2 : S.∀l : ActionLabel.∀prf : as_execute S l st1 st2.
172	is_labelled_ret_act l → ends_with_label_trace … (t_ind … prf … (t_base S st2))
173	\| non_silent_cost_act_base : ∀st1,st2 : S.∀l : ActionLabel.∀prf : as_execute S l st1 st2.
174	is_non_silent_cost_act l → ends_with_label_trace … (t_ind … prf … (t_base S st2))
175	\| cons : ∀st1,st2,st3 : S.∀l : ActionLabel.∀prf : as_execute S l st1 st2.
176	∀t : raw_trace S st2 st3. ends_with_label_trace … t →
177	ends_with_label_trace … (t_ind … prf … t).
178
179
180
181
182
183

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

Download in other formats:

Original Format