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
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
47inductive ActionLabel : Type[0] ≝
48 | call_act : FunctionName → (CallCostLabel + NonFunctionalLabel) → ActionLabel
49 | ret_act : option(ReturnPostCostLabel + NonFunctionalLabel) → ActionLabel
50 | cost_act : list NonFunctionalLabel → ActionLabel.
51 
52definition is_cost_label : ActionLabel → Prop ≝
53λact.match act with [ cost_act nf ⇒ True | _ ⇒ False ].
54
55inductive status_class : Type[0] ≝
56 | cl_jump : status_class
57 | cl_io : status_class
58 | cl_other : status_class.
59
60record 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 
68inductive 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
74definition is_cost_act : ActionLabel → Prop ≝
75λact.∃l.act = cost_act l.
76
77definition is_call_act : ActionLabel → Prop ≝
78λact.∃f,l.act = call_act f l.
79
80definition is_labelled_ret_act : ActionLabel → Prop ≝
81λact.∃l.act = ret_act (Some ? l).
82
83definition is_non_silent_cost_act : ActionLabel → Prop ≝
84λact. ∃hd,tl. act = cost_act (hd::tl).
85
86inductive 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
98let 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 ≝
100match t1
101return λst1,st2,tr.raw_trace S st2 st3 → raw_trace S st1 st3
102with
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
107interpretation "trace_append" 'append t1 t2 = (append_on_trace ???? t1 t2).
108
109lemma 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 %
114qed.
115(*
116inductive 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*)
132inductive 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
161definition 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
167inductive 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.