-
Notifications
You must be signed in to change notification settings - Fork 0
/
SPLPartialRefTemplGen.pvs~
45 lines (34 loc) · 1.41 KB
/
SPLPartialRefTemplGen.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
SPLpartialreftemplates: THEORY
BEGIN
IMPORTING SPLpartialrefinement
pl,pl2,pl3: VAR PL
aSet: VAR finite_sets[Asset].finite_set
am,am1,am2,pairs: VAR AM
a,a1,a2: VAR Asset
an: VAR AssetName
anSet: VAR set[AssetName]
s: VAR set[Conf]
c: VAR Conf
% Restriction Operator
<>: [PL, set[AssetName] -> set[Conf]]
%---------------------------------------------------------------------------------------------------------------------------------------
%---------------------------------------------CHANGE ASSET------------------------------------------------------------------------------
%---------------------------------------------------------------------------------------------------------------------------------------
syntaxChangeAsset(am1,am2,pairs,a1,a2,an):bool =
am1=union((an,a1),pairs) AND
am2=union((an,a2),pairs)
changeAsset: AXIOM
FORALL pl,am2,pairs,a1,a2,an,s : (syntaxChangeAsset(A(pl),am2,pairs,a1,a2,an) AND s = (<>(pl, singleton(an))))
=>
((([| K(pl) |] (A(pl))) (c)) = (([| K(pl) |] (pairs)) (c)) AND (([| K(pl) |] (am2)) (c)) = (([| K(pl) |] (pairs)) (c)))
changeAssetStrong: THEOREM
FORALL(pl,am2,pairs,a1,a2,an,s):
(
(
syntaxChangeAsset(A(pl),am2,pairs,a1,a2,an) AND
s = <>(pl,singleton(an))
)
=>
strongPartialRefinement(pl,pl2,s)
) WHERE pl2=(# F:=F(pl), A:=am2, K:=K(pl) #)
END SPLpartialreftemplates