86 client_progress :: clientState program set |
86 client_progress :: clientState program set |
87 "client_progress == |
87 "client_progress == |
88 Increasing giv |
88 Increasing giv |
89 guarantees[funPair rel ask] |
89 guarantees[funPair rel ask] |
90 (INT h. {s. h <= giv s & h pfixGe ask s} |
90 (INT h. {s. h <= giv s & h pfixGe ask s} |
91 LeadsTo[givenBy (funPair rel ask)] |
91 Ensures {s. tokens h <= (tokens o rel) s})" |
92 {s. tokens h <= (tokens o rel) s})" |
|
93 |
92 |
94 (*spec: preserves part*) |
93 (*spec: preserves part*) |
95 client_preserves :: clientState program set |
94 client_preserves :: clientState program set |
96 "client_preserves == preserves giv" |
95 "client_preserves == preserves giv" |
97 |
96 |
99 "client_spec == client_increasing Int client_bounded Int client_progress |
98 "client_spec == client_increasing Int client_bounded Int client_progress |
100 Int client_preserves" |
99 Int client_preserves" |
101 |
100 |
102 (** Allocator specification (required) ***) |
101 (** Allocator specification (required) ***) |
103 |
102 |
|
103 (*Specified over the systemState, not the allocState, since then the |
|
104 leads-to properties could not be transferred to extend sysOfAlloc Alloc*) |
|
105 |
104 (*spec (6)*) |
106 (*spec (6)*) |
105 alloc_increasing :: allocState program set |
107 alloc_increasing :: systemState program set |
106 "alloc_increasing == |
108 "alloc_increasing == |
107 UNIV |
109 UNIV |
108 guarantees[allocGiv] |
110 guarantees[allocGiv] |
109 (INT i : lessThan Nclients. Increasing (sub i o allocGiv))" |
111 (INT i : lessThan Nclients. Increasing (sub i o allocGiv))" |
110 |
112 |
111 (*spec (7)*) |
113 (*spec (7)*) |
112 alloc_safety :: allocState program set |
114 alloc_safety :: systemState program set |
113 "alloc_safety == |
115 "alloc_safety == |
114 (INT i : lessThan Nclients. Increasing (sub i o allocRel)) |
116 (INT i : lessThan Nclients. Increasing (sub i o allocRel)) |
115 guarantees[allocGiv] |
117 guarantees[allocGiv] |
116 Always {s. sum (%i. (tokens o sub i o allocGiv) s) Nclients |
118 Always {s. sum (%i. (tokens o sub i o allocGiv) s) Nclients |
117 <= NbT + sum (%i. (tokens o sub i o allocRel) s) Nclients}" |
119 <= NbT + sum (%i. (tokens o sub i o allocRel) s) Nclients}" |
118 |
120 |
119 (*spec (8)*) |
121 (*spec (8)*) |
120 alloc_progress :: allocState program set |
122 alloc_progress :: systemState program set |
121 "alloc_progress == |
123 "alloc_progress == |
122 (INT i : lessThan Nclients. Increasing (sub i o allocAsk) Int |
124 (INT i : lessThan Nclients. Increasing (sub i o allocAsk) Int |
123 Increasing (sub i o allocRel)) |
125 Increasing (sub i o allocRel)) |
124 Int |
126 Int |
125 Always {s. ALL i : lessThan Nclients. |
127 Always {s. ALL i : lessThan Nclients. |
130 LeadsTo |
132 LeadsTo |
131 {s. tokens h <= (tokens o sub i o allocRel)s}) |
133 {s. tokens h <= (tokens o sub i o allocRel)s}) |
132 guarantees[allocGiv] |
134 guarantees[allocGiv] |
133 (INT i : lessThan Nclients. |
135 (INT i : lessThan Nclients. |
134 INT h. {s. h <= (sub i o allocAsk) s} |
136 INT h. {s. h <= (sub i o allocAsk) s} |
135 LeadsTo[givenBy allocGiv] |
137 LeadsTo |
136 {s. h pfixLe (sub i o allocGiv) s})" |
138 {s. h pfixLe (sub i o allocGiv) s})" |
137 |
139 |
138 (*spec: preserves part*) |
140 (*spec: preserves part*) |
139 alloc_preserves :: allocState program set |
141 alloc_preserves :: systemState program set |
140 "alloc_preserves == preserves (funPair allocRel allocAsk)" |
142 "alloc_preserves == preserves (funPair client (funPair allocRel allocAsk))" |
141 |
143 |
142 alloc_spec :: allocState program set |
144 alloc_spec :: systemState program set |
143 "alloc_spec == alloc_increasing Int alloc_safety Int alloc_progress Int |
145 "alloc_spec == alloc_increasing Int alloc_safety Int alloc_progress Int |
144 alloc_preserves" |
146 alloc_preserves" |
145 |
147 |
146 (** Network specification ***) |
148 (** Network specification ***) |
147 |
149 |
188 "sysOfClient == %(x,y). sysOfAlloc(y,x)" |
190 "sysOfClient == %(x,y). sysOfAlloc(y,x)" |
189 |
191 |
190 |
192 |
191 locale System = |
193 locale System = |
192 fixes |
194 fixes |
193 Alloc :: allocState program |
195 Alloc :: systemState program |
194 Client :: clientState program |
196 Client :: clientState program |
195 Network :: systemState program |
197 Network :: systemState program |
196 System :: systemState program |
198 System :: systemState program |
197 |
199 |
198 assumes |
200 assumes |