author | wenzelm |
Thu, 11 Jan 2001 21:51:14 +0100 | |
changeset 10873 | 50608ca5785c |
parent 10064 | 1a77667b21ef |
permissions | -rw-r--r-- |
6815 | 1 |
(* Title: HOL/UNITY/Alloc |
2 |
ID: $Id$ |
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 |
Copyright 1998 University of Cambridge |
|
5 |
||
6 |
Specification of Chandy and Charpentier's Allocator |
|
7 |
*) |
|
8 |
||
8930 | 9 |
Alloc = AllocBase + PPROD + |
6815 | 10 |
|
8055
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset
|
11 |
(** State definitions. OUTPUT variables are locals **) |
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset
|
12 |
|
6815 | 13 |
record clientState = |
14 |
giv :: nat list (*client's INPUT history: tokens GRANTED*) |
|
15 |
ask :: nat list (*client's OUTPUT history: tokens REQUESTED*) |
|
16 |
rel :: nat list (*client's OUTPUT history: tokens RELEASED*) |
|
17 |
||
9403
aad13b59b8d9
much tidying in connection with the 2nd UNITY paper
paulson
parents:
9109
diff
changeset
|
18 |
record 'a clientState_d = |
8286
d4b895d3afa7
not working yet. partial conversion to use "rename" instead of "extend"
paulson
parents:
8122
diff
changeset
|
19 |
clientState + |
9403
aad13b59b8d9
much tidying in connection with the 2nd UNITY paper
paulson
parents:
9109
diff
changeset
|
20 |
dummy :: 'a (*dummy field for new variables*) |
8286
d4b895d3afa7
not working yet. partial conversion to use "rename" instead of "extend"
paulson
parents:
8122
diff
changeset
|
21 |
|
8311
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
22 |
constdefs |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
23 |
(*DUPLICATED FROM Client.thy, but with "tok" removed*) |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
24 |
(*Maybe want a special theory section to declare such maps*) |
9403
aad13b59b8d9
much tidying in connection with the 2nd UNITY paper
paulson
parents:
9109
diff
changeset
|
25 |
non_dummy :: 'a clientState_d => clientState |
aad13b59b8d9
much tidying in connection with the 2nd UNITY paper
paulson
parents:
9109
diff
changeset
|
26 |
"non_dummy s == (|giv = giv s, ask = ask s, rel = rel s|)" |
8286
d4b895d3afa7
not working yet. partial conversion to use "rename" instead of "extend"
paulson
parents:
8122
diff
changeset
|
27 |
|
8311
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
28 |
(*Renaming map to put a Client into the standard form*) |
9403
aad13b59b8d9
much tidying in connection with the 2nd UNITY paper
paulson
parents:
9109
diff
changeset
|
29 |
client_map :: "'a clientState_d => clientState*'a" |
aad13b59b8d9
much tidying in connection with the 2nd UNITY paper
paulson
parents:
9109
diff
changeset
|
30 |
"client_map == funPair non_dummy dummy" |
8311
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
31 |
|
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
32 |
|
6815 | 33 |
record allocState = |
8055
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset
|
34 |
allocGiv :: nat => nat list (*OUTPUT history: source of "giv" for i*) |
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset
|
35 |
allocAsk :: nat => nat list (*INPUT: allocator's copy of "ask" for i*) |
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset
|
36 |
allocRel :: nat => nat list (*INPUT: allocator's copy of "rel" for i*) |
6815 | 37 |
|
9403
aad13b59b8d9
much tidying in connection with the 2nd UNITY paper
paulson
parents:
9109
diff
changeset
|
38 |
record 'a allocState_d = |
8286
d4b895d3afa7
not working yet. partial conversion to use "rename" instead of "extend"
paulson
parents:
8122
diff
changeset
|
39 |
allocState + |
9403
aad13b59b8d9
much tidying in connection with the 2nd UNITY paper
paulson
parents:
9109
diff
changeset
|
40 |
dummy :: 'a (*dummy field for new variables*) |
8286
d4b895d3afa7
not working yet. partial conversion to use "rename" instead of "extend"
paulson
parents:
8122
diff
changeset
|
41 |
|
d4b895d3afa7
not working yet. partial conversion to use "rename" instead of "extend"
paulson
parents:
8122
diff
changeset
|
42 |
record 'a systemState = |
d4b895d3afa7
not working yet. partial conversion to use "rename" instead of "extend"
paulson
parents:
8122
diff
changeset
|
43 |
allocState + |
6815 | 44 |
client :: nat => clientState (*states of all clients*) |
9403
aad13b59b8d9
much tidying in connection with the 2nd UNITY paper
paulson
parents:
9109
diff
changeset
|
45 |
dummy :: 'a (*dummy field for new variables*) |
6815 | 46 |
|
47 |
||
48 |
constdefs |
|
49 |
||
50 |
(** Resource allocation system specification **) |
|
51 |
||
52 |
(*spec (1)*) |
|
8286
d4b895d3afa7
not working yet. partial conversion to use "rename" instead of "extend"
paulson
parents:
8122
diff
changeset
|
53 |
system_safety :: 'a systemState program set |
6815 | 54 |
"system_safety == |
9109 | 55 |
Always {s. setsum(%i.(tokens o giv o sub i o client)s) (lessThan Nclients) |
56 |
<= NbT + setsum(%i.(tokens o rel o sub i o client)s) (lessThan Nclients)}" |
|
6815 | 57 |
|
58 |
(*spec (2)*) |
|
8286
d4b895d3afa7
not working yet. partial conversion to use "rename" instead of "extend"
paulson
parents:
8122
diff
changeset
|
59 |
system_progress :: 'a systemState program set |
8985 | 60 |
"system_progress == INT i : lessThan Nclients. |
6815 | 61 |
INT h. |
62 |
{s. h <= (ask o sub i o client)s} LeadsTo |
|
6827 | 63 |
{s. h pfixLe (giv o sub i o client) s}" |
64 |
||
8286
d4b895d3afa7
not working yet. partial conversion to use "rename" instead of "extend"
paulson
parents:
8122
diff
changeset
|
65 |
system_spec :: 'a systemState program set |
6827 | 66 |
"system_spec == system_safety Int system_progress" |
6815 | 67 |
|
68 |
(** Client specification (required) ***) |
|
69 |
||
8055
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset
|
70 |
(*spec (3)*) |
9403
aad13b59b8d9
much tidying in connection with the 2nd UNITY paper
paulson
parents:
9109
diff
changeset
|
71 |
client_increasing :: 'a clientState_d program set |
6815 | 72 |
"client_increasing == |
10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
73 |
UNIV guarantees Increasing ask Int Increasing rel" |
6815 | 74 |
|
75 |
(*spec (4)*) |
|
9403
aad13b59b8d9
much tidying in connection with the 2nd UNITY paper
paulson
parents:
9109
diff
changeset
|
76 |
client_bounded :: 'a clientState_d program set |
6815 | 77 |
"client_bounded == |
10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
78 |
UNIV guarantees Always {s. ALL elt : set (ask s). elt <= NbT}" |
6815 | 79 |
|
80 |
(*spec (5)*) |
|
9403
aad13b59b8d9
much tidying in connection with the 2nd UNITY paper
paulson
parents:
9109
diff
changeset
|
81 |
client_progress :: 'a clientState_d program set |
6815 | 82 |
"client_progress == |
10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
83 |
Increasing giv guarantees |
6827 | 84 |
(INT h. {s. h <= giv s & h pfixGe ask s} |
8286
d4b895d3afa7
not working yet. partial conversion to use "rename" instead of "extend"
paulson
parents:
8122
diff
changeset
|
85 |
LeadsTo {s. tokens h <= (tokens o rel) s})" |
6815 | 86 |
|
8065
658e0d4e4ed9
first working version to Alloc/System_Client_Progress;
paulson
parents:
8055
diff
changeset
|
87 |
(*spec: preserves part*) |
10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
88 |
client_preserves :: 'a clientState_d program set |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
89 |
"client_preserves == preserves giv Int preserves clientState_d.dummy" |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
90 |
|
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
91 |
(*environmental constraints*) |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
92 |
client_allowed_acts :: 'a clientState_d program set |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
93 |
"client_allowed_acts == |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
94 |
{F. AllowedActs F = |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
95 |
insert Id (UNION (preserves (funPair rel ask)) Acts)}" |
8065
658e0d4e4ed9
first working version to Alloc/System_Client_Progress;
paulson
parents:
8055
diff
changeset
|
96 |
|
9403
aad13b59b8d9
much tidying in connection with the 2nd UNITY paper
paulson
parents:
9109
diff
changeset
|
97 |
client_spec :: 'a clientState_d program set |
8065
658e0d4e4ed9
first working version to Alloc/System_Client_Progress;
paulson
parents:
8055
diff
changeset
|
98 |
"client_spec == client_increasing Int client_bounded Int client_progress |
10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
99 |
Int client_allowed_acts Int client_preserves" |
6827 | 100 |
|
6815 | 101 |
(** Allocator specification (required) ***) |
102 |
||
8055
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset
|
103 |
(*spec (6)*) |
9403
aad13b59b8d9
much tidying in connection with the 2nd UNITY paper
paulson
parents:
9109
diff
changeset
|
104 |
alloc_increasing :: 'a allocState_d program set |
6815 | 105 |
"alloc_increasing == |
10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
106 |
UNIV guarantees |
8985 | 107 |
(INT i : lessThan Nclients. Increasing (sub i o allocGiv))" |
6815 | 108 |
|
109 |
(*spec (7)*) |
|
9403
aad13b59b8d9
much tidying in connection with the 2nd UNITY paper
paulson
parents:
9109
diff
changeset
|
110 |
alloc_safety :: 'a allocState_d program set |
6815 | 111 |
"alloc_safety == |
8985 | 112 |
(INT i : lessThan Nclients. Increasing (sub i o allocRel)) |
10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
113 |
guarantees |
9109 | 114 |
Always {s. setsum(%i.(tokens o sub i o allocGiv)s) (lessThan Nclients) |
115 |
<= NbT + setsum(%i.(tokens o sub i o allocRel)s) (lessThan Nclients)}" |
|
6815 | 116 |
|
117 |
(*spec (8)*) |
|
9403
aad13b59b8d9
much tidying in connection with the 2nd UNITY paper
paulson
parents:
9109
diff
changeset
|
118 |
alloc_progress :: 'a allocState_d program set |
6815 | 119 |
"alloc_progress == |
8985 | 120 |
(INT i : lessThan Nclients. Increasing (sub i o allocAsk) Int |
6815 | 121 |
Increasing (sub i o allocRel)) |
122 |
Int |
|
9403
aad13b59b8d9
much tidying in connection with the 2nd UNITY paper
paulson
parents:
9109
diff
changeset
|
123 |
Always {s. ALL i<Nclients. |
aad13b59b8d9
much tidying in connection with the 2nd UNITY paper
paulson
parents:
9109
diff
changeset
|
124 |
ALL elt : set ((sub i o allocAsk) s). elt <= NbT} |
6815 | 125 |
Int |
8985 | 126 |
(INT i : lessThan Nclients. |
6827 | 127 |
INT h. {s. h <= (sub i o allocGiv)s & h pfixGe (sub i o allocAsk)s} |
8075 | 128 |
LeadsTo |
129 |
{s. tokens h <= (tokens o sub i o allocRel)s}) |
|
10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
130 |
guarantees |
8985 | 131 |
(INT i : lessThan Nclients. |
8069
19b9f92ca503
working with weak LeadsTo in guarantees precondition\!
paulson
parents:
8065
diff
changeset
|
132 |
INT h. {s. h <= (sub i o allocAsk) s} |
8122
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8075
diff
changeset
|
133 |
LeadsTo |
6827 | 134 |
{s. h pfixLe (sub i o allocGiv) s})" |
135 |
||
9109 | 136 |
(*NOTE: to follow the original paper, the formula above should have had |
137 |
INT h. {s. h i <= (sub i o allocGiv)s & h i pfixGe (sub i o allocAsk)s} |
|
138 |
LeadsTo |
|
139 |
{s. tokens h i <= (tokens o sub i o allocRel)s}) |
|
140 |
thus h should have been a function variable. However, only h i is ever |
|
141 |
looked at.*) |
|
142 |
||
8065
658e0d4e4ed9
first working version to Alloc/System_Client_Progress;
paulson
parents:
8055
diff
changeset
|
143 |
(*spec: preserves part*) |
10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
144 |
alloc_preserves :: 'a allocState_d program set |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
145 |
"alloc_preserves == preserves allocRel Int preserves allocAsk Int |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
146 |
preserves allocState_d.dummy" |
8065
658e0d4e4ed9
first working version to Alloc/System_Client_Progress;
paulson
parents:
8055
diff
changeset
|
147 |
|
10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
148 |
(*environmental constraints*) |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
149 |
alloc_allowed_acts :: 'a allocState_d program set |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
150 |
"alloc_allowed_acts == |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
151 |
{F. AllowedActs F = |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
152 |
insert Id (UNION (preserves allocGiv) Acts)}" |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
153 |
|
9403
aad13b59b8d9
much tidying in connection with the 2nd UNITY paper
paulson
parents:
9109
diff
changeset
|
154 |
alloc_spec :: 'a allocState_d program set |
8065
658e0d4e4ed9
first working version to Alloc/System_Client_Progress;
paulson
parents:
8055
diff
changeset
|
155 |
"alloc_spec == alloc_increasing Int alloc_safety Int alloc_progress Int |
10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
156 |
alloc_allowed_acts Int alloc_preserves" |
6815 | 157 |
|
158 |
(** Network specification ***) |
|
159 |
||
160 |
(*spec (9.1)*) |
|
8286
d4b895d3afa7
not working yet. partial conversion to use "rename" instead of "extend"
paulson
parents:
8122
diff
changeset
|
161 |
network_ask :: 'a systemState program set |
8985 | 162 |
"network_ask == INT i : lessThan Nclients. |
10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
163 |
Increasing (ask o sub i o client) guarantees |
8075 | 164 |
((sub i o allocAsk) Fols (ask o sub i o client))" |
6815 | 165 |
|
166 |
(*spec (9.2)*) |
|
8286
d4b895d3afa7
not working yet. partial conversion to use "rename" instead of "extend"
paulson
parents:
8122
diff
changeset
|
167 |
network_giv :: 'a systemState program set |
8985 | 168 |
"network_giv == INT i : lessThan Nclients. |
8075 | 169 |
Increasing (sub i o allocGiv) |
10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
170 |
guarantees |
8075 | 171 |
((giv o sub i o client) Fols (sub i o allocGiv))" |
6815 | 172 |
|
173 |
(*spec (9.3)*) |
|
8286
d4b895d3afa7
not working yet. partial conversion to use "rename" instead of "extend"
paulson
parents:
8122
diff
changeset
|
174 |
network_rel :: 'a systemState program set |
8985 | 175 |
"network_rel == INT i : lessThan Nclients. |
8075 | 176 |
Increasing (rel o sub i o client) |
10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
177 |
guarantees |
8075 | 178 |
((sub i o allocRel) Fols (rel o sub i o client))" |
6815 | 179 |
|
8065
658e0d4e4ed9
first working version to Alloc/System_Client_Progress;
paulson
parents:
8055
diff
changeset
|
180 |
(*spec: preserves part*) |
10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
181 |
network_preserves :: 'a systemState program set |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
182 |
"network_preserves == |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
183 |
preserves allocGiv Int |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
184 |
(INT i : lessThan Nclients. preserves (rel o sub i o client) Int |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
185 |
preserves (ask o sub i o client))" |
8065
658e0d4e4ed9
first working version to Alloc/System_Client_Progress;
paulson
parents:
8055
diff
changeset
|
186 |
|
10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
187 |
(*environmental constraints*) |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
188 |
network_allowed_acts :: 'a systemState program set |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
189 |
"network_allowed_acts == |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
190 |
{F. AllowedActs F = |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
191 |
insert Id |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
192 |
(UNION (preserves allocRel Int |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
193 |
(INT i: lessThan Nclients. preserves(giv o sub i o client))) |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
194 |
Acts)}" |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
195 |
|
8286
d4b895d3afa7
not working yet. partial conversion to use "rename" instead of "extend"
paulson
parents:
8122
diff
changeset
|
196 |
network_spec :: 'a systemState program set |
8065
658e0d4e4ed9
first working version to Alloc/System_Client_Progress;
paulson
parents:
8055
diff
changeset
|
197 |
"network_spec == network_ask Int network_giv Int |
10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
198 |
network_rel Int network_allowed_acts Int |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
199 |
network_preserves" |
6827 | 200 |
|
201 |
||
202 |
(** State mappings **) |
|
9403
aad13b59b8d9
much tidying in connection with the 2nd UNITY paper
paulson
parents:
9109
diff
changeset
|
203 |
sysOfAlloc :: "((nat => clientState) * 'a) allocState_d => 'a systemState" |
aad13b59b8d9
much tidying in connection with the 2nd UNITY paper
paulson
parents:
9109
diff
changeset
|
204 |
"sysOfAlloc == %s. let (cl,xtr) = allocState_d.dummy s |
8286
d4b895d3afa7
not working yet. partial conversion to use "rename" instead of "extend"
paulson
parents:
8122
diff
changeset
|
205 |
in (| allocGiv = allocGiv s, |
d4b895d3afa7
not working yet. partial conversion to use "rename" instead of "extend"
paulson
parents:
8122
diff
changeset
|
206 |
allocAsk = allocAsk s, |
d4b895d3afa7
not working yet. partial conversion to use "rename" instead of "extend"
paulson
parents:
8122
diff
changeset
|
207 |
allocRel = allocRel s, |
d4b895d3afa7
not working yet. partial conversion to use "rename" instead of "extend"
paulson
parents:
8122
diff
changeset
|
208 |
client = cl, |
9403
aad13b59b8d9
much tidying in connection with the 2nd UNITY paper
paulson
parents:
9109
diff
changeset
|
209 |
dummy = xtr|)" |
6827 | 210 |
|
8286
d4b895d3afa7
not working yet. partial conversion to use "rename" instead of "extend"
paulson
parents:
8122
diff
changeset
|
211 |
|
9403
aad13b59b8d9
much tidying in connection with the 2nd UNITY paper
paulson
parents:
9109
diff
changeset
|
212 |
sysOfClient :: "(nat => clientState) * 'a allocState_d => 'a systemState" |
8286
d4b895d3afa7
not working yet. partial conversion to use "rename" instead of "extend"
paulson
parents:
8122
diff
changeset
|
213 |
"sysOfClient == %(cl,al). (| allocGiv = allocGiv al, |
d4b895d3afa7
not working yet. partial conversion to use "rename" instead of "extend"
paulson
parents:
8122
diff
changeset
|
214 |
allocAsk = allocAsk al, |
d4b895d3afa7
not working yet. partial conversion to use "rename" instead of "extend"
paulson
parents:
8122
diff
changeset
|
215 |
allocRel = allocRel al, |
d4b895d3afa7
not working yet. partial conversion to use "rename" instead of "extend"
paulson
parents:
8122
diff
changeset
|
216 |
client = cl, |
9403
aad13b59b8d9
much tidying in connection with the 2nd UNITY paper
paulson
parents:
9109
diff
changeset
|
217 |
systemState.dummy = allocState_d.dummy al|)" |
6827 | 218 |
|
8311
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
219 |
consts |
9403
aad13b59b8d9
much tidying in connection with the 2nd UNITY paper
paulson
parents:
9109
diff
changeset
|
220 |
Alloc :: 'a allocState_d program |
aad13b59b8d9
much tidying in connection with the 2nd UNITY paper
paulson
parents:
9109
diff
changeset
|
221 |
Client :: 'a clientState_d program |
8286
d4b895d3afa7
not working yet. partial conversion to use "rename" instead of "extend"
paulson
parents:
8122
diff
changeset
|
222 |
Network :: 'a systemState program |
d4b895d3afa7
not working yet. partial conversion to use "rename" instead of "extend"
paulson
parents:
8122
diff
changeset
|
223 |
System :: 'a systemState program |
6827 | 224 |
|
8311
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
225 |
rules |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
226 |
Alloc "Alloc : alloc_spec" |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
227 |
Client "Client : client_spec" |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
228 |
Network "Network : network_spec" |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
229 |
|
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
230 |
defs |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
231 |
System_def |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
232 |
"System == rename sysOfAlloc Alloc Join Network Join |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
233 |
(rename sysOfClient |
8985 | 234 |
(plam x: lessThan Nclients. rename client_map Client))" |
8311
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
235 |
|
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
236 |
|
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
237 |
(** |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
238 |
locale System = |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
239 |
fixes |
9403
aad13b59b8d9
much tidying in connection with the 2nd UNITY paper
paulson
parents:
9109
diff
changeset
|
240 |
Alloc :: 'a allocState_d program |
aad13b59b8d9
much tidying in connection with the 2nd UNITY paper
paulson
parents:
9109
diff
changeset
|
241 |
Client :: 'a clientState_d program |
8311
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
242 |
Network :: 'a systemState program |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
243 |
System :: 'a systemState program |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
244 |
|
6827 | 245 |
assumes |
246 |
Alloc "Alloc : alloc_spec" |
|
247 |
Client "Client : client_spec" |
|
248 |
Network "Network : network_spec" |
|
249 |
||
250 |
defines |
|
251 |
System_def |
|
8311
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
252 |
"System == rename sysOfAlloc Alloc |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
253 |
Join |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
254 |
Network |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
255 |
Join |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
256 |
(rename sysOfClient |
8985 | 257 |
(plam x: lessThan Nclients. rename client_map Client))" |
8311
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
258 |
**) |
8286
d4b895d3afa7
not working yet. partial conversion to use "rename" instead of "extend"
paulson
parents:
8122
diff
changeset
|
259 |
|
d4b895d3afa7
not working yet. partial conversion to use "rename" instead of "extend"
paulson
parents:
8122
diff
changeset
|
260 |
|
6815 | 261 |
end |