1 | include "Common.ma". |
---|
2 | |
---|
3 | record relations: Type[0] ≝ |
---|
4 | { Srel: status → status → Prop |
---|
5 | ; Crel: status → status → Prop |
---|
6 | }. |
---|
7 | |
---|
8 | definition Rrel ≝ λs,s'. |
---|
9 | ∀s1,s1'. succ s1 s → Crel s1 s1' → succ s1' s'. |
---|
10 | |
---|
11 | record 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 | Srel s1 s1' → |
---|
50 | ∃s2',s2'',s2'''. |
---|
51 | ∃t1: raw_trace s1' s2'. |
---|
52 | as_execute s2' s2'' (ret_act None) ∧ |
---|
53 | ∃t3: raw_trace s2'' s2'''. |
---|
54 | Srel s2 s2''' ∧ silent t1 ∧ silent t3 ∧ Rrel s2 s2'' ∧ Crel s1 s2' |
---|
55 | ; simulate_ret_n: |
---|
56 | ∀s1,s2,l,s1'. |
---|
57 | as_execute s1 s2 (ret_act None) → |
---|
58 | Srel s1 s1' → |
---|
59 | ∃s2',s2'',s2'''. |
---|
60 | ∃t1: raw_trace s1' s2'. |
---|
61 | as_execute s2' s2'' (ret_act None) ∧ |
---|
62 | ∃t3: raw_trace s2'' s2'''. |
---|
63 | Srel s2 s2''' ∧ silent t1 ∧ silent t3 ∧ Rrel s2 s2'' |
---|
64 | }. |
---|
65 | |
---|
66 | theorem simulates: |
---|
67 | ∀s1,s2. ∀τ1: raw_trace … s1 s2. |
---|
68 | pre_measurable_trace … t1 → |
---|
69 | well_formed_trace … t1. |
---|
70 | ∀s1'. |
---|
71 | S s1 s1' → |
---|
72 | ∃s2'. ∃t2: raw_trace … s1' s2'. |
---|
73 | pre_mesurable_trace … t2 ∧ |
---|
74 | well_formed_trace … t2 ∧ |
---|
75 | |t1| = |t2| ∧ |
---|
76 | S s2 s2. |
---|
77 | |
---|
78 | (*********************************************************************) |
---|
79 | |
---|
80 | replace_last x : weak_trace → weak_trace |
---|
81 | [] ⇒ [], Some x |
---|
82 | | l::t ⇒ |
---|
83 | let 〈t',x'〉 ≝ replace_last x t in |
---|
84 | match x' with |
---|
85 | [ None ⇒ l::t', None |
---|
86 | | Some x'' ⇒ [], Some x'' |
---|
87 | |
---|
88 | theorem simulates: |
---|
89 | ∀s1,s2. ∀τ1: raw_trace … s1 s2. |
---|
90 | pre_measurable_trace … t1 → |
---|
91 | well_formed_trace … t1. |
---|
92 | ∀l1: option NonFunctionalLabel. |
---|
93 | ∀s1'. |
---|
94 | S s1 s1' → |
---|
95 | ∃dead_labels. |
---|
96 | ∃s2'. ∃t2: raw_trace … s1' s2'. |
---|
97 | pre_mesurable_trace … t2 ∧ |
---|
98 | well_formed_trace … t2. |
---|
99 | ∃l2: option NonFunctionalLabel. |
---|
100 | match l1 with |
---|
101 | [ None ⇒ |
---|
102 | match l2 with |
---|
103 | [ None ⇒ |t1| = |t2| |
---|
104 | | Some l2' ⇒ |t1| = l2'::|t2| ] |
---|
105 | | Some l1' ⇒ |
---|
106 | match l2 with |
---|
107 | [ None ⇒ |t1| = replace_last l1' |t2| ∧ ends_with l1' t1 |
---|
108 | | Some l2' ⇒ |
---|
109 | if |t2| = [] then |t1| = [l1'] ∧ l2' = l1' |
---|
110 | else |t1| = l2' :: replace_last l1' |t2| ∧ ends_with l1' t1 |
---|
111 | ] |
---|
112 | ] |
---|