Changeset 3387
- Timestamp:
- Jul 23, 2013, 4:33:51 PM (8 years ago)
- Location:
- LTS
- Files:
-
- 2 edited
Legend:
- Unmodified
- Added
- Removed
-
LTS/Simulation.ma
r3386 r3387 1 1 include "Common.ma". 2 3 record relations: Type[0] ≝ 4 { Srel: status → status → Prop 5 ; Crel: status → status → Prop 2 include "Traces.ma". 3 4 record relations (S : abstract_status) : Type[0] ≝ 5 { Srel: S → S → Prop 6 ; Crel: S → S → Prop 6 7 }. 7 8 8 definition Rrel ≝ λ s,s'.9 ∀s1,s1'. succ s1 s → Crel s1 s1' → succs1' s'.10 11 record simulation_conditions : Type[0] ≝9 definition Rrel ≝ λS : abstract_status.λrel : relations S.λs,s' : S. 10 ∀s1,s1'. as_syntactical_succ S s1 s → Crel … rel s1 s1' → as_syntactical_succ S s1' s'. 11 12 record simulation_conditions (S : abstract_status) (rel : relations S) : Type[0] ≝ 12 13 { simulate_tau: 13 ∀s1,s2,s1' .14 as_execute s1 s2 (cost_act [])→15 Srel s1 s1'→16 ∃s2'. ∃t: raw_trace s1's2'.17 Srel s2 s2' ∧ silentt14 ∀s1,s2,s1' : S. 15 as_execute … (cost_act (None ?)) s1 s1'→ 16 Srel … rel s1 s2 → 17 ∃s2'. ∃t: raw_trace S s2 s2'. 18 Srel … rel s2 s2' ∧ silent_trace … t 18 19 ; simulate_label: 19 20 ∀s1,s2,l,s1'. 20 as_execute s1 s2 (cost_act [l])→21 Srel s1 s1'→22 ∃s2',s2'',s2'''. 23 ∃t1: raw_trace s1's2'.24 as_execute s2' s2'' (cost_act [l])∧25 ∃t3: raw_trace s2'' s2'''.26 Srel s2 s2''' ∧ silent t1 ∧ silentt321 as_execute S (cost_act (Some ? l)) s1 s1' → 22 Srel … rel s1 s2 → 23 ∃s2',s2'',s2'''. 24 ∃t1: raw_trace S s2 s2'. 25 as_execute … (cost_act (Some ? l)) s2' s2'' ∧ 26 ∃t3: raw_trace S s2'' s2'''. 27 Srel … rel s1' s2''' ∧ silent_trace … t1 ∧ silent_trace … t3 27 28 ; simulate_call_pl: 28 ∀s1,s2, l,s1'.29 post_labelleds1 →30 as_execute s1 s2 (call_act l)→31 Srel s1 s1'→32 ∃s2',s2'',s2'''. 33 ∃t1: raw_trace s1's2'.34 as_execute s2' s2'' (call_act l)∧35 ∃t3: raw_trace s2'' s2'''.36 Srel s2 s2''' ∧ silent t1 ∧ silentt329 ∀s1,s2,s1' : S.∀f,l. 30 is_call_post_label … s1 → 31 as_execute … (call_act f l) s1 s1' → 32 Srel … rel s1 s2 → 33 ∃s2',s2'',s2'''. 34 ∃t1: raw_trace S s2 s2'. 35 as_execute … (call_act f l) s2' s2'' ∧ 36 ∃t3: raw_trace S s2'' s2'''. 37 Srel … rel s1' s2''' ∧ silent_trace … t1 ∧ silent_trace … t3 37 38 ; simulate_ret_l: 38 ∀s1,s2, l,s1'.39 as_execute s1 s2 (ret_act (Some l))→40 Srel s1 s1'→41 ∃s2',s2'',s2'''. 42 ∃t1: raw_trace s1's2'.43 as_execute s2' s2'' (ret_act (Some l))∧44 ∃t3: raw_trace s2'' s2'''.45 Srel s2 s2''' ∧ silent t1 ∧ silentt339 ∀s1,s2,s1' : S.∀l. 40 as_execute S (ret_act (Some ? l)) s1 s1' → 41 Srel … rel s1 s2 → 42 ∃s2',s2'',s2'''. 43 ∃t1: raw_trace S s2 s2'. 44 as_execute … (ret_act (Some ? l)) s2' s2'' ∧ 45 ∃t3: raw_trace S s2'' s2'''. 46 Srel … rel s2 s2''' ∧ silent_trace … t1 ∧ silent_trace … t3 46 47 ; simulate_call_n: 47 ∀s1,s2,l,s1'. 48 as_execute s1 s2 (call_act l) → 49 ¬ post_labelled … → 50 Srel s1 s1' → 51 ∃s2',s2'',s2'''. 52 ∃t1: raw_trace s1' s2'. 53 as_execute s2' s2'' (ret_act None) ∧ 54 ∃t3: raw_trace s2'' s2'''. 55 Srel s2 s2''' ∧ silent t1 ∧ silent t3 (*???? BUG? ∧ Rrel s2 s2''*) ∧ Crel s1 s2' 48 ∀s1,s2,s1' : S.∀f,l. 49 as_execute … (call_act f l) s1 s1' → 50 ¬ is_call_post_label … s1 → 51 Srel … rel s1 s2 → 52 ∃s2',s2'',s2'''. 53 ∃t1: raw_trace S s2 s2'. 54 as_execute … (call_act f l) s2' s2'' ∧ 55 ∃t3: raw_trace S s2'' s2'''. 56 Srel … rel s1' s2''' ∧ silent_trace … t1 ∧ silent_trace … t3 57 ∧ Crel … rel s1 s2' 56 58 ; simulate_ret_n: 57 ∀s1,s2,l,s1'. 58 as_execute s1 s2 (ret_act None) → 59 Srel s1 s1' → 60 ∃s2',s2'',s2'''. 61 ∃t1: raw_trace s1' s2'. 62 as_execute s2' s2'' (ret_act None) ∧ 63 ∃t3: raw_trace s2'' s2'''. 64 Srel s2 s2''' ∧ silent t1 ∧ silent t3 ∧ Rrel s2 s2'' 59 ∀s1,s2,s1' : S. 60 as_execute … (ret_act (None ?)) s1 s1' → 61 Srel … rel s1 s2 → 62 ∃s2',s2'',s2'''. 63 ∃t1: raw_trace S s2 s2'. 64 as_execute … (ret_act (None ?)) s2' s2'' ∧ 65 ∃t3: raw_trace S s2'' s2'''. 66 Srel … rel s1' s2''' ∧ silent_trace … t1 ∧ silent_trace … t3 67 ∧ Rrel … rel s2 s2'' 65 68 }. 66 69 70 let rec get_costlabels_of_trace (S : abstract_status) (st1 : S) (st2 : S) 71 (t : raw_trace S st1 st2) on t : list CostLabel ≝ 72 match t with 73 [ t_base st ⇒ [ ] 74 | t_ind st1' st2' st3' l prf t' ⇒ 75 let tl ≝ get_costlabels_of_trace … t' in 76 match l with 77 [ call_act f c ⇒ c :: tl 78 | ret_act x ⇒ match x with 79 [ Some c ⇒ ret_act_label_to_cost_label c :: tl 80 | None ⇒ tl 81 ] 82 | cost_act x ⇒ match x with 83 [ Some c ⇒ a_non_functional_label c :: tl 84 | None ⇒ tl 85 ] 86 | init_act ⇒ tl 87 ] 88 ]. 89 90 67 91 theorem simulates_pre_mesurable: 68 ∀s1,s2. ∀τ1: raw_trace … s1 s2. 92 ∀S : abstract_status.∀rel : relations S. 93 ∀s1,s1' : S. ∀t1: raw_trace S s1 s1'. 69 94 pre_measurable_trace … t1 → 70 well_formed_trace … t1 → 71 ∀s1'. 72 S s1 s1' → 73 ∃s2'. ∃t2: raw_trace … s1' s2'. 74 pre_mesurable_trace … t2 ∧ 95 well_formed_trace … t1 → ∀s2.Srel … rel s1 s2 → 96 ∃s2'. ∃t2: raw_trace … s1' s2'. 97 pre_measurable_trace … t2 ∧ 75 98 well_formed_trace … t2 ∧ 76 |t1| = |t2| ∧ 77 S s2 s2'. 99 get_costlabels_of_trace … t1 = get_costlabels_of_trace … t2 ∧ 100 Srel … rel s2 s2'. 101 cases daemon (*TODO*) 102 qed. 78 103 79 104 (* IDEA: aggiungere stati di I/O e cambiare la semantica del linguaggio … … 89 114 as_execute … s2 so L'. *) 90 115 91 (*CSC: definire usando un record?*) 92 record L_raw_trace ≝ 93 { L_label: label 94 ; L_s1: status 95 ; L_s2: status 96 ; L_t: raw_trace … s1 s2 97 ; L_ok: ∃s0. as_execute … s0 L_s1 L_label. 98 (* o, nel caso in cui s1 sia lo stato iniziale, non serve nessun s0 99 e L e' la label init *) 116 record LR_raw_trace (S : abstract_status) : Type[0] ≝ 117 { L_label: ActionLabel 118 ; R_label : ActionLabel 119 ; LR_s1: S 120 ; LR_s2: S 121 ; LR_t : raw_trace S LR_s1 LR_s2 122 ; L_init_ok : bool_to_Prop(as_initial … LR_s1) → L_label = init_act 123 ; L_noinit_ok : 124 bool_to_Prop (¬ as_initial … LR_s1) → 125 ∃s0. as_execute … L_label s0 LR_s1 ∧ is_costlabelled_act L_label 126 ∧ ¬ bool_to_Prop (is_act_io_entering S L_label) 127 ; R_nonfin_ok : 128 bool_to_Prop (¬ as_final … (LR_s2)) → 129 ∃so.as_execute … R_label LR_s2 so ∧ is_costlabelled_act R_label 130 ∧ ¬ bool_to_Prop (is_act_io_exiting S R_label) 100 131 }. 101 102 definition measurable' ≝ 103 λt: L_raw_trace. 104 ∃L',so. 105 pre_measurable_trace … (L_t t) ∧ 106 well_formed_trace … (L_t t) ∧ 107 as_execute … (L_s2 t) so L'. 108 (* o, nel caso in cui s2 sia uno stato finale, non serve nessun so e nessuna L' *) 132 133 definition measurable ≝ λS : abstract_status.λt : LR_raw_trace S. 134 pre_measurable_trace … (LR_t … t) ∧ well_formed_trace … (LR_t … t). 135 109 136 110 137 (*CSC: oppure fare il merge di L_raw_trace e measurable in un'unico record se … … 113 140 114 141 definition unmovable_entry_label ≝ 115 call, return post-labelled, init, I/O-uscente. 142 λS : abstract_status.λl. 143 match l with 144 [ call_act _ _ ⇒ false 145 | ret_act _ ⇒ false 146 | cost_act x ⇒ match x with [Some c ⇒ is_io_exiting S c 147 | None ⇒ false 148 ] 149 | init_act ⇒ true 150 ]. 116 151 117 definition unmovable_exit_lable ≝ 118 I/O-entrante, stato finale (???). 152 definition unmovable_exit_label ≝ 153 λS : abstract_status.λl. 154 match l with 155 [ call_act _ _ ⇒ false 156 | ret_act _ ⇒ false 157 | cost_act x ⇒ match x with [Some c ⇒ is_io_entering S c 158 | None ⇒ false 159 ] 160 | init_act ⇒ false 161 ]. 162 163 theorem simulates_LR_raw_trace : 164 ∀S : abstract_status. 165 ∀t : LR_raw_trace S. 166 ∀rel : relations S. 167 measurable S t → 168 ∀s1'.Srel … rel (LR_s1 … t) s1' → 169 ∃ t' : LR_raw_trace S. 170 measurable S t' ∧ 171 if as_initial … (LR_s1 … t) ∨ unmovable_entry_label S (L_label … t) then 172 LR_s1 … t' = s1' 173 else 174 ∃pre : raw_trace … (LR_s1 … t') s1'.trace_prefix … pre (LR_t … t') 175 ∧ ∃s1''.Srel … rel (LR_s2 … t) s1'' ∧ 176 if as_final … (LR_s2 … t) ∨ unmovable_exit_label S (R_label … t) then 177 LR_s2 … t' = s1'' 178 else 179 ∃suff : raw_trace … s1'' (LR_s2 … t'). trace_suffix … suff (LR_t … t') 180 ∧ 181 get_costlabels_of_trace … (LR_t … t) = get_costlabels_of_trace … (LR_t … t'). 182 cases daemon (*TODO*) 183 qed. 184 185 xxxx 119 186 120 187 theorem simulates_L_raw_trace: -
LTS/Traces.ma
r3380 r3387 45 45 coercion ret_act_label_to_cost_label. 46 46 47 definition 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 51 coercion call_act_label_to_cost_label. 52 47 53 inductive ActionLabel : Type[0] ≝ 48 54 | call_act : FunctionName → (CallCostLabel + NonFunctionalLabel) → ActionLabel 49 55 | ret_act : option(ReturnPostCostLabel + NonFunctionalLabel) → ActionLabel 50 | cost_act : list NonFunctionalLabel → ActionLabel. 56 | cost_act : option NonFunctionalLabel → ActionLabel 57 | init_act : ActionLabel. 51 58 52 59 definition is_cost_label : ActionLabel → Prop ≝ … … 64 71 ; as_classify : as_status → status_class 65 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 66 77 }. 67 78 79 definition 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 90 definition 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 68 102 inductive raw_trace (S : abstract_status) : S → S → Type[0] ≝ 69 103 | t_base : ∀st : S.raw_trace S st st … … 81 115 λact.∃l.act = ret_act (Some ? l). 82 116 117 definition is_unlabelled_ret_act : ActionLabel → Prop ≝ 118 λact.act = ret_act (None ?). 119 83 120 definition is_non_silent_cost_act : ActionLabel → Prop ≝ 84 λact. ∃hd,tl. act = cost_act (hd::tl). 121 λact. ∃l. act = cost_act (Some ? l). 122 123 definition 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 ]. 85 129 86 130 inductive well_formed_trace (S : abstract_status) : … … 113 157 [ #st #t2 #t3 %] #st1' #st2' #st3' #l #prf #tl #IH #t2 #t3 whd in ⊢ (??%%); >IH % 114 158 qed. 115 (* 116 inductive balanced_trace (S : abstract_status) : 159 160 definition trace_prefix: ∀S : abstract_status.∀st1,st2,st3 : S.raw_trace … st1 st2 → 161 raw_trace … st1 st3 → Prop≝ 162 λS,st1,st2,st3,t1,t2.∃t3 : raw_trace … st2 st3.t2 = t1 @ t3. 163 164 definition trace_suffix : ∀S : abstract_status.∀st1,st2,st3 : S.raw_trace … st2 st3 → 165 raw_trace … st1 st3 → Prop≝ 166 λS,st1,st2,st3,t1,t2.∃t3 : raw_trace … st1 st2.t2 = t3 @ t1. 167 168 inductive silent_trace (S : abstract_status) : 117 169 ∀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 *) 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 132 175 inductive pre_measurable_trace (S : abstract_status) : 133 176 ∀st1,st2 : S.raw_trace ? st1 st2 → Prop ≝ 134 | pm_empty : ∀st : S. pre_measurable_trace … (t_base ? st)177 | pm_empty : ∀st : S. as_classify … st ≠ cl_io → pre_measurable_trace … (t_base ? st) 135 178 | pm_cons_cost_act : ∀st1,st2,st3 : S.∀l : ActionLabel. 136 179 ∀prf : as_execute S l st1 st2.∀tl : raw_trace S st2 st3. 137 is_cost_act l → pre_measurable_trace … tl →180 as_classify … st1 ≠ cl_io → is_cost_act l → pre_measurable_trace … tl → 138 181 pre_measurable_trace … (t_ind … prf … tl) 139 182 | pm_cons_lab_ret : ∀st1,st2,st3 : S.∀l : ActionLabel. 183 as_classify … st1 ≠ cl_io → 140 184 ∀prf : as_execute S l st1 st2.∀tl : raw_trace S st2 st3. 141 185 is_labelled_ret_act l → pre_measurable_trace … tl → … … 143 187 | pm_cons_post_call : ∀st1,st2,st3 : S.∀l : ActionLabel. 144 188 ∀prf : as_execute S l st1 st2.∀tl : raw_trace S st2 st3. 145 is_call_act l → is_call_post_label … st1 →189 as_classify … st1 ≠ cl_io → is_call_act l → is_call_post_label … st1 → 146 190 pre_measurable_trace … tl → 147 191 pre_measurable_trace … (t_ind … prf … tl) … … 149 193 ∀prf : as_execute S l1 st1 st2.∀t1 : raw_trace S st2 st3. 150 194 ∀t2 : raw_trace S st4 st5.∀prf' : as_execute S l2 st3 st4. 151 is_call_act l1 → ¬ is_call_post_label … st1 → 195 as_classify … st1 ≠ cl_io → as_classify … st3 ≠ cl_io 196 → is_call_act l1 → ¬ is_call_post_label … st1 → 152 197 pre_measurable_trace … t1 → pre_measurable_trace … t2 → 153 198 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 199 is_unlabelled_ret_act l2 → 200 pre_measurable_trace … (t_ind … prf … (t1 @ (t_ind … prf' … t2))).
Note: See TracChangeset
for help on using the changeset viewer.