source: LTS/Simulation.ma @ 3384

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

Bug found?? We think so.

File size: 3.2 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      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 (*???? BUG? ∧ 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
66theorem 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
80replace_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
88theorem 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    ]
Note: See TracBrowser for help on using the repository browser.