source: LTS/Simulation.ma @ 3386

Last change on this file since 3386 was 3386, checked in by sacerdot, 6 years ago

Something that seems to be working after all.
File size: 5.3 KB
Line 
1include "Common.ma".
2
3record relations: Type[0] ≝
4 { Srel: status → status → Prop
5 ; Crel: status → status → Prop
6 }.
7
8definition Rrel ≝ λs,s'.
9 ∀s1,s1'. succ s1 s → Crel s1 s1' → succ s1' s'.
10
11record simulation_conditions: Type[0] ≝
12 { 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' ∧ silent t
18 ; simulate_label:
19     ∀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 ∧ silent t3
27 ; simulate_call_pl:
28     ∀s1,s2,l,s1'.
29      post_labelled s1 →
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 ∧ silent t3
37 ; 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 ∧ silent t3
46 ; 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'
56 ; 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''
65 }.
66
67theorem simulates_pre_mesurable:
68 ∀s1,s2. ∀τ1: raw_trace … s1 s2.
69  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 ∧
75    well_formed_trace … t2 ∧
76    |t1| = |t2| ∧
77    S s2 s2'.
78
79(* IDEA: aggiungere stati di I/O e cambiare la semantica del linguaggio
80   sorgente; aggiungere nella pre_measurable il vincolo nessuno stato e' di I/O;
81   cambiare la definizione di traccia tornando a una sola etichetta sugli archi *)
82
83(* measurable fattorizzata sotto come measurable'
84definition measurable ≝
85 λL,s1,s2.λt: raw_trace … s1 s2.
86  ∃L',s0,so. as_execute … s0 s1 L ∧
87  pre_measurable_trace … t ∧
88  well_formed_trace … t ∧
89  as_execute … s2 so L'. *)
90
91(*CSC: definire usando un record?*)
92record 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 *)
100 }.
101
102definition 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' *)
109
110(*CSC: oppure fare il merge di L_raw_trace e measurable in un'unico record se
111  non c'e' nulla di interessante sulle L_raw_trace non measurabili. Per esempio
112  il teorema sotto sembra suggerire il merge *)
113
114definition unmovable_entry_label ≝
115  call, return post-labelled, init, I/O-uscente.
116 
117definition unmovable_exit_lable ≝
118  I/O-entrante, stato finale (???).
119
120theorem simulates_L_raw_trace:
121 ∀t: L_raw_trace.
122  pre_measurable_trace … (L_t t1) →
123  well_formed_trace … (L_t t1) →
124 ∀s1'.
125   S (L_s1 t) s1' →
126   s1' -flat-→ (L_s1 t2) →
127   ∃s2',t2: L_raw_trace.
128    pre_mesurable_trace … (L_t t2) ∧
129    well_formed_trace … (L_t t2) ∧
130    |t1| = |t2| ∧
131    S (L_s2 t1) s2' ∧
132    (L_s2 t2) -flat-→ s2'.
133 (* o, nel caso in cui (L_label t1) e' unmovable_entry_label nessuna coda prefissa e
134       nel caso in cui ??? e' unmovable_exit_label, nessuna coda suffissa *)
135
136
137(*********************************************************************)
138
139(* quello che segue tentava di permettere di evitare l'emissione di label
140   associate a codice morto *)
141
142replace_last x : weak_trace → weak_trace
143   [] ⇒ [], Some x
144 | l::t ⇒
145     let 〈t',x'〉 ≝ replace_last x t in
146     match x' with
147     [ None ⇒ l::t', None
148     | Some x'' ⇒ [], Some x''
149
150theorem simulates:
151 ∀s1,s2. ∀τ1: raw_trace … s1 s2.
152  pre_measurable_trace … t1 →
153  well_formed_trace … t1.
154 ∀l1: option NonFunctionalLabel.
155 ∀s1'.
156   S s1 s1' →
157   ∃dead_labels.
158   ∃s2'. ∃t2: raw_trace … s1' s2'.
159    pre_mesurable_trace … t2 ∧
160    well_formed_trace … t2.
161   ∃l2: option NonFunctionalLabel.
162    match l1 with
163    [ None ⇒
164       match l2 with
165       [ None ⇒ |t1| = |t2|
166       | Some l2' ⇒ |t1| = l2'::|t2| ]
167    | Some l1' ⇒
168       match l2 with
169       [ None ⇒ |t1| = replace_last l1' |t2| ∧ ends_with l1' t1
170       | Some l2' ⇒
171          if |t2| = [] then |t1| = [l1'] ∧ l2' = l1'
172          else |t1| = l2' :: replace_last l1' |t2| ∧ ends_with l1' t1
173       ]
174    ]
Note: See TracBrowser for help on using the repository browser.