Changeset 3387 for LTS/Simulation.ma
 Timestamp:
 Jul 23, 2013, 4:33:51 PM (7 years ago)
 File:

 1 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 postlabelled, init, I/Ouscente. 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/Oentrante, 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:
Note: See TracChangeset
for help on using the changeset viewer.