source: LTS/Simulation.ma @ 3383

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

Simple simulation conditions and statements added.

The complex ones would allow the code to tunnel away labels by
returning an initial label that has not been emitted and that must be
emitted by the predecessor code.
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 ∧ 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.