source: LTS/Traces.ma @ 3387

Last change on this file since 3387 was 3387, checked in by piccolo, 6 years ago

unified notation

File size: 9.2 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
15include "arithmetics/nat.ma".
16include "basics/types.ma".
17include "basics/deqsets.ma".
18include "../src/ASM/Util.ma".
19
20inductive FunctionName : Type[0] ≝
21 | a_function_id : ℕ → FunctionName.
22 
23inductive CallCostLabel : Type[0] ≝
24 | a_call_label : ℕ → CallCostLabel.
25 
26inductive ReturnPostCostLabel : Type[0] ≝
27 | a_return_cost_label : ℕ → ReturnPostCostLabel.
28 
29inductive NonFunctionalLabel : Type[0] ≝
30 | a_non_functional_label : ℕ → NonFunctionalLabel.
31 
32inductive CostLabel : Type[0] ≝
33 | a_call : CallCostLabel → CostLabel
34 | a_return_post : ReturnPostCostLabel → CostLabel
35 | a_non_functional_label : NonFunctionalLabel → CostLabel.
36
37coercion a_call.
38coercion a_return_post.
39coercion a_non_functional_label.
40
41definition 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
45coercion ret_act_label_to_cost_label.
46
47definition call_act_label_to_cost_label :
48(CallCostLabel + NonFunctionalLabel) → CostLabel ≝
49λx.match x with [inl a ⇒ a_call a | inr b ⇒ a_non_functional_label b].
50
51coercion call_act_label_to_cost_label.
52
53inductive ActionLabel : Type[0] ≝
54 | call_act : FunctionName → (CallCostLabel + NonFunctionalLabel) → ActionLabel
55 | ret_act : option(ReturnPostCostLabel + NonFunctionalLabel) → ActionLabel
56 | cost_act : option NonFunctionalLabel → ActionLabel
57 | init_act : ActionLabel.
58 
59definition is_cost_label : ActionLabel → Prop ≝
60λact.match act with [ cost_act nf ⇒ True | _ ⇒ False ].
61
62inductive status_class : Type[0] ≝
63 | cl_jump : status_class
64 | cl_io : status_class
65 | cl_other : status_class.
66
67record abstract_status : Type[2] ≝
68 { as_status :> Type[0]
69 ; as_execute : ActionLabel → relation as_status
70 ; as_syntactical_succ : relation as_status
71 ; as_classify : as_status → status_class
72 ; is_call_post_label : as_status → bool
73 ; as_initial : as_status → bool
74 ; as_final : as_status → bool
75 ; is_io_entering : NonFunctionalLabel → bool
76 ; is_io_exiting : NonFunctionalLabel → bool
77 }.
78 
79definition is_act_io_entering : abstract_status → ActionLabel → bool ≝
80λS,l.match l with
81[ call_act f c ⇒ match c with [ inl _ ⇒ false | inr c' ⇒ is_io_entering S c' ]
82| ret_act x ⇒ match x with [ Some c ⇒ match c with [inl _ ⇒ false
83                                                   | inr c' ⇒ is_io_entering S c']
84                           | None ⇒ false
85                           ]
86| cost_act x ⇒ match x with [ Some c ⇒ is_io_entering S c | None ⇒ false ]
87| init_act ⇒ false
88].
89
90definition is_act_io_exiting : abstract_status → ActionLabel → bool ≝
91λS,l.match l with
92[ call_act f c ⇒ match c with [ inl _ ⇒ false | inr c' ⇒ is_io_exiting S c' ]
93| ret_act x ⇒ match x with [ Some c ⇒ match c with [inl _ ⇒ false
94                                                   | inr c' ⇒ is_io_exiting S c']
95                           | None ⇒ false
96                           ]
97| cost_act x ⇒ match x with [ Some c ⇒ is_io_exiting S c | None ⇒ false ]
98| init_act ⇒ false
99].
100
101
102inductive raw_trace (S : abstract_status) : S → S → Type[0] ≝
103  | t_base : ∀st : S.raw_trace S st st
104  | t_ind : ∀st1,st2,st3 : S.∀l : ActionLabel.
105             as_execute S l st1 st2 → raw_trace S st2 st3 →
106             raw_trace S st1 st3.
107
108definition is_cost_act : ActionLabel → Prop ≝
109λact.∃l.act = cost_act l.
110
111definition is_call_act : ActionLabel → Prop ≝
112λact.∃f,l.act = call_act f l.
113
114definition is_labelled_ret_act : ActionLabel → Prop ≝
115λact.∃l.act = ret_act (Some ? l).
116
117definition is_unlabelled_ret_act : ActionLabel → Prop ≝
118λact.act = ret_act (None ?).
119
120definition is_non_silent_cost_act : ActionLabel → Prop ≝
121λact. ∃l. act = cost_act (Some ? l).
122
123definition is_costlabelled_act : ActionLabel → Prop ≝
124λact.match act with [ call_act _ _ ⇒ True
125                    | ret_act x ⇒ match x with [ Some _ ⇒ True | None ⇒ False ]
126                    | cost_act x ⇒ match x with [ Some _ ⇒ True | None ⇒ False ]
127                    | init_act ⇒ False
128                    ].
129
130inductive well_formed_trace (S : abstract_status) :
131   ∀st1,st2 : S.raw_trace S st1 st2 → Prop ≝
132  | wf_empty : ∀st: S.well_formed_trace … (t_base S st)
133  | wf_cons_no_jump :  ∀st1,st2,st3 : S.∀l : ActionLabel.
134                       ∀prf: as_execute S l st1 st2.∀ tl: raw_trace S st2 st3.
135                       well_formed_trace … tl → as_classify … st1 ≠ cl_jump →
136                       well_formed_trace … (t_ind … prf … tl)
137  | wf_cons_jump : ∀st1,st2,st3 : S.∀ l : ActionLabel.
138                  ∀prf : as_execute S l st1 st2.∀tl : raw_trace S st2 st3.
139                  well_formed_trace … tl → is_non_silent_cost_act l →
140                  well_formed_trace … (t_ind … prf … tl).
141
142let rec append_on_trace (S : abstract_status) (st1 : S) (st2 : S) (st3 : S)
143(t1 : raw_trace S st1 st2) on t1 : raw_trace S st2 st3 → raw_trace S st1 st3 ≝
144match t1
145return λst1,st2,tr.raw_trace S st2 st3 → raw_trace S st1 st3
146with
147[ t_base st ⇒ λt2.t2
148| t_ind st1' st2' st3' l prf tl ⇒ λt2.t_ind … prf … (append_on_trace … tl t2)
149].
150
151interpretation "trace_append" 'append t1 t2 = (append_on_trace ???? t1 t2).
152
153lemma append_associative : ∀S,st1,st2,st3,st4.
154∀t1 : raw_trace S st1 st2.∀t2 : raw_trace S st2 st3.
155∀t3 : raw_trace S st3 st4.(t1 @ t2) @ t3 = t1 @ (t2 @ t3).
156#S #st1 #st2 #st3 #st4 #t1 elim t1 -t1
157[ #st #t2 #t3 %] #st1' #st2' #st3' #l #prf #tl #IH #t2 #t3 whd in ⊢ (??%%); >IH %
158qed.
159
160definition trace_prefix: ∀S : abstract_status.∀st1,st2,st3 : S.raw_trace … st1 st2 →
161raw_trace … st1 st3 → Prop≝
162λS,st1,st2,st3,t1,t2.∃t3 : raw_trace … st2 st3.t2 = t1 @ t3.
163
164definition trace_suffix : ∀S : abstract_status.∀st1,st2,st3 : S.raw_trace … st2 st3 →
165raw_trace … st1 st3 → Prop≝
166λS,st1,st2,st3,t1,t2.∃t3 : raw_trace … st1 st2.t2 = t3 @ t1.
167
168inductive silent_trace (S : abstract_status) :
169∀st1,st2 : S.raw_trace S st1 st2 → Prop ≝
170| silent_empty : ∀st : S.silent_trace … (t_base S st)
171| silent_cons : ∀st1,st2,st3 : S.∀prf : as_execute S (cost_act (None ?)) st1 st2.
172                ∀tl : raw_trace S st2 st3. silent_trace … tl →
173                silent_trace … (t_ind … prf … tl).
174
175inductive pre_measurable_trace (S : abstract_status) :
176∀st1,st2 : S.raw_trace ? st1 st2 → Prop ≝
177 | pm_empty : ∀st : S. as_classify … st ≠ cl_io → pre_measurable_trace … (t_base ? st)
178 | pm_cons_cost_act : ∀st1,st2,st3 : S.∀l : ActionLabel.
179                      ∀prf : as_execute S l st1 st2.∀tl : raw_trace S st2 st3.
180                      as_classify … st1 ≠ cl_io → is_cost_act l → pre_measurable_trace … tl →
181                      pre_measurable_trace … (t_ind … prf … tl)
182 | pm_cons_lab_ret : ∀st1,st2,st3 : S.∀l : ActionLabel.
183                      as_classify … st1 ≠ cl_io →
184                      ∀prf : as_execute S l st1 st2.∀tl : raw_trace S st2 st3.
185                      is_labelled_ret_act l → pre_measurable_trace … tl →
186                      pre_measurable_trace … (t_ind … prf … tl)
187 | pm_cons_post_call : ∀st1,st2,st3 : S.∀l : ActionLabel.
188                      ∀prf : as_execute S l st1 st2.∀tl : raw_trace S st2 st3.
189                      as_classify … st1 ≠ cl_io → is_call_act l → is_call_post_label … st1 →
190                      pre_measurable_trace … tl →
191                      pre_measurable_trace … (t_ind … prf … tl)
192 | pm_balanced_call : ∀st1,st2,st3,st4,st5.∀l1,l2.
193                      ∀prf : as_execute S l1 st1 st2.∀t1 : raw_trace S st2 st3.
194                      ∀t2 : raw_trace S st4 st5.∀prf' : as_execute S l2 st3 st4.
195                      as_classify … st1 ≠ cl_io → as_classify … st3 ≠ cl_io
196                      →  is_call_act l1 → ¬ is_call_post_label … st1 →
197                      pre_measurable_trace … t1 → pre_measurable_trace … t2 →
198                      as_syntactical_succ S st1 st4 →
199                      is_unlabelled_ret_act l2 →
200                      pre_measurable_trace … (t_ind … prf … (t1 @ (t_ind … prf' … t2))).
Note: See TracBrowser for help on using the repository browser.