source: LTS/Simulation.ma @ 3387

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

unified notation

File size: 7.9 KB
Line 
1include "Common.ma".
2include "Traces.ma".
3
4record relations (S : abstract_status) : Type[0] ≝
5 { Srel: S → S → Prop
6 ; Crel: S → S → Prop
7 }.
8
9definition 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
12record simulation_conditions (S : abstract_status) (rel : relations S) : Type[0] ≝
13 { simulate_tau:
14     ∀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
19 ; simulate_label:
20     ∀s1,s2,l,s1'.
21      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
28 ; simulate_call_pl:
29     ∀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
38 ; simulate_ret_l:
39     ∀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
47 ; simulate_call_n:
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'
58 ; simulate_ret_n:
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''
68 }.
69
70let rec get_costlabels_of_trace (S : abstract_status) (st1 : S) (st2 : S)
71(t : raw_trace S st1 st2) on t : list CostLabel ≝
72match 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
91theorem simulates_pre_mesurable:
92 ∀S : abstract_status.∀rel : relations S.
93 ∀s1,s1' : S. ∀t1: raw_trace S s1 s1'.
94  pre_measurable_trace … t1 →
95  well_formed_trace … t1 → ∀s2.Srel … rel s1 s2 →
96  ∃s2'. ∃t2: raw_trace … s1' s2'.
97    pre_measurable_trace … t2 ∧
98    well_formed_trace … t2 ∧
99    get_costlabels_of_trace … t1 = get_costlabels_of_trace … t2 ∧
100    Srel … rel s2 s2'.
101cases daemon (*TODO*)
102qed.
103
104(* IDEA: aggiungere stati di I/O e cambiare la semantica del linguaggio
105   sorgente; aggiungere nella pre_measurable il vincolo nessuno stato e' di I/O;
106   cambiare la definizione di traccia tornando a una sola etichetta sugli archi *)
107
108(* measurable fattorizzata sotto come measurable'
109definition measurable ≝
110 λL,s1,s2.λt: raw_trace … s1 s2.
111  ∃L',s0,so. as_execute … s0 s1 L ∧
112  pre_measurable_trace … t ∧
113  well_formed_trace … t ∧
114  as_execute … s2 so L'. *)
115
116record 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)
131 }.
132 
133definition measurable ≝ λS : abstract_status.λt : LR_raw_trace S.
134pre_measurable_trace … (LR_t … t) ∧ well_formed_trace … (LR_t … t).
135
136
137(*CSC: oppure fare il merge di L_raw_trace e measurable in un'unico record se
138  non c'e' nulla di interessante sulle L_raw_trace non measurabili. Per esempio
139  il teorema sotto sembra suggerire il merge *)
140
141definition unmovable_entry_label ≝
142λS : abstract_status.λl.
143match 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].
151 
152definition unmovable_exit_label ≝
153λS : abstract_status.λl.
154match 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
163theorem simulates_LR_raw_trace :
164∀S : abstract_status.
165∀t : LR_raw_trace S.
166∀rel : relations S.
167measurable S t →
168∀s1'.Srel … rel (LR_s1 … t) s1' →
169∃ t' : LR_raw_trace S.
170measurable S t' ∧
171if as_initial … (LR_s1 … t) ∨ unmovable_entry_label  S (L_label … t) then
172   LR_s1 … t' = s1'
173else
174   ∃pre : raw_trace … (LR_s1 … t') s1'.trace_prefix … pre (LR_t … t')
175∧ ∃s1''.Srel … rel (LR_s2 … t) s1'' ∧
176if as_final … (LR_s2 … t) ∨ unmovable_exit_label S (R_label … t) then
177   LR_s2 … t' = s1''
178else
179  ∃suff : raw_trace … s1'' (LR_s2 … t'). trace_suffix … suff (LR_t … t')
180
181get_costlabels_of_trace … (LR_t … t) = get_costlabels_of_trace … (LR_t … t').
182cases daemon (*TODO*)
183qed.
184
185xxxx
186
187theorem simulates_L_raw_trace:
188 ∀t: L_raw_trace.
189  pre_measurable_trace … (L_t t1) →
190  well_formed_trace … (L_t t1) →
191 ∀s1'.
192   S (L_s1 t) s1' →
193   s1' -flat-→ (L_s1 t2) →
194   ∃s2',t2: L_raw_trace.
195    pre_mesurable_trace … (L_t t2) ∧
196    well_formed_trace … (L_t t2) ∧
197    |t1| = |t2| ∧
198    S (L_s2 t1) s2' ∧
199    (L_s2 t2) -flat-→ s2'.
200 (* o, nel caso in cui (L_label t1) e' unmovable_entry_label nessuna coda prefissa e
201       nel caso in cui ??? e' unmovable_exit_label, nessuna coda suffissa *)
202
203
204(*********************************************************************)
205
206(* quello che segue tentava di permettere di evitare l'emissione di label
207   associate a codice morto *)
208
209replace_last x : weak_trace → weak_trace
210   [] ⇒ [], Some x
211 | l::t ⇒
212     let 〈t',x'〉 ≝ replace_last x t in
213     match x' with
214     [ None ⇒ l::t', None
215     | Some x'' ⇒ [], Some x''
216
217theorem simulates:
218 ∀s1,s2. ∀τ1: raw_trace … s1 s2.
219  pre_measurable_trace … t1 →
220  well_formed_trace … t1.
221 ∀l1: option NonFunctionalLabel.
222 ∀s1'.
223   S s1 s1' →
224   ∃dead_labels.
225   ∃s2'. ∃t2: raw_trace … s1' s2'.
226    pre_mesurable_trace … t2 ∧
227    well_formed_trace … t2.
228   ∃l2: option NonFunctionalLabel.
229    match l1 with
230    [ None ⇒
231       match l2 with
232       [ None ⇒ |t1| = |t2|
233       | Some l2' ⇒ |t1| = l2'::|t2| ]
234    | Some l1' ⇒
235       match l2 with
236       [ None ⇒ |t1| = replace_last l1' |t2| ∧ ends_with l1' t1
237       | Some l2' ⇒
238          if |t2| = [] then |t1| = [l1'] ∧ l2' = l1'
239          else |t1| = l2' :: replace_last l1' |t2| ∧ ends_with l1' t1
240       ]
241    ]
Note: See TracBrowser for help on using the repository browser.