-
Notifications
You must be signed in to change notification settings - Fork 0
/
PartialRefDefault.pvs
184 lines (145 loc) · 9.17 KB
/
PartialRefDefault.pvs
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
PartialRefDefault[Conf: TYPE,
FM: TYPE,
{||}: [FM -> set[Conf]],
Asset: TYPE,
AssetName: TYPE,
CK: TYPE,
(IMPORTING maps[AssetName,Asset]) [||]: [CK -> [mapping -> [Conf -> finite_sets[Asset].finite_set]]] ]: THEORY
BEGIN
% Partial SPL Strong Refinement
% --------------------------------------------------------------------------------------------------------
% ------------------------------------------------VARIABLES-----------------------------------------------
% --------------------------------------------------------------------------------------------------------
c,c2: VAR Conf
s,t,u: VAR set[Conf]
fm,fm1,fm2: VAR FM
ck,ck2: VAR CK
a,a1,a2: VAR Asset
an: VAR AssetName
anSet: VAR set[AssetName]
pair: VAR [AssetName,Asset]
IMPORTING PartialRefBasics[Conf,FM,{||},Asset,AssetName,CK,[||]]
am,am1,am2,pairs: VAR AM
pl, pl1, pl2, pl3, pl4: VAR PL
% --------------------------------------------------------------------------------------------------------
% ------------------------------------------------RELATION DEF--------------------------------------------
% --------------------------------------------------------------------------------------------------------
% Partial Refinement Relation - this definition requires that the configuration does not change
strongPartialRefinement(pl1,pl2,s) : bool =
subset?(s,{||}(F(pl1))) AND
subset?(s,{||}(F(pl2))) AND
FORALL c: s(c) =>
(
prod(pl1,c)
|-
prod(pl2,c)
)
% --------------------------------------------------------------------------------------------------------
% ------------------------------------------------PROPERTIES----------------------------------------------
% --------------------------------------------------------------------------------------------------------
%--------------------------------------------------PREORDER-----------------------------------------------
% Theorem <strong partial refinement is reflexive>
strongPartRefReflexive: THEOREM FORALL pl,s: subset?(s,{||}(F(pl))) => strongPartialRefinement(pl,pl,s)
% Theorem <strong partial refinement is transitive>
strongPartRefTransitive: THEOREM (FORALL pl1,pl2,pl3,s,t:
(
strongPartialRefinement(pl1,pl2,s)
AND
strongPartialRefinement(pl2,pl3,t)
)
=> strongPartialRefinement(pl1,pl3,intersection(s,t))
)
partialRefSubset: THEOREM FORALL pl1,s,pl2 : strongPartialRefinement(pl1,pl2,s) => (FORALL t: subset?(t,s) => strongPartialRefinement(pl1,pl2,t))
%-------------------------------------------------------COMPOSITIONALITY---------------------------------------------------
% Theorem <FM Equivalence compositionality - weak definition>
%fmCompStrongDef: THEOREM
%FORALL(pl,fm1,fm2,s,t):
%(
% subset?(s,t) AND fmPartialRefinement(fm1,fm2,t) AND wfPL(pl2)
% =>
% strongPartialRefinement(pl,pl2,s)
%)
%WHERE fm1=F(pl),pl2=(# F := fm2, A := A(pl), K := K(pl) #)
fmCompStrongDef: THEOREM
FORALL(pl,fm2,s):
(
fmPartialRefinement(F(pl),fm2,s) AND wfPL(pl2)
=>
strongPartialRefinement(pl,pl2,s)
)
WHERE fm1=F(pl),pl2=(# F := fm2, A := A(pl), K := K(pl) #)
fmRefStrongDef: THEOREM
FORALL(pl,fm2,s):
(
subset?(s,{||}(F(pl))) AND (F(pl) |= fm2) AND wfPL(pl2)
=>
strongPartialRefinement(pl,pl2,s)
)
WHERE fm1=F(pl),pl2=(# F := fm2, A := A(pl), K := K(pl) #)
ckWeakerEqStrongDef: THEOREM
FORALL (pl,ck2,s):
(
subset?(s,{||}(F(pl))) AND ckWeakerEq(ck1,ck2,s) AND wfPL(pl2)
=>
strongPartialRefinement(pl,pl2,s)
)
WHERE ck1=K(pl),pl2=(# F:= F(pl), A := A(pl), K := ck2 #)
%--------------------------------------------------COMMUTABLE DIAGRAM------------------------------------------------------
partCaseStrongerPLRef: THEOREM FORALL pl1,pl2,s: s = {||}(F(pl1)) => (strongPartialRefinement(pl1,pl2,s) <=> strongerPLrefinement(pl1,pl2))
%--------------------------------------------------COMMUTABLE DIAGRAM------------------------------------------------------
% auxiliar definitions
partRefRel(pl1,pl2:PL,s:{confs:set[Conf]| subset?(confs,{||}(F(pl1)))}): bool =
FORALL c : s(c) =>
(EXISTS c2 : {||}(F(pl2))(c2) AND (prod(pl1,c) |- prod(pl2,c2)))
partRefFun(pl1,pl2:PL,s:set[Conf],f:[(s) -> ({||}(F(pl2)))]): bool =
FORALL (c:domain(f)) : {||}(F(pl2))(f(c)) AND (prod(pl1,c) |- prod(pl2,f(c)))
% considering strongerPlRefinement definition
totalImpliesPartial: LEMMA FORALL pl1,pl2,(s:set[Conf] | subset?(s,{||}(F(pl1)))):
strongerPLrefinement(pl1,pl2) => strongPartialRefinement(pl1,pl2,s)
partialImpliesTotal: LEMMA FORALL pl1,pl2,s: (s = {||}(F(pl1)) AND strongPartialRefinement(pl1,pl2,s))
=> strongerPLrefinement(pl1,pl2)
commutableDiagram: THEOREM FORALL pl1,pl3,
pl4,(s:set[Conf] | subset?(s,{||}(F(pl1)))):
(strongerPLrefinement(pl1,pl3) AND strongPartialRefinement(pl3,pl4,s)) =>
(EXISTS pl2:
strongPartialRefinement(pl1,pl2,s) AND strongerPLrefinement(pl2,pl4))
commutableDiagram2: THEOREM FORALL pl1,pl2,
pl4,s:
(strongPartialRefinement(pl1,pl2,s) AND strongerPLrefinement(pl2,pl4)) =>
(EXISTS pl3:
strongerPLrefinement(pl1,pl3) AND strongPartialRefinement(pl3,pl4,s))
commutableDiagramAlt: THEOREM FORALL pl1,pl4,(s:set[Conf] | subset?(s,{||}(F(pl1)))):
(EXISTS pl2: strongPartialRefinement(pl1,pl2,s) AND strongerPLrefinement(pl2,pl4)) <=>
(EXISTS pl3: strongerPLrefinement(pl1,pl3) AND strongPartialRefinement(pl3,pl4,s))
%--------------------------------------------------TRANSITIVITY MIXING DEFS-------------------------------------------------
%------ STRONG TOTAL AND STRONG PARTIAL
partPlusTotalStrongerImpliesPart: THEOREM FORALL pl1,pl2,pl3,s:
strongPartialRefinement(pl1,pl2,s) AND strongerPLrefinement(pl2,pl3)
=> strongPartialRefinement(pl1,pl3,s)
totalStrongerPlusPartImpliesPart: THEOREM FORALL pl1,pl2,pl3,(s:set[Conf] | subset?(s,{||}(F(pl1)))):
strongerPLrefinement(pl1,pl2) AND strongPartialRefinement(pl2,pl3,s)
=> strongPartialRefinement(pl1,pl3,s)
%------ TOTAL AND STRONG PARTIAL
partPlusTotalImpliesPartRel: THEOREM FORALL pl1,pl2,pl3,s:
strongPartialRefinement(pl1,pl2,s) AND plRefinement(pl2,pl3) =>
partRefRel(pl1,pl3,s)
totalPlusPartImpliesPartRef: THEOREM FORALL pl1,pl2,pl3,s:
plRefinement(pl1,pl2) AND strongPartialRefinement(pl2,pl3,s) =>
(EXISTS (t:set[Conf] | subset?(t,{||}(F(pl1)))) : partRefRel(pl1,pl3,t))
partRefExistsFunId: LEMMA FORALL pl1,pl2,s: strongPartialRefinement(pl1,pl2,s) =>
(EXISTS (f:[(s) -> (s)]) : (FORALL c : s(c) => ({||}(F(pl2))(f(c))) and (prod(pl1,c) |- prod(pl2,f(c)))))
partPlusTotalImpliesPartFun: THEOREM FORALL pl1,pl2,pl3,s:
strongPartialRefinement(pl1,pl2,s) AND plRefinement(pl2,pl3) =>
(EXISTS (f:[(s) -> ({||}(F(pl3)))]) :
(FORALL c : s(c) => ({||}(F(pl3))(f(c)) AND (prod(pl1,c) |- prod(pl3,f(c))))))
%------ TOTAL FUN AND STRONG PARTIAL
%partPlusTotalFunImpliesPartFun: THEOREM FORALL pl1,pl2,pl3,s,(f: [(s) -> ({||}(F(pl3)))]):
% strongPartialRefinement(pl1,pl2,s) AND plRefinementFun(pl2,pl3,f) =>
% partRefFun(pl1,pl3,f,s)
%totalFunPlusPartImpliesPartFun: THEOREM FORALL pl1,pl2,pl3,s,(f:[Conf -> Conf]):
% plRefinementFun(pl1,pl2,f) AND strongPartialRefinement(pl2,pl3,s) =>
% EXISTS (t:set[Conf]) :
% partRefFun(pl1,pl3,
% {c:Conf | {||}(F(pl1))(c) AND s(f(c)) AND (prod(pl1,c) |- prod(pl2,f(c)))},
% f)
END PartialRefDefault