65 (** Client specification (required) ***) |
65 (** Client specification (required) ***) |
66 |
66 |
67 (*spec (3) PROBABLY REQUIRES A LOCALTO PRECONDITION*) |
67 (*spec (3) PROBABLY REQUIRES A LOCALTO PRECONDITION*) |
68 client_increasing :: clientState program set |
68 client_increasing :: clientState program set |
69 "client_increasing == |
69 "client_increasing == |
70 UNIV guar Increasing ask Int Increasing rel" |
70 UNIV guarantees Increasing ask Int Increasing rel" |
71 |
71 |
72 (*spec (4)*) |
72 (*spec (4)*) |
73 client_bounded :: clientState program set |
73 client_bounded :: clientState program set |
74 "client_bounded == |
74 "client_bounded == |
75 UNIV guar Always {s. ALL elt : set (ask s). elt <= NbT}" |
75 UNIV guarantees Always {s. ALL elt : set (ask s). elt <= NbT}" |
76 |
76 |
77 (*spec (5)*) |
77 (*spec (5)*) |
78 client_progress :: clientState program set |
78 client_progress :: clientState program set |
79 "client_progress == |
79 "client_progress == |
80 Increasing giv |
80 Increasing giv |
81 guar |
81 guarantees |
82 (INT h. {s. h <= giv s & h pfixGe ask s} |
82 (INT h. {s. h <= giv s & h pfixGe ask s} |
83 LeadsTo |
83 LeadsTo |
84 {s. tokens h <= (tokens o rel) s})" |
84 {s. tokens h <= (tokens o rel) s})" |
85 |
85 |
86 client_spec :: clientState program set |
86 client_spec :: clientState program set |
90 |
90 |
91 (*spec (6) PROBABLY REQUIRES A LOCALTO PRECONDITION*) |
91 (*spec (6) PROBABLY REQUIRES A LOCALTO PRECONDITION*) |
92 alloc_increasing :: allocState program set |
92 alloc_increasing :: allocState program set |
93 "alloc_increasing == |
93 "alloc_increasing == |
94 UNIV |
94 UNIV |
95 guar |
95 guarantees |
96 (INT i : lessThan Nclients. Increasing (sub i o allocAsk))" |
96 (INT i : lessThan Nclients. Increasing (sub i o allocAsk))" |
97 |
97 |
98 (*spec (7)*) |
98 (*spec (7)*) |
99 alloc_safety :: allocState program set |
99 alloc_safety :: allocState program set |
100 "alloc_safety == |
100 "alloc_safety == |
101 (INT i : lessThan Nclients. Increasing (sub i o allocRel)) |
101 (INT i : lessThan Nclients. Increasing (sub i o allocRel)) |
102 guar |
102 guarantees |
103 Always {s. sum (%i. (tokens o sub i o allocGiv) s) Nclients |
103 Always {s. sum (%i. (tokens o sub i o allocGiv) s) Nclients |
104 <= NbT + sum (%i. (tokens o sub i o allocRel) s) Nclients}" |
104 <= NbT + sum (%i. (tokens o sub i o allocRel) s) Nclients}" |
105 |
105 |
106 (*spec (8)*) |
106 (*spec (8)*) |
107 alloc_progress :: allocState program set |
107 alloc_progress :: allocState program set |
114 allocAsk s i ! k <= NbT} |
114 allocAsk s i ! k <= NbT} |
115 Int |
115 Int |
116 (INT i : lessThan Nclients. |
116 (INT i : lessThan Nclients. |
117 INT h. {s. h <= (sub i o allocGiv)s & h pfixGe (sub i o allocAsk)s} |
117 INT h. {s. h <= (sub i o allocGiv)s & h pfixGe (sub i o allocAsk)s} |
118 LeadsTo {s. tokens h <= (tokens o sub i o allocRel)s}) |
118 LeadsTo {s. tokens h <= (tokens o sub i o allocRel)s}) |
119 guar |
119 guarantees |
120 (INT i : lessThan Nclients. |
120 (INT i : lessThan Nclients. |
121 INT h. {s. h <= (sub i o allocAsk) s} LeadsTo |
121 INT h. {s. h <= (sub i o allocAsk) s} LeadsTo |
122 {s. h pfixLe (sub i o allocGiv) s})" |
122 {s. h pfixLe (sub i o allocGiv) s})" |
123 |
123 |
124 alloc_spec :: allocState program set |
124 alloc_spec :: allocState program set |
128 |
128 |
129 (*spec (9.1)*) |
129 (*spec (9.1)*) |
130 network_ask :: systemState program set |
130 network_ask :: systemState program set |
131 "network_ask == INT i : lessThan Nclients. |
131 "network_ask == INT i : lessThan Nclients. |
132 Increasing (ask o sub i o client) |
132 Increasing (ask o sub i o client) |
133 guar |
133 guarantees |
134 ((sub i o allocAsk) Fols (ask o sub i o client))" |
134 ((sub i o allocAsk) Fols (ask o sub i o client))" |
135 |
135 |
136 (*spec (9.2)*) |
136 (*spec (9.2)*) |
137 network_giv :: systemState program set |
137 network_giv :: systemState program set |
138 "network_giv == INT i : lessThan Nclients. |
138 "network_giv == INT i : lessThan Nclients. |
139 Increasing (sub i o allocGiv) |
139 Increasing (sub i o allocGiv) |
140 guar |
140 guarantees |
141 ((giv o sub i o client) Fols (sub i o allocGiv))" |
141 ((giv o sub i o client) Fols (sub i o allocGiv))" |
142 |
142 |
143 (*spec (9.3)*) |
143 (*spec (9.3)*) |
144 network_rel :: systemState program set |
144 network_rel :: systemState program set |
145 "network_rel == INT i : lessThan Nclients. |
145 "network_rel == INT i : lessThan Nclients. |
146 Increasing (rel o sub i o client) |
146 Increasing (rel o sub i o client) |
147 guar |
147 guarantees |
148 ((sub i o allocRel) Fols (rel o sub i o client))" |
148 ((sub i o allocRel) Fols (rel o sub i o client))" |
149 |
149 |
150 network_spec :: systemState program set |
150 network_spec :: systemState program set |
151 "network_spec == network_ask Int network_giv Int network_rel" |
151 "network_spec == network_ask Int network_giv Int network_rel" |
152 |
152 |