source: LTS/Simulation.ma @ 3385

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

...

File size: 3.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:
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(*********************************************************************)
80
81replace_last x : weak_trace → weak_trace
82   [] ⇒ [], Some x
83 | l::t ⇒
84     let 〈t',x'〉 ≝ replace_last x t in
85     match x' with
86     [ None ⇒ l::t', None
87     | Some x'' ⇒ [], Some x''
88
89theorem simulates:
90 ∀s1,s2. ∀τ1: raw_trace … s1 s2.
91  pre_measurable_trace … t1 →
92  well_formed_trace … t1.
93 ∀l1: option NonFunctionalLabel.
94 ∀s1'.
95   S s1 s1' →
96   ∃dead_labels.
97   ∃s2'. ∃t2: raw_trace … s1' s2'.
98    pre_mesurable_trace … t2 ∧
99    well_formed_trace … t2.
100   ∃l2: option NonFunctionalLabel.
101    match l1 with
102    [ None ⇒
103       match l2 with
104       [ None ⇒ |t1| = |t2|
105       | Some l2' ⇒ |t1| = l2'::|t2| ]
106    | Some l1' ⇒
107       match l2 with
108       [ None ⇒ |t1| = replace_last l1' |t2| ∧ ends_with l1' t1
109       | Some l2' ⇒
110          if |t2| = [] then |t1| = [l1'] ∧ l2' = l1'
111          else |t1| = l2' :: replace_last l1' |t2| ∧ ends_with l1' t1
112       ]
113    ]
Note: See TracBrowser for help on using the repository browser.