-
Notifications
You must be signed in to change notification settings - Fork 0
/
m10.bcm
348 lines (348 loc) · 91 KB
/
m10.bcm
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
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<org.eventb.core.scMachineFile org.eventb.core.accurate="true" org.eventb.core.configuration="org.eventb.core.fwd;ch.ethz.eventb.qualprob.qpConfig">
<org.eventb.core.scRefinesMachine name="'" org.eventb.core.scTarget="/Test/m9.bcm" org.eventb.core.source="/Test/m10.bum|org.eventb.core.machineFile#m10|org.eventb.core.refinesMachine#'"/>
<org.eventb.core.scSeesContext name="(" org.eventb.core.scTarget="/Test/c0.bcc" org.eventb.core.source="/Test/m10.bum|org.eventb.core.machineFile#m10|org.eventb.core.seesContext#_tdtnUBy0Ee61L_Ef0FP_Qw"/>
<org.eventb.core.scInternalContext name="c0">
<org.eventb.core.scAxiom name="'" org.eventb.core.label="axm1" org.eventb.core.predicate="finite(UNIT)∧finite(ORG)∧finite(ROLE)∧finite(EMPLOYEE)∧finite(CONTEXT)" org.eventb.core.source="/Test/c0.buc|org.eventb.core.contextFile#c0|org.eventb.core.axiom#_p2XGIhy0Ee61L_Ef0FP_Qx" org.eventb.core.theorem="false"/>
<org.eventb.core.scAxiom name="(" org.eventb.core.label="axm2" org.eventb.core.predicate="finite(PERMISSION)" org.eventb.core.source="/Test/c0.buc|org.eventb.core.contextFile#c0|org.eventb.core.axiom#_p2XGIhy0Ee61L_Ef0FP_Qy" org.eventb.core.theorem="false"/>
<org.eventb.core.scAxiom name=")" org.eventb.core.label="axm3" org.eventb.core.predicate="finite(ACTIVITY)∧finite(ACTION)∧finite(VIEW)∧finite(RESOURCE)" org.eventb.core.source="/Test/c0.buc|org.eventb.core.contextFile#c0|org.eventb.core.axiom#_p2XGIhy0Ee61L_Ef0FP_Qz" org.eventb.core.theorem="false"/>
<org.eventb.core.scAxiom name="*" org.eventb.core.label="axm4" org.eventb.core.predicate="finite(COR)" org.eventb.core.source="/Test/c0.buc|org.eventb.core.contextFile#c0|org.eventb.core.axiom#_p2XGIhy0Ee61L_Ef0FP_Q\|" org.eventb.core.theorem="false"/>
<org.eventb.core.scAxiom name="+" org.eventb.core.label="axm5" org.eventb.core.predicate="GLOBAL_DEADLINE∈ℕ1" org.eventb.core.source="/Test/c0.buc|org.eventb.core.contextFile#c0|org.eventb.core.axiom#_p2XGIhy0Ee61L_Ef0FP_Q~" org.eventb.core.theorem="false"/>
<org.eventb.core.scAxiom name="," org.eventb.core.label="axm7" org.eventb.core.predicate="POSITION=1 ‥ 100" org.eventb.core.source="/Test/c0.buc|org.eventb.core.contextFile#c0|org.eventb.core.axiom#_p2XGIhy0Ee61L_Ef0FP_R*" org.eventb.core.theorem="false"/>
<org.eventb.core.scAxiom name="-" org.eventb.core.label="axm8" org.eventb.core.predicate="DEADLINE=ℕ" org.eventb.core.source="/Test/c0.buc|org.eventb.core.contextFile#c0|org.eventb.core.axiom#_p2XGIhy0Ee61L_Ef0FP_R," org.eventb.core.theorem="false"/>
<org.eventb.core.scAxiom name="." org.eventb.core.label="axm6" org.eventb.core.predicate="APPROVER=UNIT × POSITION × DEADLINE" org.eventb.core.source="/Test/c0.buc|org.eventb.core.contextFile#c0|org.eventb.core.axiom#_p2XGIhy0Ee61L_Ef0FP_R(" org.eventb.core.theorem="false"/>
<org.eventb.core.scAxiom name="/" org.eventb.core.label="axm9" org.eventb.core.predicate="isTrue∈CONTEXT → 0 ‥ 1" org.eventb.core.source="/Test/c0.buc|org.eventb.core.contextFile#c0|org.eventb.core.axiom#_p2XGIhy0Ee61L_Ef0FP_R." org.eventb.core.theorem="false"/>
<org.eventb.core.scAxiom name="0" org.eventb.core.label="axm10" org.eventb.core.predicate="card(CONTEXT)=1000" org.eventb.core.source="/Test/c0.buc|org.eventb.core.contextFile#c0|org.eventb.core.axiom#_p2XGIhy0Ee61L_Ef0FP_R\/" org.eventb.core.theorem="false"/>
<org.eventb.core.scCarrierSet name="ROLE" org.eventb.core.source="/Test/c0.buc|org.eventb.core.contextFile#c0|org.eventb.core.carrierSet#_p2WfEBy0Ee61L_Ef0FP_Qw" org.eventb.core.type="ℙ(ROLE)"/>
<org.eventb.core.scConstant name="isTrue" org.eventb.core.source="/Test/c0.buc|org.eventb.core.contextFile#c0|org.eventb.core.constant#_p2XGIhy0Ee61L_Ef0FP_R-" org.eventb.core.type="ℙ(CONTEXT×ℤ)"/>
<org.eventb.core.scCarrierSet name="ACTION" org.eventb.core.source="/Test/c0.buc|org.eventb.core.contextFile#c0|org.eventb.core.carrierSet#_p2XGIRy0Ee61L_Ef0FP_Qw" org.eventb.core.type="ℙ(ACTION)"/>
<org.eventb.core.scCarrierSet name="ACTIVITY" org.eventb.core.source="/Test/c0.buc|org.eventb.core.contextFile#c0|org.eventb.core.carrierSet#_p2WfFBy0Ee61L_Ef0FP_Qw" org.eventb.core.type="ℙ(ACTIVITY)"/>
<org.eventb.core.scCarrierSet name="UNIT" org.eventb.core.source="/Test/c0.buc|org.eventb.core.contextFile#c0|org.eventb.core.carrierSet#_p2V4ABy0Ee61L_Ef0FP_Qw" org.eventb.core.type="ℙ(UNIT)"/>
<org.eventb.core.scCarrierSet name="CONTEXT" org.eventb.core.source="/Test/c0.buc|org.eventb.core.contextFile#c0|org.eventb.core.carrierSet#_p2WfEhy0Ee61L_Ef0FP_Qw" org.eventb.core.type="ℙ(CONTEXT)"/>
<org.eventb.core.scConstant name="POSITION" org.eventb.core.source="/Test/c0.buc|org.eventb.core.contextFile#c0|org.eventb.core.constant#_p2XGIhy0Ee61L_Ef0FP_R)" org.eventb.core.type="ℙ(ℤ)"/>
<org.eventb.core.scCarrierSet name="VIEW" org.eventb.core.source="/Test/c0.buc|org.eventb.core.contextFile#c0|org.eventb.core.carrierSet#_p2WfExy0Ee61L_Ef0FP_Qw" org.eventb.core.type="ℙ(VIEW)"/>
<org.eventb.core.scCarrierSet name="ORG" org.eventb.core.source="/Test/c0.buc|org.eventb.core.contextFile#c0|org.eventb.core.carrierSet#_p2V4ARy0Ee61L_Ef0FP_Qw" org.eventb.core.type="ℙ(ORG)"/>
<org.eventb.core.scCarrierSet name="EMPLOYEE" org.eventb.core.source="/Test/c0.buc|org.eventb.core.contextFile#c0|org.eventb.core.carrierSet#_p2WfERy0Ee61L_Ef0FP_Qw" org.eventb.core.type="ℙ(EMPLOYEE)"/>
<org.eventb.core.scConstant name="APPROVER" org.eventb.core.source="/Test/c0.buc|org.eventb.core.contextFile#c0|org.eventb.core.constant#_p2XGIhy0Ee61L_Ef0FP_R'" org.eventb.core.type="ℙ(UNIT×ℤ×ℤ)"/>
<org.eventb.core.scCarrierSet name="COR" org.eventb.core.source="/Test/c0.buc|org.eventb.core.contextFile#c0|org.eventb.core.carrierSet#_p2XGIhy0Ee61L_Ef0FP_Q{" org.eventb.core.type="ℙ(COR)"/>
<org.eventb.core.scCarrierSet name="RESOURCE" org.eventb.core.source="/Test/c0.buc|org.eventb.core.contextFile#c0|org.eventb.core.carrierSet#_p2XGIBy0Ee61L_Ef0FP_Qw" org.eventb.core.type="ℙ(RESOURCE)"/>
<org.eventb.core.scConstant name="GLOBAL_DEADLINE" org.eventb.core.source="/Test/c0.buc|org.eventb.core.contextFile#c0|org.eventb.core.constant#_p2XGIhy0Ee61L_Ef0FP_Q}" org.eventb.core.type="ℤ"/>
<org.eventb.core.scConstant name="DEADLINE" org.eventb.core.source="/Test/c0.buc|org.eventb.core.contextFile#c0|org.eventb.core.constant#_p2XGIhy0Ee61L_Ef0FP_R+" org.eventb.core.type="ℙ(ℤ)"/>
<org.eventb.core.scCarrierSet name="PERMISSION" org.eventb.core.source="/Test/c0.buc|org.eventb.core.contextFile#c0|org.eventb.core.carrierSet#_p2XGIhy0Ee61L_Ef0FP_Qw" org.eventb.core.type="ℙ(PERMISSION)"/>
</org.eventb.core.scInternalContext>
<org.eventb.core.scInvariant name="c1" org.eventb.core.label="inv1" org.eventb.core.predicate="CiO⊆CONTEXT × ORG" org.eventb.core.source="/Test/m0.bum|org.eventb.core.machineFile#m0|org.eventb.core.invariant#_tdyf0xy0Ee61L_Ef0FP_Qw" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="c2" org.eventb.core.label="inv2" org.eventb.core.predicate="root∈ORG ⇸ UNIT" org.eventb.core.source="/Test/m0.bum|org.eventb.core.machineFile#m0|org.eventb.core.invariant#_tdzG4By0Ee61L_Ef0FP_Qw" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="c3" org.eventb.core.label="inv3" org.eventb.core.predicate="OU∈UNIT ⇸ ORG" org.eventb.core.source="/Test/m0.bum|org.eventb.core.machineFile#m0|org.eventb.core.invariant#_tdzG4Ry0Ee61L_Ef0FP_Qw" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="c4" org.eventb.core.label="inv4" org.eventb.core.predicate="AiO⊆ACTIVITY × ORG" org.eventb.core.source="/Test/m0.bum|org.eventb.core.machineFile#m0|org.eventb.core.invariant#_tdzG4hy0Ee61L_Ef0FP_Qw" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="c5" org.eventb.core.label="inv5" org.eventb.core.predicate="UH∈UNIT ⇸ UNIT" org.eventb.core.source="/Test/m0.bum|org.eventb.core.machineFile#m0|org.eventb.core.invariant#_tdzG4xy0Ee61L_Ef0FP_Qw" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="c6" org.eventb.core.label="inv6" org.eventb.core.predicate="ViO⊆VIEW × ORG" org.eventb.core.source="/Test/m0.bum|org.eventb.core.machineFile#m0|org.eventb.core.invariant#_tdzt8By0Ee61L_Ef0FP_Qw" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="c7" org.eventb.core.label="inv7" org.eventb.core.predicate="RiO⊆ROLE × ORG" org.eventb.core.source="/Test/m0.bum|org.eventb.core.machineFile#m0|org.eventb.core.invariant#_tdzt8Ry0Ee61L_Ef0FP_Qw" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="c8" org.eventb.core.label="inv8" org.eventb.core.predicate="CA⊆COR × UNIT × POSITION × DEADLINE" org.eventb.core.source="/Test/m0.bum|org.eventb.core.machineFile#m0|org.eventb.core.invariant#_tdzt8hy0Ee61L_Ef0FP_Qw" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="c9" org.eventb.core.label="inv9" org.eventb.core.predicate="PCA∈PERMISSION ⇸ COR" org.eventb.core.source="/Test/m0.bum|org.eventb.core.machineFile#m0|org.eventb.core.invariant#_tdzt8xy0Ee61L_Ef0FP_Qw" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="c:" org.eventb.core.label="inv10" org.eventb.core.predicate="PRA∈PERMISSION ⇸ RiO" org.eventb.core.source="/Test/m0.bum|org.eventb.core.machineFile#m0|org.eventb.core.invariant#_tdzt9By0Ee61L_Ef0FP_Qw" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="c;" org.eventb.core.label="inv11" org.eventb.core.predicate="EA⊆EMPLOYEE × UNIT" org.eventb.core.source="/Test/m0.bum|org.eventb.core.machineFile#m0|org.eventb.core.invariant#_td0VABy0Ee61L_Ef0FP_Qw" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="c=" org.eventb.core.label="inv12" org.eventb.core.predicate="UR⊆UNIT × RiO" org.eventb.core.source="/Test/m0.bum|org.eventb.core.machineFile#m0|org.eventb.core.invariant#_td0VARy0Ee61L_Ef0FP_Qw" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="c>" org.eventb.core.label="inv13" org.eventb.core.predicate="PAA∈PERMISSION ⇸ AiO" org.eventb.core.source="/Test/m0.bum|org.eventb.core.machineFile#m0|org.eventb.core.invariant#_td0VAhy0Ee61L_Ef0FP_Qw" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="c?" org.eventb.core.label="inv14" org.eventb.core.predicate="PVA∈PERMISSION ⇸ ViO" org.eventb.core.source="/Test/m0.bum|org.eventb.core.machineFile#m0|org.eventb.core.invariant#_td0VAxy0Ee61L_Ef0FP_Qw" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="c@" org.eventb.core.label="inv15" org.eventb.core.predicate="PCxA∈PERMISSION ⇸ CiO" org.eventb.core.source="/Test/m0.bum|org.eventb.core.machineFile#m0|org.eventb.core.invariant#_td0VBBy0Ee61L_Ef0FP_Qw" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="cA" org.eventb.core.label="inv16" org.eventb.core.predicate="AV⊆ACTION × ViO" org.eventb.core.source="/Test/m0.bum|org.eventb.core.machineFile#m0|org.eventb.core.invariant#_td08EBy0Ee61L_Ef0FP_Qw" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="cB" org.eventb.core.label="inv17" org.eventb.core.predicate="AA⊆ACTION × AiO" org.eventb.core.source="/Test/m0.bum|org.eventb.core.machineFile#m0|org.eventb.core.invariant#_td08ERy0Ee61L_Ef0FP_Qw" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="cC" org.eventb.core.label="inv18" org.eventb.core.predicate="RV⊆RESOURCE × ViO" org.eventb.core.source="/Test/m0.bum|org.eventb.core.machineFile#m0|org.eventb.core.invariant#_td08Ehy0Ee61L_Ef0FP_Qw" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="cD" org.eventb.core.label="inv2" org.eventb.core.predicate="UH1∈UNIT ⇸ UNIT" org.eventb.core.source="/Test/m1.bum|org.eventb.core.machineFile#m1|org.eventb.core.invariant#_tdyf0hy0Ee61L_Ef0FP_R)" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="cE" org.eventb.core.label="inv3" org.eventb.core.predicate="UH1∩(id ⦂ ℙ(UNIT×UNIT))=(∅ ⦂ ℙ(UNIT×UNIT))" org.eventb.core.source="/Test/m1.bum|org.eventb.core.machineFile#m1|org.eventb.core.invariant#_tdyf0hy0Ee61L_Ef0FP_R," org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="cF" org.eventb.core.label="inv4" org.eventb.core.predicate="UH1∩UH1∼=(∅ ⦂ ℙ(UNIT×UNIT))" org.eventb.core.source="/Test/m1.bum|org.eventb.core.machineFile#m1|org.eventb.core.invariant#_tdyf0hy0Ee61L_Ef0FP_Q}" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="cG" org.eventb.core.label="inv5" org.eventb.core.predicate="∀u1⦂UNIT,u2⦂UNIT,u3⦂UNIT·u1 ↦ u2∈UH1∧u1 ↦ u3∈UH1⇒u2=u3" org.eventb.core.source="/Test/m1.bum|org.eventb.core.machineFile#m1|org.eventb.core.invariant#_tdyf0hy0Ee61L_Ef0FP_Q~" org.eventb.core.theorem="true"/>
<org.eventb.core.scInvariant name="cH" org.eventb.core.label="inv7" org.eventb.core.predicate="OU1∈UNIT ⇸ ORG" org.eventb.core.source="/Test/m1.bum|org.eventb.core.machineFile#m1|org.eventb.core.invariant#_tdyf0hy0Ee61L_Ef0FP_R\/" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="cI" org.eventb.core.label="inv1" org.eventb.core.predicate="root1∈ORG ⇸ dom(OU1)" org.eventb.core.source="/Test/m1.bum|org.eventb.core.machineFile#m1|org.eventb.core.invariant#_tdyf0hy0Ee61L_Ef0FP_Q\|" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="cJ" org.eventb.core.label="inv10" org.eventb.core.predicate="∀org1⦂ORG,org2⦂ORG,u⦂UNIT·org1 ↦ u∈root1∧org2 ↦ u∈root1⇒org1=org2" org.eventb.core.source="/Test/m1.bum|org.eventb.core.machineFile#m1|org.eventb.core.invariant#_tdyf0hy0Ee61L_Ef0FP_R3" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="cK" org.eventb.core.label="inv6" org.eventb.core.predicate="ran(root1)∩dom(UH1)=(∅ ⦂ ℙ(UNIT))" org.eventb.core.source="/Test/m1.bum|org.eventb.core.machineFile#m1|org.eventb.core.invariant#_tdyf0hy0Ee61L_Ef0FP_R'" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="cL" org.eventb.core.label="inv8" org.eventb.core.predicate="∀u⦂UNIT,org⦂ORG·org ↦ u∈root1⇒u ↦ org∈OU1" org.eventb.core.source="/Test/m1.bum|org.eventb.core.machineFile#m1|org.eventb.core.invariant#_tdyf0hy0Ee61L_Ef0FP_R1" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="cM" org.eventb.core.label="inv9" org.eventb.core.predicate="∀us⦂UNIT,um⦂UNIT·us ↦ um∈UH1⇒(OU1[{us}]≠(∅ ⦂ ℙ(ORG))∧OU1[{um}]≠(∅ ⦂ ℙ(ORG))⇒OU1(us)=OU1(um))" org.eventb.core.source="/Test/m1.bum|org.eventb.core.machineFile#m1|org.eventb.core.invariant#_tdyf0hy0Ee61L_Ef0FP_R0" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="cN" org.eventb.core.label="inv1" org.eventb.core.predicate="RiO1⊆ROLE × ORG" org.eventb.core.source="/Test/m2.bum|org.eventb.core.machineFile#m2|org.eventb.core.invariant#_tdyf0hy0Ee61L_Ef0FP_R:" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="cO" org.eventb.core.label="inv2" org.eventb.core.predicate="UR1⊆UNIT × RiO1" org.eventb.core.source="/Test/m2.bum|org.eventb.core.machineFile#m2|org.eventb.core.invariant#_tdyf0hy0Ee61L_Ef0FP_R6" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="cP" org.eventb.core.label="inv3" org.eventb.core.predicate="∀u⦂UNIT,org⦂ORG,role⦂ROLE·u ↦ (role ↦ org)∈UR1⇒(OU1[{u}]≠(∅ ⦂ ℙ(ORG))⇒OU1(u)=org)" org.eventb.core.source="/Test/m2.bum|org.eventb.core.machineFile#m2|org.eventb.core.invariant#_tdyf0hy0Ee61L_Ef0FP_R;" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="cQ" org.eventb.core.label="inv1" org.eventb.core.predicate="EA1⊆EMPLOYEE × UNIT" org.eventb.core.source="/Test/m3.bum|org.eventb.core.machineFile#m3|org.eventb.core.invariant#_tdyf0hy0Ee61L_Ef0FP_RD" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="cR" org.eventb.core.label="inv2" org.eventb.core.predicate="∀u1⦂UNIT,u2⦂UNIT,e⦂EMPLOYEE·u1 ↦ u2∈UH1∧e ↦ u1∈EA1⇒e ↦ u2∉EA1" org.eventb.core.source="/Test/m3.bum|org.eventb.core.machineFile#m3|org.eventb.core.invariant#_tdyf0hy0Ee61L_Ef0FP_RE" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="cS" org.eventb.core.label="inv1" org.eventb.core.predicate="CA1⊆COR × UNIT × POSITION × DEADLINE" org.eventb.core.source="/Test/m4.bum|org.eventb.core.machineFile#m4|org.eventb.core.invariant#_tdyf0hy0Ee61L_Ef0FP_RN" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="cT" org.eventb.core.label="inv3" org.eventb.core.predicate="PRA1∈PERMISSION ⇸ RiO1" org.eventb.core.source="/Test/m4.bum|org.eventb.core.machineFile#m4|org.eventb.core.invariant#_tdyf0hy0Ee61L_Ef0FP_RV" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="cU" org.eventb.core.label="inv4" org.eventb.core.predicate="PAA1∈PERMISSION ⇸ AiO" org.eventb.core.source="/Test/m4.bum|org.eventb.core.machineFile#m4|org.eventb.core.invariant#_tdyf0hy0Ee61L_Ef0FP_RW" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="cV" org.eventb.core.label="inv5" org.eventb.core.predicate="PVA1∈PERMISSION ⇸ ViO" org.eventb.core.source="/Test/m4.bum|org.eventb.core.machineFile#m4|org.eventb.core.invariant#_tdyf0hy0Ee61L_Ef0FP_RX" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="cW" org.eventb.core.label="inv6" org.eventb.core.predicate="PCA1∈PERMISSION ⇸ COR" org.eventb.core.source="/Test/m4.bum|org.eventb.core.machineFile#m4|org.eventb.core.invariant#_tdyf0hy0Ee61L_Ef0FP_RY" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="cX" org.eventb.core.label="inv7" org.eventb.core.predicate="PCxA1∈PERMISSION ⇸ CiO" org.eventb.core.source="/Test/m4.bum|org.eventb.core.machineFile#m4|org.eventb.core.invariant#_tdyf0hy0Ee61L_Ef0FP_RZ" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="cY" org.eventb.core.label="inv2" org.eventb.core.predicate="∀cor⦂COR,u1⦂UNIT,p1⦂ℤ,d1⦂ℤ,u2⦂UNIT,p2⦂ℤ,d2⦂ℤ·cor ↦ u1 ↦ p1 ↦ d1∈CA1∧cor ↦ u2 ↦ p2 ↦ d2∈CA1∧u1≠u2⇒(OU1[{u1}]≠(∅ ⦂ ℙ(ORG))∧OU1[{u2}]≠(∅ ⦂ ℙ(ORG))⇒OU1(u1)=OU1(u2))" org.eventb.core.source="/Test/m4.bum|org.eventb.core.machineFile#m4|org.eventb.core.invariant#_tdyf0hy0Ee61L_Ef0FP_RO" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="cZ" org.eventb.core.label="inv1" org.eventb.core.predicate="ViO1⊆VIEW × ORG" org.eventb.core.source="/Test/m5.bum|org.eventb.core.machineFile#m5|org.eventb.core.invariant#_tdyf0hy0Ee61L_Ef0FP_Rb" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="c[" org.eventb.core.label="inv2" org.eventb.core.predicate="RV1⊆RESOURCE × ViO1" org.eventb.core.source="/Test/m5.bum|org.eventb.core.machineFile#m5|org.eventb.core.invariant#_tdyf0hy0Ee61L_Ef0FP_Re" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="c\" org.eventb.core.label="inv1" org.eventb.core.predicate="AiO1⊆ACTIVITY × ORG" org.eventb.core.source="/Test/m6.bum|org.eventb.core.machineFile#m6|org.eventb.core.invariant#_tdyf0hy0Ee61L_Ef0FP_Rv" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="c]" org.eventb.core.label="inv2" org.eventb.core.predicate="AV1⊆ACTION × ViO1" org.eventb.core.source="/Test/m6.bum|org.eventb.core.machineFile#m6|org.eventb.core.invariant#_tdyf0hy0Ee61L_Ef0FP_Rw" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="c^" org.eventb.core.label="inv3" org.eventb.core.predicate="AA1⊆ACTION × AiO1" org.eventb.core.source="/Test/m6.bum|org.eventb.core.machineFile#m6|org.eventb.core.invariant#_tdyf0hy0Ee61L_Ef0FP_Rx" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="c_" org.eventb.core.label="inv1" org.eventb.core.predicate="CiO1⊆CONTEXT × ORG" org.eventb.core.source="/Test/m7.bum|org.eventb.core.machineFile#m7|org.eventb.core.invariant#_tdyf0hy0Ee61L_Ef0FP_S." org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="c`" org.eventb.core.label="inv1" org.eventb.core.predicate="Access_Requested⊆ℕ1 × EMPLOYEE × ACTION × RESOURCE × DEADLINE × ℕ × CONTEXT" org.eventb.core.source="/Test/m9.bum|org.eventb.core.machineFile#m9|org.eventb.core.invariant#_tdyf0hy0Ee61L_Ef0FP_S@" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="ca" org.eventb.core.label="inv2" org.eventb.core.predicate="PDistA∈PERMISSION ⇸ ℕ" org.eventb.core.source="/Test/m9.bum|org.eventb.core.machineFile#m9|org.eventb.core.invariant#_tdyf0hy0Ee61L_Ef0FP_SC" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="cb" org.eventb.core.label="inv3" org.eventb.core.predicate="PAcA∈PERMISSION ⇸ CiO" org.eventb.core.source="/Test/m9.bum|org.eventb.core.machineFile#m9|org.eventb.core.invariant#_tdyf0hy0Ee61L_Ef0FP_SE" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="cc" org.eventb.core.label="inv1" org.eventb.core.predicate="Request_Treated⊆ℕ1 × Access_Requested × EMPLOYEE × 0 ‥ 1" org.eventb.core.source="/Test/m10.bum|org.eventb.core.machineFile#m10|org.eventb.core.invariant#_tdyf0hy0Ee61L_Ef0FP_SR" org.eventb.core.theorem="false"/>
<org.eventb.core.scVariable name="AiO1" org.eventb.core.abstract="true" org.eventb.core.concrete="true" org.eventb.core.source="/Test/m10.bum|org.eventb.core.machineFile#m10|org.eventb.core.variable#_tdyf0hy0Ee61L_Ef0FP_Rs" org.eventb.core.type="ℙ(ACTIVITY×ORG)"/>
<org.eventb.core.scVariable name="AA" org.eventb.core.abstract="true" org.eventb.core.concrete="true" org.eventb.core.source="/Test/m10.bum|org.eventb.core.machineFile#m10|org.eventb.core.variable#_tdyf0hy0Ee61L_Ef0FP_Qw" org.eventb.core.type="ℙ(ACTION×(ACTIVITY×ORG))"/>
<org.eventb.core.scVariable name="AV" org.eventb.core.abstract="true" org.eventb.core.concrete="true" org.eventb.core.source="/Test/m10.bum|org.eventb.core.machineFile#m10|org.eventb.core.variable#_tdyf0Ry0Ee61L_Ef0FP_Qw" org.eventb.core.type="ℙ(ACTION×(VIEW×ORG))"/>
<org.eventb.core.scVariable name="CA" org.eventb.core.abstract="true" org.eventb.core.concrete="true" org.eventb.core.source="/Test/m10.bum|org.eventb.core.machineFile#m10|org.eventb.core.variable#_tdwqoRy0Ee61L_Ef0FP_Qw" org.eventb.core.type="ℙ(COR×UNIT×ℤ×ℤ)"/>
<org.eventb.core.scVariable name="CiO" org.eventb.core.abstract="true" org.eventb.core.concrete="true" org.eventb.core.source="/Test/m10.bum|org.eventb.core.machineFile#m10|org.eventb.core.variable#_tdx4wxy0Ee61L_Ef0FP_Qw" org.eventb.core.type="ℙ(CONTEXT×ORG)"/>
<org.eventb.core.scVariable name="EA" org.eventb.core.abstract="true" org.eventb.core.concrete="true" org.eventb.core.source="/Test/m10.bum|org.eventb.core.machineFile#m10|org.eventb.core.variable#_tdxRshy0Ee61L_Ef0FP_Qw" org.eventb.core.type="ℙ(EMPLOYEE×UNIT)"/>
<org.eventb.core.scVariable name="PVA1" org.eventb.core.abstract="true" org.eventb.core.concrete="true" org.eventb.core.source="/Test/m10.bum|org.eventb.core.machineFile#m10|org.eventb.core.variable#_tdyf0hy0Ee61L_Ef0FP_RS" org.eventb.core.type="ℙ(PERMISSION×(VIEW×ORG))"/>
<org.eventb.core.scVariable name="root" org.eventb.core.abstract="true" org.eventb.core.concrete="true" org.eventb.core.source="/Test/m10.bum|org.eventb.core.machineFile#m10|org.eventb.core.variable#_tdwqoxy0Ee61L_Ef0FP_Qw" org.eventb.core.type="ℙ(ORG×UNIT)"/>
<org.eventb.core.scVariable name="RiO" org.eventb.core.abstract="true" org.eventb.core.concrete="true" org.eventb.core.source="/Test/m10.bum|org.eventb.core.machineFile#m10|org.eventb.core.variable#_tdxRsBy0Ee61L_Ef0FP_Qw" org.eventb.core.type="ℙ(ROLE×ORG)"/>
<org.eventb.core.scVariable name="CiO1" org.eventb.core.abstract="true" org.eventb.core.concrete="true" org.eventb.core.source="/Test/m10.bum|org.eventb.core.machineFile#m10|org.eventb.core.variable#_tdyf0hy0Ee61L_Ef0FP_S-" org.eventb.core.type="ℙ(CONTEXT×ORG)"/>
<org.eventb.core.scVariable name="AiO" org.eventb.core.abstract="true" org.eventb.core.concrete="true" org.eventb.core.source="/Test/m10.bum|org.eventb.core.machineFile#m10|org.eventb.core.variable#_tdx4wBy0Ee61L_Ef0FP_Qw" org.eventb.core.type="ℙ(ACTIVITY×ORG)"/>
<org.eventb.core.scVariable name="UR1" org.eventb.core.abstract="true" org.eventb.core.concrete="true" org.eventb.core.source="/Test/m10.bum|org.eventb.core.machineFile#m10|org.eventb.core.variable#_tdyf0hy0Ee61L_Ef0FP_R5" org.eventb.core.type="ℙ(UNIT×(ROLE×ORG))"/>
<org.eventb.core.scVariable name="PCA1" org.eventb.core.abstract="true" org.eventb.core.concrete="true" org.eventb.core.source="/Test/m10.bum|org.eventb.core.machineFile#m10|org.eventb.core.variable#_tdyf0hy0Ee61L_Ef0FP_RT" org.eventb.core.type="ℙ(PERMISSION×COR)"/>
<org.eventb.core.scVariable name="Access_Requested" org.eventb.core.abstract="true" org.eventb.core.concrete="true" org.eventb.core.source="/Test/m10.bum|org.eventb.core.machineFile#m10|org.eventb.core.variable#_tdyf0hy0Ee61L_Ef0FP_S?" org.eventb.core.type="ℙ(ℤ×EMPLOYEE×ACTION×RESOURCE×ℤ×ℤ×CONTEXT)"/>
<org.eventb.core.scVariable name="PRA1" org.eventb.core.abstract="true" org.eventb.core.concrete="true" org.eventb.core.source="/Test/m10.bum|org.eventb.core.machineFile#m10|org.eventb.core.variable#_tdyf0hy0Ee61L_Ef0FP_RQ" org.eventb.core.type="ℙ(PERMISSION×(ROLE×ORG))"/>
<org.eventb.core.scVariable name="PAA1" org.eventb.core.abstract="true" org.eventb.core.concrete="true" org.eventb.core.source="/Test/m10.bum|org.eventb.core.machineFile#m10|org.eventb.core.variable#_tdyf0hy0Ee61L_Ef0FP_RR" org.eventb.core.type="ℙ(PERMISSION×(ACTIVITY×ORG))"/>
<org.eventb.core.scVariable name="OU" org.eventb.core.abstract="true" org.eventb.core.concrete="true" org.eventb.core.source="/Test/m10.bum|org.eventb.core.machineFile#m10|org.eventb.core.variable#_tdwqpBy0Ee61L_Ef0FP_Qw" org.eventb.core.type="ℙ(UNIT×ORG)"/>
<org.eventb.core.scVariable name="RV" org.eventb.core.abstract="true" org.eventb.core.concrete="true" org.eventb.core.source="/Test/m10.bum|org.eventb.core.machineFile#m10|org.eventb.core.variable#_tdyf0By0Ee61L_Ef0FP_Qw" org.eventb.core.type="ℙ(RESOURCE×(VIEW×ORG))"/>
<org.eventb.core.scVariable name="RiO1" org.eventb.core.abstract="true" org.eventb.core.concrete="true" org.eventb.core.source="/Test/m10.bum|org.eventb.core.machineFile#m10|org.eventb.core.variable#_tdyf0hy0Ee61L_Ef0FP_R9" org.eventb.core.type="ℙ(ROLE×ORG)"/>
<org.eventb.core.scVariable name="UH" org.eventb.core.abstract="true" org.eventb.core.concrete="true" org.eventb.core.source="/Test/m10.bum|org.eventb.core.machineFile#m10|org.eventb.core.variable#_tdyf0hy0Ee61L_Ef0FP_R*" org.eventb.core.type="ℙ(UNIT×UNIT)"/>
<org.eventb.core.scVariable name="UR" org.eventb.core.abstract="true" org.eventb.core.concrete="true" org.eventb.core.source="/Test/m10.bum|org.eventb.core.machineFile#m10|org.eventb.core.variable#_tdyf0hy0Ee61L_Ef0FP_R7" org.eventb.core.type="ℙ(UNIT×(ROLE×ORG))"/>
<org.eventb.core.scVariable name="OU1" org.eventb.core.abstract="true" org.eventb.core.concrete="true" org.eventb.core.source="/Test/m10.bum|org.eventb.core.machineFile#m10|org.eventb.core.variable#_tdyf0hy0Ee61L_Ef0FP_R." org.eventb.core.type="ℙ(UNIT×ORG)"/>
<org.eventb.core.scVariable name="EA1" org.eventb.core.abstract="true" org.eventb.core.concrete="true" org.eventb.core.source="/Test/m10.bum|org.eventb.core.machineFile#m10|org.eventb.core.variable#_tdyf0hy0Ee61L_Ef0FP_RC" org.eventb.core.type="ℙ(EMPLOYEE×UNIT)"/>
<org.eventb.core.scVariable name="Request_Treated" org.eventb.core.abstract="false" org.eventb.core.concrete="true" org.eventb.core.source="/Test/m10.bum|org.eventb.core.machineFile#m10|org.eventb.core.variable#_tdyf0hy0Ee61L_Ef0FP_SQ" org.eventb.core.type="ℙ(ℤ×(ℤ×EMPLOYEE×ACTION×RESOURCE×ℤ×ℤ×CONTEXT)×EMPLOYEE×ℤ)"/>
<org.eventb.core.scVariable name="PCxA1" org.eventb.core.abstract="true" org.eventb.core.concrete="true" org.eventb.core.source="/Test/m10.bum|org.eventb.core.machineFile#m10|org.eventb.core.variable#_tdyf0hy0Ee61L_Ef0FP_RU" org.eventb.core.type="ℙ(PERMISSION×(CONTEXT×ORG))"/>
<org.eventb.core.scVariable name="CA1" org.eventb.core.abstract="true" org.eventb.core.concrete="true" org.eventb.core.source="/Test/m10.bum|org.eventb.core.machineFile#m10|org.eventb.core.variable#_tdyf0hy0Ee61L_Ef0FP_RM" org.eventb.core.type="ℙ(COR×UNIT×ℤ×ℤ)"/>
<org.eventb.core.scVariable name="ViO1" org.eventb.core.abstract="true" org.eventb.core.concrete="true" org.eventb.core.source="/Test/m10.bum|org.eventb.core.machineFile#m10|org.eventb.core.variable#_tdyf0hy0Ee61L_Ef0FP_Ra" org.eventb.core.type="ℙ(VIEW×ORG)"/>
<org.eventb.core.scVariable name="AA1" org.eventb.core.abstract="true" org.eventb.core.concrete="true" org.eventb.core.source="/Test/m10.bum|org.eventb.core.machineFile#m10|org.eventb.core.variable#_tdyf0hy0Ee61L_Ef0FP_Rt" org.eventb.core.type="ℙ(ACTION×(ACTIVITY×ORG))"/>
<org.eventb.core.scVariable name="PAA" org.eventb.core.abstract="true" org.eventb.core.concrete="true" org.eventb.core.source="/Test/m10.bum|org.eventb.core.machineFile#m10|org.eventb.core.variable#_tdx4wRy0Ee61L_Ef0FP_Qw" org.eventb.core.type="ℙ(PERMISSION×(ACTIVITY×ORG))"/>
<org.eventb.core.scVariable name="PDistA" org.eventb.core.abstract="true" org.eventb.core.concrete="true" org.eventb.core.source="/Test/m10.bum|org.eventb.core.machineFile#m10|org.eventb.core.variable#_tdyf0hy0Ee61L_Ef0FP_SS" org.eventb.core.type="ℙ(PERMISSION×ℤ)"/>
<org.eventb.core.scVariable name="PCA" org.eventb.core.abstract="true" org.eventb.core.concrete="true" org.eventb.core.source="/Test/m10.bum|org.eventb.core.machineFile#m10|org.eventb.core.variable#_tdwqohy0Ee61L_Ef0FP_Qw" org.eventb.core.type="ℙ(PERMISSION×COR)"/>
<org.eventb.core.scVariable name="PAcA" org.eventb.core.abstract="true" org.eventb.core.concrete="true" org.eventb.core.source="/Test/m10.bum|org.eventb.core.machineFile#m10|org.eventb.core.variable#_tdyf0hy0Ee61L_Ef0FP_ST" org.eventb.core.type="ℙ(PERMISSION×(CONTEXT×ORG))"/>
<org.eventb.core.scVariable name="root1" org.eventb.core.abstract="true" org.eventb.core.concrete="true" org.eventb.core.source="/Test/m10.bum|org.eventb.core.machineFile#m10|org.eventb.core.variable#_tdyf0hy0Ee61L_Ef0FP_Q{" org.eventb.core.type="ℙ(ORG×UNIT)"/>
<org.eventb.core.scVariable name="RV1" org.eventb.core.abstract="true" org.eventb.core.concrete="true" org.eventb.core.source="/Test/m10.bum|org.eventb.core.machineFile#m10|org.eventb.core.variable#_tdyf0hy0Ee61L_Ef0FP_Rd" org.eventb.core.type="ℙ(RESOURCE×(VIEW×ORG))"/>
<org.eventb.core.scVariable name="PRA" org.eventb.core.abstract="true" org.eventb.core.concrete="true" org.eventb.core.source="/Test/m10.bum|org.eventb.core.machineFile#m10|org.eventb.core.variable#_tdxRsRy0Ee61L_Ef0FP_Qw" org.eventb.core.type="ℙ(PERMISSION×(ROLE×ORG))"/>
<org.eventb.core.scVariable name="AV1" org.eventb.core.abstract="true" org.eventb.core.concrete="true" org.eventb.core.source="/Test/m10.bum|org.eventb.core.machineFile#m10|org.eventb.core.variable#_tdyf0hy0Ee61L_Ef0FP_Ru" org.eventb.core.type="ℙ(ACTION×(VIEW×ORG))"/>
<org.eventb.core.scVariable name="PVA" org.eventb.core.abstract="true" org.eventb.core.concrete="true" org.eventb.core.source="/Test/m10.bum|org.eventb.core.machineFile#m10|org.eventb.core.variable#_tdx4why0Ee61L_Ef0FP_Qw" org.eventb.core.type="ℙ(PERMISSION×(VIEW×ORG))"/>
<org.eventb.core.scVariable name="PCxA" org.eventb.core.abstract="true" org.eventb.core.concrete="true" org.eventb.core.source="/Test/m10.bum|org.eventb.core.machineFile#m10|org.eventb.core.variable#_tdx4xBy0Ee61L_Ef0FP_Qw" org.eventb.core.type="ℙ(PERMISSION×(CONTEXT×ORG))"/>
<org.eventb.core.scVariable name="ViO" org.eventb.core.abstract="true" org.eventb.core.concrete="true" org.eventb.core.source="/Test/m10.bum|org.eventb.core.machineFile#m10|org.eventb.core.variable#_tdxRtBy0Ee61L_Ef0FP_Qw" org.eventb.core.type="ℙ(VIEW×ORG)"/>
<org.eventb.core.scVariable name="UH1" org.eventb.core.abstract="true" org.eventb.core.concrete="true" org.eventb.core.source="/Test/m10.bum|org.eventb.core.machineFile#m10|org.eventb.core.variable#_tdyf0hy0Ee61L_Ef0FP_R(" org.eventb.core.type="ℙ(UNIT×UNIT)"/>
<org.eventb.core.scEvent name="Access_Requestee" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="INITIALISATION" org.eventb.core.source="/Test/m10.bum|org.eventb.core.machineFile#m10|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_S@">
<org.eventb.core.scRefinesEvent name="'" org.eventb.core.scTarget="/Test/m9.bcm|org.eventb.core.scMachineFile#m9|org.eventb.core.scEvent#Access_Requestee" org.eventb.core.source="/Test/m10.bum|org.eventb.core.machineFile#m10|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_S@"/>
<org.eventb.core.scAction name="(" org.eventb.core.assignment="CiO ≔ ∅ ⦂ ℙ(CONTEXT×ORG)" org.eventb.core.label="act1" org.eventb.core.source="/Test/m10.bum|org.eventb.core.machineFile#m10|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_S@|org.eventb.core.action#_tduOYBy0Ee61L_Ef0FP_Qw"/>
<org.eventb.core.scAction name=")" org.eventb.core.assignment="root :∈ ORG ⇸ UNIT" org.eventb.core.label="act2" org.eventb.core.source="/Test/m10.bum|org.eventb.core.machineFile#m10|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_S@|org.eventb.core.action#_tduOYRy0Ee61L_Ef0FP_Qw"/>
<org.eventb.core.scAction name="*" org.eventb.core.assignment="OU :∈ UNIT ⇸ ORG" org.eventb.core.label="act3" org.eventb.core.source="/Test/m10.bum|org.eventb.core.machineFile#m10|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_S@|org.eventb.core.action#_tdu1cBy0Ee61L_Ef0FP_Qw"/>
<org.eventb.core.scAction name="+" org.eventb.core.assignment="AiO ≔ ∅ ⦂ ℙ(ACTIVITY×ORG)" org.eventb.core.label="act4" org.eventb.core.source="/Test/m10.bum|org.eventb.core.machineFile#m10|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_S@|org.eventb.core.action#_tdu1cRy0Ee61L_Ef0FP_Qw"/>
<org.eventb.core.scAction name="," org.eventb.core.assignment="UH :∈ UNIT ⇸ UNIT" org.eventb.core.label="act5" org.eventb.core.source="/Test/m10.bum|org.eventb.core.machineFile#m10|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_S@|org.eventb.core.action#_tdu1chy0Ee61L_Ef0FP_Qw"/>
<org.eventb.core.scAction name="-" org.eventb.core.assignment="ViO ≔ ∅ ⦂ ℙ(VIEW×ORG)" org.eventb.core.label="act6" org.eventb.core.source="/Test/m10.bum|org.eventb.core.machineFile#m10|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_S@|org.eventb.core.action#_tdu1cxy0Ee61L_Ef0FP_Qw"/>
<org.eventb.core.scAction name="." org.eventb.core.assignment="RiO ≔ ∅ ⦂ ℙ(ROLE×ORG)" org.eventb.core.label="act7" org.eventb.core.source="/Test/m10.bum|org.eventb.core.machineFile#m10|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_S@|org.eventb.core.action#_tdu1dBy0Ee61L_Ef0FP_Qw"/>
<org.eventb.core.scAction name="/" org.eventb.core.assignment="PCA :∈ PERMISSION ⇸ COR" org.eventb.core.label="act9" org.eventb.core.source="/Test/m10.bum|org.eventb.core.machineFile#m10|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_S@|org.eventb.core.action#_tdu1dhy0Ee61L_Ef0FP_Qw"/>
<org.eventb.core.scAction name="0" org.eventb.core.assignment="PRA ≔ ∅ ⦂ ℙ(PERMISSION×(ROLE×ORG))" org.eventb.core.label="act10" org.eventb.core.source="/Test/m10.bum|org.eventb.core.machineFile#m10|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_S@|org.eventb.core.action#_tdvcgBy0Ee61L_Ef0FP_Qw"/>
<org.eventb.core.scAction name="1" org.eventb.core.assignment="EA ≔ ∅ ⦂ ℙ(EMPLOYEE×UNIT)" org.eventb.core.label="act11" org.eventb.core.source="/Test/m10.bum|org.eventb.core.machineFile#m10|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_S@|org.eventb.core.action#_tdvcgRy0Ee61L_Ef0FP_Qw"/>
<org.eventb.core.scAction name="2" org.eventb.core.assignment="UR ≔ ∅ ⦂ ℙ(UNIT×(ROLE×ORG))" org.eventb.core.label="act12" org.eventb.core.source="/Test/m10.bum|org.eventb.core.machineFile#m10|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_S@|org.eventb.core.action#_tdvcghy0Ee61L_Ef0FP_Qw"/>
<org.eventb.core.scAction name="3" org.eventb.core.assignment="PAA ≔ ∅ ⦂ ℙ(PERMISSION×(ACTIVITY×ORG))" org.eventb.core.label="act13" org.eventb.core.source="/Test/m10.bum|org.eventb.core.machineFile#m10|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_S@|org.eventb.core.action#_tdvcgxy0Ee61L_Ef0FP_Qw"/>
<org.eventb.core.scAction name="4" org.eventb.core.assignment="PVA ≔ ∅ ⦂ ℙ(PERMISSION×(VIEW×ORG))" org.eventb.core.label="act14" org.eventb.core.source="/Test/m10.bum|org.eventb.core.machineFile#m10|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_S@|org.eventb.core.action#_tdvchBy0Ee61L_Ef0FP_Qw"/>
<org.eventb.core.scAction name="5" org.eventb.core.assignment="PCxA ≔ ∅ ⦂ ℙ(PERMISSION×(CONTEXT×ORG))" org.eventb.core.label="act15" org.eventb.core.source="/Test/m10.bum|org.eventb.core.machineFile#m10|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_S@|org.eventb.core.action#_tdvchRy0Ee61L_Ef0FP_Qw"/>
<org.eventb.core.scAction name="6" org.eventb.core.assignment="AV ≔ ∅ ⦂ ℙ(ACTION×(VIEW×ORG))" org.eventb.core.label="act16" org.eventb.core.source="/Test/m10.bum|org.eventb.core.machineFile#m10|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_S@|org.eventb.core.action#_tdwDkBy0Ee61L_Ef0FP_Qw"/>
<org.eventb.core.scAction name="7" org.eventb.core.assignment="AA ≔ ∅ ⦂ ℙ(ACTION×(ACTIVITY×ORG))" org.eventb.core.label="act17" org.eventb.core.source="/Test/m10.bum|org.eventb.core.machineFile#m10|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_S@|org.eventb.core.action#_tdwDkRy0Ee61L_Ef0FP_Qw"/>
<org.eventb.core.scAction name="8" org.eventb.core.assignment="RV ≔ ∅ ⦂ ℙ(RESOURCE×(VIEW×ORG))" org.eventb.core.label="act18" org.eventb.core.source="/Test/m10.bum|org.eventb.core.machineFile#m10|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_S@|org.eventb.core.action#_tdwDkhy0Ee61L_Ef0FP_Qw"/>
<org.eventb.core.scAction name="9" org.eventb.core.assignment="root1 ≔ ∅ ⦂ ℙ(ORG×UNIT)" org.eventb.core.label="act20" org.eventb.core.source="/Test/m10.bum|org.eventb.core.machineFile#m10|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_S@|org.eventb.core.action#_tdwDkhy0Ee61L_Ef0FP_Qx"/>
<org.eventb.core.scAction name=":" org.eventb.core.assignment="OU1 :∈ UNIT ⇸ ORG" org.eventb.core.label="act21" org.eventb.core.source="/Test/m10.bum|org.eventb.core.machineFile#m10|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_S@|org.eventb.core.action#_tdwDkhy0Ee61L_Ef0FP_Qy"/>
<org.eventb.core.scAction name=";" org.eventb.core.assignment="UH1 ≔ ∅ ⦂ ℙ(UNIT×UNIT)" org.eventb.core.label="act22" org.eventb.core.source="/Test/m10.bum|org.eventb.core.machineFile#m10|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_S@|org.eventb.core.action#_tdwDkhy0Ee61L_Ef0FP_Qz"/>
<org.eventb.core.scAction name="=" org.eventb.core.assignment="CA ≔ ∅ ⦂ ℙ(COR×UNIT×ℤ×ℤ)" org.eventb.core.label="act23" org.eventb.core.source="/Test/m10.bum|org.eventb.core.machineFile#m10|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_S@|org.eventb.core.action#_tdwDkhy0Ee61L_Ef0FP_Q{"/>
<org.eventb.core.scAction name=">" org.eventb.core.assignment="UR1 ≔ ∅ ⦂ ℙ(UNIT×(ROLE×ORG))" org.eventb.core.label="act24" org.eventb.core.source="/Test/m10.bum|org.eventb.core.machineFile#m10|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_S@|org.eventb.core.action#_tdwDkhy0Ee61L_Ef0FP_Q\|"/>
<org.eventb.core.scAction name="?" org.eventb.core.assignment="RiO1 ≔ ∅ ⦂ ℙ(ROLE×ORG)" org.eventb.core.label="act25" org.eventb.core.source="/Test/m10.bum|org.eventb.core.machineFile#m10|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_S@|org.eventb.core.action#_tdwDkhy0Ee61L_Ef0FP_Q}"/>
<org.eventb.core.scAction name="@" org.eventb.core.assignment="EA1 ≔ ∅ ⦂ ℙ(EMPLOYEE×UNIT)" org.eventb.core.label="act26" org.eventb.core.source="/Test/m10.bum|org.eventb.core.machineFile#m10|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_S@|org.eventb.core.action#internal1"/>
<org.eventb.core.scAction name="A" org.eventb.core.assignment="CA1 ≔ ∅ ⦂ ℙ(COR×UNIT×ℤ×ℤ)" org.eventb.core.label="act27" org.eventb.core.source="/Test/m10.bum|org.eventb.core.machineFile#m10|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_S@|org.eventb.core.action#internal2"/>
<org.eventb.core.scAction name="B" org.eventb.core.assignment="PRA1 ≔ ∅ ⦂ ℙ(PERMISSION×(ROLE×ORG))" org.eventb.core.label="act28" org.eventb.core.source="/Test/m10.bum|org.eventb.core.machineFile#m10|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_S@|org.eventb.core.action#internal3"/>
<org.eventb.core.scAction name="C" org.eventb.core.assignment="PAA1 ≔ ∅ ⦂ ℙ(PERMISSION×(ACTIVITY×ORG))" org.eventb.core.label="act29" org.eventb.core.source="/Test/m10.bum|org.eventb.core.machineFile#m10|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_S@|org.eventb.core.action#)"/>
<org.eventb.core.scAction name="D" org.eventb.core.assignment="PVA1 ≔ ∅ ⦂ ℙ(PERMISSION×(VIEW×ORG))" org.eventb.core.label="act30" org.eventb.core.source="/Test/m10.bum|org.eventb.core.machineFile#m10|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_S@|org.eventb.core.action#*"/>
<org.eventb.core.scAction name="E" org.eventb.core.assignment="PCA1 ≔ ∅ ⦂ ℙ(PERMISSION×COR)" org.eventb.core.label="act31" org.eventb.core.source="/Test/m10.bum|org.eventb.core.machineFile#m10|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_S@|org.eventb.core.action#+"/>
<org.eventb.core.scAction name="F" org.eventb.core.assignment="PCxA1 ≔ ∅ ⦂ ℙ(PERMISSION×(CONTEXT×ORG))" org.eventb.core.label="act32" org.eventb.core.source="/Test/m10.bum|org.eventb.core.machineFile#m10|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_S@|org.eventb.core.action#,"/>
<org.eventb.core.scAction name="G" org.eventb.core.assignment="ViO1 ≔ ∅ ⦂ ℙ(VIEW×ORG)" org.eventb.core.label="act33" org.eventb.core.source="/Test/m10.bum|org.eventb.core.machineFile#m10|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_S@|org.eventb.core.action#internal4"/>
<org.eventb.core.scAction name="H" org.eventb.core.assignment="RV1 ≔ ∅ ⦂ ℙ(RESOURCE×(VIEW×ORG))" org.eventb.core.label="act34" org.eventb.core.source="/Test/m10.bum|org.eventb.core.machineFile#m10|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_S@|org.eventb.core.action#("/>
<org.eventb.core.scAction name="I" org.eventb.core.assignment="AiO1 ≔ ∅ ⦂ ℙ(ACTIVITY×ORG)" org.eventb.core.label="act35" org.eventb.core.source="/Test/m10.bum|org.eventb.core.machineFile#m10|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_S@|org.eventb.core.action#internal5"/>
<org.eventb.core.scAction name="J" org.eventb.core.assignment="AV1 ≔ ∅ ⦂ ℙ(ACTION×(VIEW×ORG))" org.eventb.core.label="act36" org.eventb.core.source="/Test/m10.bum|org.eventb.core.machineFile#m10|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_S@|org.eventb.core.action#internal6"/>
<org.eventb.core.scAction name="K" org.eventb.core.assignment="AA1 ≔ ∅ ⦂ ℙ(ACTION×(ACTIVITY×ORG))" org.eventb.core.label="act37" org.eventb.core.source="/Test/m10.bum|org.eventb.core.machineFile#m10|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_S@|org.eventb.core.action#internal7"/>
<org.eventb.core.scAction name="L" org.eventb.core.assignment="CiO1 ≔ ∅ ⦂ ℙ(CONTEXT×ORG)" org.eventb.core.label="act38" org.eventb.core.source="/Test/m10.bum|org.eventb.core.machineFile#m10|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_S@|org.eventb.core.action#internal8"/>
<org.eventb.core.scAction name="M" org.eventb.core.assignment="Access_Requested ≔ ∅ ⦂ ℙ(ℤ×EMPLOYEE×ACTION×RESOURCE×ℤ×ℤ×CONTEXT)" org.eventb.core.label="act39" org.eventb.core.source="/Test/m10.bum|org.eventb.core.machineFile#m10|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_S@|org.eventb.core.action#internal9"/>
<org.eventb.core.scAction name="N" org.eventb.core.assignment="PDistA ≔ ∅ ⦂ ℙ(PERMISSION×ℤ)" org.eventb.core.label="act40" org.eventb.core.source="/Test/m10.bum|org.eventb.core.machineFile#m10|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_S@|org.eventb.core.action#internal10"/>
<org.eventb.core.scAction name="O" org.eventb.core.assignment="Request_Treated ≔ ∅ ⦂ ℙ(ℤ×(ℤ×EMPLOYEE×ACTION×RESOURCE×ℤ×ℤ×CONTEXT)×EMPLOYEE×ℤ)" org.eventb.core.label="act41" org.eventb.core.source="/Test/m10.bum|org.eventb.core.machineFile#m10|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_S@|org.eventb.core.action#_tdwDkhy0Ee61L_Ef0FP_Q~"/>
<org.eventb.core.scAction name="P" org.eventb.core.assignment="PAcA ≔ ∅ ⦂ ℙ(PERMISSION×(CONTEXT×ORG))" org.eventb.core.label="act42" org.eventb.core.source="/Test/m10.bum|org.eventb.core.machineFile#m10|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_S@|org.eventb.core.action#_tdwDkhy0Ee61L_Ef0FP_R'"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="Access_Requestef" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="Concrete_Model_Generation" org.eventb.core.source="/Test/m10.bum|org.eventb.core.machineFile#m10|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_SA">
<org.eventb.core.scRefinesEvent name="'" org.eventb.core.scTarget="/Test/m9.bcm|org.eventb.core.scMachineFile#m9|org.eventb.core.scEvent#Access_Requestef" org.eventb.core.source="/Test/m10.bum|org.eventb.core.machineFile#m10|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_SA|org.eventb.core.refinesEvent#'"/>
<org.eventb.core.scAction name="(" org.eventb.core.assignment="CiO ≔ CiO1" org.eventb.core.label="act1" org.eventb.core.source="/Test/m10.bum|org.eventb.core.machineFile#m10|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_SA|org.eventb.core.action#_td1jIBy0Ee61L_Ef0FP_Qw"/>
<org.eventb.core.scAction name=")" org.eventb.core.assignment="AiO ≔ AiO1" org.eventb.core.label="act4" org.eventb.core.source="/Test/m10.bum|org.eventb.core.machineFile#m10|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_SA|org.eventb.core.action#__StoEBy2Ee61L_Ef0FP_Qw"/>
<org.eventb.core.scAction name="*" org.eventb.core.assignment="ViO ≔ ViO1" org.eventb.core.label="act6" org.eventb.core.source="/Test/m10.bum|org.eventb.core.machineFile#m10|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_SA|org.eventb.core.action#_D2pGQBy3Ee61L_Ef0FP_Qw"/>
<org.eventb.core.scAction name="+" org.eventb.core.assignment="AV ≔ AV1" org.eventb.core.label="act16" org.eventb.core.source="/Test/m10.bum|org.eventb.core.machineFile#m10|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_SA|org.eventb.core.action#_td1jIhy0Ee61L_Ef0FP_R9"/>
<org.eventb.core.scAction name="," org.eventb.core.assignment="AA ≔ AA1" org.eventb.core.label="act17" org.eventb.core.source="/Test/m10.bum|org.eventb.core.machineFile#m10|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_SA|org.eventb.core.action#_td1jIhy0Ee61L_Ef0FP_R:"/>
<org.eventb.core.scAction name="-" org.eventb.core.assignment="RV ≔ RV1" org.eventb.core.label="act18" org.eventb.core.source="/Test/m10.bum|org.eventb.core.machineFile#m10|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_SA|org.eventb.core.action#_td1jIhy0Ee61L_Ef0FP_R;"/>
<org.eventb.core.scAction name="." org.eventb.core.assignment="root ≔ root1" org.eventb.core.label="act2" org.eventb.core.source="/Test/m10.bum|org.eventb.core.machineFile#m10|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_SA|org.eventb.core.action#_td1jIRy0Ee61L_Ef0FP_Qw"/>
<org.eventb.core.scAction name="/" org.eventb.core.assignment="UH ≔ UH1" org.eventb.core.label="act5" org.eventb.core.source="/Test/m10.bum|org.eventb.core.machineFile#m10|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_SA|org.eventb.core.action#_BFqMYBy3Ee61L_Ef0FP_Qw"/>
<org.eventb.core.scAction name="0" org.eventb.core.assignment="OU ≔ OU1" org.eventb.core.label="act3" org.eventb.core.source="/Test/m10.bum|org.eventb.core.machineFile#m10|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_SA|org.eventb.core.action#_td1jIhy0Ee61L_Ef0FP_Qw"/>
<org.eventb.core.scAction name="1" org.eventb.core.assignment="RiO ≔ RiO1" org.eventb.core.label="act7" org.eventb.core.source="/Test/m10.bum|org.eventb.core.machineFile#m10|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_SA|org.eventb.core.action#_aKm3kBy3Ee61L_Ef0FP_Qw"/>
<org.eventb.core.scAction name="2" org.eventb.core.assignment="UR ≔ UR1" org.eventb.core.label="act12" org.eventb.core.source="/Test/m10.bum|org.eventb.core.machineFile#m10|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_SA|org.eventb.core.action#_td1jIhy0Ee61L_Ef0FP_R,"/>
<org.eventb.core.scAction name="3" org.eventb.core.assignment="EA ≔ EA1" org.eventb.core.label="act11" org.eventb.core.source="/Test/m10.bum|org.eventb.core.machineFile#m10|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_SA|org.eventb.core.action#_td1jIhy0Ee61L_Ef0FP_R+"/>
<org.eventb.core.scAction name="4" org.eventb.core.assignment="PCA ≔ PCA1" org.eventb.core.label="act9" org.eventb.core.source="/Test/m10.bum|org.eventb.core.machineFile#m10|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_SA|org.eventb.core.action#_td1jIhy0Ee61L_Ef0FP_Q~"/>
<org.eventb.core.scAction name="5" org.eventb.core.assignment="PRA ≔ PRA1" org.eventb.core.label="act10" org.eventb.core.source="/Test/m10.bum|org.eventb.core.machineFile#m10|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_SA|org.eventb.core.action#_td1jIhy0Ee61L_Ef0FP_R'"/>
<org.eventb.core.scAction name="6" org.eventb.core.assignment="PAA ≔ PAA1" org.eventb.core.label="act13" org.eventb.core.source="/Test/m10.bum|org.eventb.core.machineFile#m10|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_SA|org.eventb.core.action#_td1jIhy0Ee61L_Ef0FP_R-"/>
<org.eventb.core.scAction name="7" org.eventb.core.assignment="PVA ≔ PVA1" org.eventb.core.label="act14" org.eventb.core.source="/Test/m10.bum|org.eventb.core.machineFile#m10|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_SA|org.eventb.core.action#_td1jIhy0Ee61L_Ef0FP_R1"/>
<org.eventb.core.scAction name="8" org.eventb.core.assignment="PCxA ≔ PCxA1" org.eventb.core.label="act15" org.eventb.core.source="/Test/m10.bum|org.eventb.core.machineFile#m10|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_SA|org.eventb.core.action#_td1jIhy0Ee61L_Ef0FP_R5"/>
<org.eventb.core.scAction name="9" org.eventb.core.assignment="CA ≔ CA1" org.eventb.core.label="act19" org.eventb.core.source="/Test/m10.bum|org.eventb.core.machineFile#m10|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_SA|org.eventb.core.action#_PSi28By5Ee61L_Ef0FP_Qw"/>
<org.eventb.core.scAction name=":" org.eventb.core.assignment="PAcA :∈ PERMISSION ⇸ CiO" org.eventb.core.label="act20" org.eventb.core.source="/Test/m10.bum|org.eventb.core.machineFile#m10|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_SA|org.eventb.core.action#("/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="Access_Requesteg" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="Assign_Oragnization_Root" org.eventb.core.source="/Test/m10.bum|org.eventb.core.machineFile#m10|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_SB">
<org.eventb.core.scRefinesEvent name="'" org.eventb.core.scTarget="/Test/m9.bcm|org.eventb.core.scMachineFile#m9|org.eventb.core.scEvent#Access_Requesteg" org.eventb.core.source="/Test/m10.bum|org.eventb.core.machineFile#m10|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_SB|org.eventb.core.refinesEvent#'"/>
<org.eventb.core.scGuard name="'" org.eventb.core.label="grd1" org.eventb.core.predicate="org∈ORG∧u∈UNIT" org.eventb.core.source="/Test/m1.bum|org.eventb.core.machineFile#m1|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_Qz|org.eventb.core.guard#)" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="(" org.eventb.core.label="grd2" org.eventb.core.predicate="org∉dom(root1)" org.eventb.core.source="/Test/m1.bum|org.eventb.core.machineFile#m1|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_Qz|org.eventb.core.guard#-" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name=")" org.eventb.core.label="grd3" org.eventb.core.predicate="u∉dom(UH1)" org.eventb.core.source="/Test/m1.bum|org.eventb.core.machineFile#m1|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_Qz|org.eventb.core.guard#." org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="*" org.eventb.core.label="grd4" org.eventb.core.predicate="ran(root1∪{org ↦ u})∩dom(UH1)=(∅ ⦂ ℙ(UNIT))" org.eventb.core.source="/Test/m1.bum|org.eventb.core.machineFile#m1|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_Qz|org.eventb.core.guard#\/" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="+" org.eventb.core.label="grd5" org.eventb.core.predicate="u ↦ org∈OU1" org.eventb.core.source="/Test/m1.bum|org.eventb.core.machineFile#m1|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_Qz|org.eventb.core.guard#0" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="," org.eventb.core.label="grd6" org.eventb.core.predicate="u∉ran(root1)" org.eventb.core.source="/Test/m1.bum|org.eventb.core.machineFile#m1|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_Qz|org.eventb.core.guard#1" org.eventb.core.theorem="false"/>
<org.eventb.core.scAction name="orh" org.eventb.core.assignment="root1 ≔ root1∪{org ↦ u}" org.eventb.core.label="act1" org.eventb.core.source="/Test/m1.bum|org.eventb.core.machineFile#m1|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_Qz|org.eventb.core.action#*"/>
<org.eventb.core.scParameter name="org" org.eventb.core.source="/Test/m1.bum|org.eventb.core.machineFile#m1|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_Qz|org.eventb.core.parameter#(" org.eventb.core.type="ORG"/>
<org.eventb.core.scParameter name="u" org.eventb.core.source="/Test/m1.bum|org.eventb.core.machineFile#m1|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_Qz|org.eventb.core.parameter#'" org.eventb.core.type="UNIT"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="Access_Requesteh" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="Add_Unit_Hierarchy" org.eventb.core.source="/Test/m10.bum|org.eventb.core.machineFile#m10|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_SC">
<org.eventb.core.scRefinesEvent name="'" org.eventb.core.scTarget="/Test/m9.bcm|org.eventb.core.scMachineFile#m9|org.eventb.core.scEvent#Access_Requesteh" org.eventb.core.source="/Test/m10.bum|org.eventb.core.machineFile#m10|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_SC|org.eventb.core.refinesEvent#'"/>
<org.eventb.core.scGuard name="(" org.eventb.core.label="grd1" org.eventb.core.predicate="u1∈UNIT∧u2∈UNIT" org.eventb.core.source="/Test/m3.bum|org.eventb.core.machineFile#m3|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_R>|org.eventb.core.guard#)" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name=")" org.eventb.core.label="grd3" org.eventb.core.predicate="u1∉dom(UH1)" org.eventb.core.source="/Test/m3.bum|org.eventb.core.machineFile#m3|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_R>|org.eventb.core.guard#," org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="*" org.eventb.core.label="grd7" org.eventb.core.predicate="u1 ↦ u2∉UH1" org.eventb.core.source="/Test/m3.bum|org.eventb.core.machineFile#m3|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_R>|org.eventb.core.guard#0" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="+" org.eventb.core.label="grd4" org.eventb.core.predicate="u1≠u2" org.eventb.core.source="/Test/m3.bum|org.eventb.core.machineFile#m3|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_R>|org.eventb.core.guard#-" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="," org.eventb.core.label="grd5" org.eventb.core.predicate="u2 ↦ u1∉UH1" org.eventb.core.source="/Test/m3.bum|org.eventb.core.machineFile#m3|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_R>|org.eventb.core.guard#." org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="-" org.eventb.core.label="grd6" org.eventb.core.predicate="u1∉ran(root1)" org.eventb.core.source="/Test/m3.bum|org.eventb.core.machineFile#m3|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_R>|org.eventb.core.guard#\/" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="." org.eventb.core.label="grd8" org.eventb.core.predicate="OU1[{u1}]=OU1[{u2}]" org.eventb.core.source="/Test/m3.bum|org.eventb.core.machineFile#m3|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_R>|org.eventb.core.guard#1" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="/" org.eventb.core.label="grd9" org.eventb.core.predicate="∀e⦂EMPLOYEE·e ↦ u1∈EA1⇒e ↦ u2∉EA1" org.eventb.core.source="/Test/m3.bum|org.eventb.core.machineFile#m3|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_R>|org.eventb.core.guard#2" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="0" org.eventb.core.label="grd10" org.eventb.core.predicate="∀e⦂EMPLOYEE·e ↦ u2∈EA1⇒e ↦ u1∉EA1" org.eventb.core.source="/Test/m3.bum|org.eventb.core.machineFile#m3|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_R>|org.eventb.core.guard#3" org.eventb.core.theorem="false"/>
<org.eventb.core.scAction name="u3" org.eventb.core.assignment="UH1 ≔ UH1∪{u1 ↦ u2}" org.eventb.core.label="act1" org.eventb.core.source="/Test/m3.bum|org.eventb.core.machineFile#m3|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_R>|org.eventb.core.action#+"/>
<org.eventb.core.scParameter name="u1" org.eventb.core.source="/Test/m3.bum|org.eventb.core.machineFile#m3|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_R>|org.eventb.core.parameter#'" org.eventb.core.type="UNIT"/>
<org.eventb.core.scParameter name="u2" org.eventb.core.source="/Test/m3.bum|org.eventb.core.machineFile#m3|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_R>|org.eventb.core.parameter#(" org.eventb.core.type="UNIT"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="Access_Requestei" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="Assign_Unit_to_Org" org.eventb.core.source="/Test/m10.bum|org.eventb.core.machineFile#m10|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_SD">
<org.eventb.core.scRefinesEvent name="'" org.eventb.core.scTarget="/Test/m9.bcm|org.eventb.core.scMachineFile#m9|org.eventb.core.scEvent#Access_Requestei" org.eventb.core.source="/Test/m10.bum|org.eventb.core.machineFile#m10|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_SD|org.eventb.core.refinesEvent#'"/>
<org.eventb.core.scGuard name="(" org.eventb.core.label="grd1" org.eventb.core.predicate="u ↦ org∉OU1" org.eventb.core.source="/Test/m2.bum|org.eventb.core.machineFile#m2|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_R3|org.eventb.core.guard#)" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name=")" org.eventb.core.label="grd2" org.eventb.core.predicate="u∉dom(OU1)" org.eventb.core.source="/Test/m2.bum|org.eventb.core.machineFile#m2|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_R3|org.eventb.core.guard#+" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="*" org.eventb.core.label="grd3" org.eventb.core.predicate="∀org1⦂ORG,role⦂ROLE·u ↦ (role ↦ org1)∈UR1⇒org=org1" org.eventb.core.source="/Test/m2.bum|org.eventb.core.machineFile#m2|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_R3|org.eventb.core.guard#," org.eventb.core.theorem="false"/>
<org.eventb.core.scAction name="orh" org.eventb.core.assignment="OU1 ≔ OU1∪{u ↦ org}" org.eventb.core.label="act1" org.eventb.core.source="/Test/m2.bum|org.eventb.core.machineFile#m2|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_R3|org.eventb.core.action#*"/>
<org.eventb.core.scParameter name="org" org.eventb.core.source="/Test/m2.bum|org.eventb.core.machineFile#m2|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_R3|org.eventb.core.parameter#(" org.eventb.core.type="ORG"/>
<org.eventb.core.scParameter name="u" org.eventb.core.source="/Test/m2.bum|org.eventb.core.machineFile#m2|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_R3|org.eventb.core.parameter#'" org.eventb.core.type="UNIT"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="Access_Requestej" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="Assign_Role_to_Unit" org.eventb.core.source="/Test/m10.bum|org.eventb.core.machineFile#m10|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_SE">
<org.eventb.core.scRefinesEvent name="'" org.eventb.core.scTarget="/Test/m9.bcm|org.eventb.core.scMachineFile#m9|org.eventb.core.scEvent#Access_Requestej" org.eventb.core.source="/Test/m10.bum|org.eventb.core.machineFile#m10|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_SE|org.eventb.core.refinesEvent#'"/>
<org.eventb.core.scGuard name="'" org.eventb.core.label="grd1" org.eventb.core.predicate="r∈RiO1∧u∈UNIT∧u ↦ r∉UR1" org.eventb.core.source="/Test/m2.bum|org.eventb.core.machineFile#m2|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_R4|org.eventb.core.guard#*" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="(" org.eventb.core.label="grd2" org.eventb.core.predicate="∀role⦂ROLE,org⦂ORG·r=role ↦ org⇒(OU1[{u}]≠(∅ ⦂ ℙ(ORG))⇒OU1(u)=org)" org.eventb.core.source="/Test/m2.bum|org.eventb.core.machineFile#m2|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_R4|org.eventb.core.guard#." org.eventb.core.theorem="false"/>
<org.eventb.core.scAction name="v" org.eventb.core.assignment="UR1 ≔ UR1∪{u ↦ r}" org.eventb.core.label="act1" org.eventb.core.source="/Test/m2.bum|org.eventb.core.machineFile#m2|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_R4|org.eventb.core.action#)"/>
<org.eventb.core.scParameter name="r" org.eventb.core.source="/Test/m2.bum|org.eventb.core.machineFile#m2|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_R4|org.eventb.core.parameter#'" org.eventb.core.type="ROLE×ORG"/>
<org.eventb.core.scParameter name="u" org.eventb.core.source="/Test/m2.bum|org.eventb.core.machineFile#m2|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_R4|org.eventb.core.parameter#(" org.eventb.core.type="UNIT"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="Access_Requestek" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="Assign_Role_to_Organization" org.eventb.core.source="/Test/m10.bum|org.eventb.core.machineFile#m10|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_SF">
<org.eventb.core.scRefinesEvent name="'" org.eventb.core.scTarget="/Test/m9.bcm|org.eventb.core.scMachineFile#m9|org.eventb.core.scEvent#Access_Requestek" org.eventb.core.source="/Test/m10.bum|org.eventb.core.machineFile#m10|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_SF|org.eventb.core.refinesEvent#'"/>
<org.eventb.core.scGuard name="'" org.eventb.core.label="grd1" org.eventb.core.predicate="r∈ROLE∧org∈ORG" org.eventb.core.source="/Test/m2.bum|org.eventb.core.machineFile#m2|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_R8|org.eventb.core.guard#)" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="(" org.eventb.core.label="grd2" org.eventb.core.predicate="r ↦ org∉RiO1" org.eventb.core.source="/Test/m2.bum|org.eventb.core.machineFile#m2|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_R8|org.eventb.core.guard#+" org.eventb.core.theorem="false"/>
<org.eventb.core.scAction name="orh" org.eventb.core.assignment="RiO1 ≔ RiO1∪{r ↦ org}" org.eventb.core.label="act1" org.eventb.core.source="/Test/m2.bum|org.eventb.core.machineFile#m2|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_R8|org.eventb.core.action#*"/>
<org.eventb.core.scParameter name="org" org.eventb.core.source="/Test/m2.bum|org.eventb.core.machineFile#m2|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_R8|org.eventb.core.parameter#(" org.eventb.core.type="ORG"/>
<org.eventb.core.scParameter name="r" org.eventb.core.source="/Test/m2.bum|org.eventb.core.machineFile#m2|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_R8|org.eventb.core.parameter#'" org.eventb.core.type="ROLE"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="Access_Requestel" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="Assign_Employee−to_Unit" org.eventb.core.source="/Test/m10.bum|org.eventb.core.machineFile#m10|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_SG">
<org.eventb.core.scRefinesEvent name="'" org.eventb.core.scTarget="/Test/m9.bcm|org.eventb.core.scMachineFile#m9|org.eventb.core.scEvent#Access_Requestel" org.eventb.core.source="/Test/m10.bum|org.eventb.core.machineFile#m10|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_SG|org.eventb.core.refinesEvent#'"/>
<org.eventb.core.scGuard name="'" org.eventb.core.label="grd1" org.eventb.core.predicate="e ↦ u∉EA1" org.eventb.core.source="/Test/m3.bum|org.eventb.core.machineFile#m3|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_RB|org.eventb.core.guard#)" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="(" org.eventb.core.label="grd2" org.eventb.core.predicate="∀u1⦂UNIT·e ↦ u1∈EA1⇒u ↦ u1∉UH1∧u1 ↦ u∉UH1" org.eventb.core.source="/Test/m3.bum|org.eventb.core.machineFile#m3|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_RB|org.eventb.core.guard#+" org.eventb.core.theorem="false"/>
<org.eventb.core.scAction name="v" org.eventb.core.assignment="EA1 ≔ EA1∪{e ↦ u}" org.eventb.core.label="act1" org.eventb.core.source="/Test/m3.bum|org.eventb.core.machineFile#m3|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_RB|org.eventb.core.action#*"/>
<org.eventb.core.scParameter name="e" org.eventb.core.source="/Test/m3.bum|org.eventb.core.machineFile#m3|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_RB|org.eventb.core.parameter#'" org.eventb.core.type="EMPLOYEE"/>
<org.eventb.core.scParameter name="u" org.eventb.core.source="/Test/m3.bum|org.eventb.core.machineFile#m3|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_RB|org.eventb.core.parameter#(" org.eventb.core.type="UNIT"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="Access_Requestem" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="Assign_Approver" org.eventb.core.source="/Test/m10.bum|org.eventb.core.machineFile#m10|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_SH">
<org.eventb.core.scRefinesEvent name="'" org.eventb.core.scTarget="/Test/m9.bcm|org.eventb.core.scMachineFile#m9|org.eventb.core.scEvent#Access_Requestem" org.eventb.core.source="/Test/m10.bum|org.eventb.core.machineFile#m10|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_SH|org.eventb.core.refinesEvent#'"/>
<org.eventb.core.scGuard name="'" org.eventb.core.label="grd2" org.eventb.core.predicate="cor ↦ u ↦ p ↦ d∉CA1" org.eventb.core.source="/Test/m4.bum|org.eventb.core.machineFile#m4|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_RL|org.eventb.core.guard#*" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="(" org.eventb.core.label="grd5" org.eventb.core.predicate="∀u1⦂UNIT,p1⦂ℤ,d1⦂ℤ·cor ↦ u1 ↦ p1 ↦ d1∈CA1⇒u1≠u∧(u1 ↦ u∈UH1∨(∃u2⦂UNIT,p2⦂ℤ,d2⦂ℤ·cor ↦ u2 ↦ p2 ↦ d2∈CA1∧u2 ↦ u∈UH1))" org.eventb.core.source="/Test/m4.bum|org.eventb.core.machineFile#m4|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_RL|org.eventb.core.guard#0" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name=")" org.eventb.core.label="grd4" org.eventb.core.predicate="u ↦ p ↦ d∈APPROVER" org.eventb.core.source="/Test/m4.bum|org.eventb.core.machineFile#m4|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_RL|org.eventb.core.guard#\/" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="*" org.eventb.core.label="grd3" org.eventb.core.predicate="∀u2⦂UNIT,p2⦂ℤ,d2⦂ℤ·cor ↦ u2 ↦ p2 ↦ d2∈CA1∧u≠u2⇒(OU1[{u}]≠(∅ ⦂ ℙ(ORG))∧OU1[{u2}]≠(∅ ⦂ ℙ(ORG))⇒OU1(u)=OU1(u2))" org.eventb.core.source="/Test/m4.bum|org.eventb.core.machineFile#m4|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_RL|org.eventb.core.guard#," org.eventb.core.theorem="false"/>
<org.eventb.core.scAction name="cos" org.eventb.core.assignment="CA1 ≔ CA1∪{cor ↦ u ↦ p ↦ d}" org.eventb.core.label="act1" org.eventb.core.source="/Test/m4.bum|org.eventb.core.machineFile#m4|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_RL|org.eventb.core.action#+"/>
<org.eventb.core.scParameter name="d" org.eventb.core.source="/Test/m4.bum|org.eventb.core.machineFile#m4|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_RL|org.eventb.core.parameter#-" org.eventb.core.type="ℤ"/>
<org.eventb.core.scParameter name="cor" org.eventb.core.source="/Test/m4.bum|org.eventb.core.machineFile#m4|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_RL|org.eventb.core.parameter#(" org.eventb.core.type="COR"/>
<org.eventb.core.scParameter name="p" org.eventb.core.source="/Test/m4.bum|org.eventb.core.machineFile#m4|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_RL|org.eventb.core.parameter#'" org.eventb.core.type="ℤ"/>
<org.eventb.core.scParameter name="u" org.eventb.core.source="/Test/m4.bum|org.eventb.core.machineFile#m4|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_RL|org.eventb.core.parameter#." org.eventb.core.type="UNIT"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="Access_Requesten" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="Define_Security_Rule" org.eventb.core.source="/Test/m10.bum|org.eventb.core.machineFile#m10|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_SI">
<org.eventb.core.scRefinesEvent name="'" org.eventb.core.scTarget="/Test/m9.bcm|org.eventb.core.scMachineFile#m9|org.eventb.core.scEvent#Access_Requesten" org.eventb.core.source="/Test/m10.bum|org.eventb.core.machineFile#m10|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_SI|org.eventb.core.refinesEvent#'"/>
<org.eventb.core.scGuard name="'" org.eventb.core.label="grd1" org.eventb.core.predicate="rio∈RiO1∧aio∈AiO∧vio∈ViO∧cio∈CiO∧cor∈COR∧perm∈PERMISSION" org.eventb.core.source="/Test/m4.bum|org.eventb.core.machineFile#m4|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_RP|org.eventb.core.guard#," org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="(" org.eventb.core.label="grd2" org.eventb.core.predicate="∀a⦂ACTIVITY,v⦂VIEW,c⦂CONTEXT,org1⦂ORG,org2⦂ORG,org3⦂ORG·aio=a ↦ org1∧vio=v ↦ org2∧cio=c ↦ org3⇒org1=org2∧org2=org3" org.eventb.core.source="/Test/m4.bum|org.eventb.core.machineFile#m4|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_RP|org.eventb.core.guard#3" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name=")" org.eventb.core.label="grd3" org.eventb.core.predicate="perm∉dom(PRA1)∧perm∉dom(PAA1)∧perm∉dom(PVA1)∧perm∉dom(PCA1)∧perm∉dom(PCxA1)" org.eventb.core.source="/Test/m4.bum|org.eventb.core.machineFile#m4|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_RP|org.eventb.core.guard#4" org.eventb.core.theorem="false"/>
<org.eventb.core.scAction name="pern" org.eventb.core.assignment="PRA1 ≔ PRA1∪{perm ↦ rio}" org.eventb.core.label="act1" org.eventb.core.source="/Test/m4.bum|org.eventb.core.machineFile#m4|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_RP|org.eventb.core.action#."/>
<org.eventb.core.scAction name="pero" org.eventb.core.assignment="PAA1 ≔ PAA1∪{perm ↦ aio}" org.eventb.core.label="act2" org.eventb.core.source="/Test/m4.bum|org.eventb.core.machineFile#m4|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_RP|org.eventb.core.action#\/"/>
<org.eventb.core.scAction name="perp" org.eventb.core.assignment="PVA1 ≔ PVA1∪{perm ↦ vio}" org.eventb.core.label="act3" org.eventb.core.source="/Test/m4.bum|org.eventb.core.machineFile#m4|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_RP|org.eventb.core.action#0"/>
<org.eventb.core.scAction name="perq" org.eventb.core.assignment="PCA1 ≔ PCA1∪{perm ↦ cor}" org.eventb.core.label="act4" org.eventb.core.source="/Test/m4.bum|org.eventb.core.machineFile#m4|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_RP|org.eventb.core.action#1"/>
<org.eventb.core.scAction name="perr" org.eventb.core.assignment="PCxA1 ≔ PCxA1∪{perm ↦ cio}" org.eventb.core.label="act5" org.eventb.core.source="/Test/m4.bum|org.eventb.core.machineFile#m4|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_RP|org.eventb.core.action#2"/>
<org.eventb.core.scParameter name="perm" org.eventb.core.source="/Test/m4.bum|org.eventb.core.machineFile#m4|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_RP|org.eventb.core.parameter#+" org.eventb.core.type="PERMISSION"/>
<org.eventb.core.scParameter name="aio" org.eventb.core.source="/Test/m4.bum|org.eventb.core.machineFile#m4|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_RP|org.eventb.core.parameter#(" org.eventb.core.type="ACTIVITY×ORG"/>
<org.eventb.core.scParameter name="cor" org.eventb.core.source="/Test/m4.bum|org.eventb.core.machineFile#m4|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_RP|org.eventb.core.parameter#*" org.eventb.core.type="COR"/>
<org.eventb.core.scParameter name="cio" org.eventb.core.source="/Test/m4.bum|org.eventb.core.machineFile#m4|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_RP|org.eventb.core.parameter#-" org.eventb.core.type="CONTEXT×ORG"/>
<org.eventb.core.scParameter name="rio" org.eventb.core.source="/Test/m4.bum|org.eventb.core.machineFile#m4|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_RP|org.eventb.core.parameter#'" org.eventb.core.type="ROLE×ORG"/>
<org.eventb.core.scParameter name="vio" org.eventb.core.source="/Test/m4.bum|org.eventb.core.machineFile#m4|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_RP|org.eventb.core.parameter#)" org.eventb.core.type="VIEW×ORG"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="Access_Requesteo" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="Assign_Resource_to_View" org.eventb.core.source="/Test/m10.bum|org.eventb.core.machineFile#m10|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_SJ">
<org.eventb.core.scRefinesEvent name="'" org.eventb.core.scTarget="/Test/m9.bcm|org.eventb.core.scMachineFile#m9|org.eventb.core.scEvent#Access_Requesteo" org.eventb.core.source="/Test/m10.bum|org.eventb.core.machineFile#m10|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_SJ|org.eventb.core.refinesEvent#'"/>
<org.eventb.core.scGuard name="'" org.eventb.core.label="grd1" org.eventb.core.predicate="r∈RESOURCE∧vio∈ViO1" org.eventb.core.source="/Test/m5.bum|org.eventb.core.machineFile#m5|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_R`|org.eventb.core.guard#)" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="(" org.eventb.core.label="grd2" org.eventb.core.predicate="r ↦ vio∉RV1" org.eventb.core.source="/Test/m5.bum|org.eventb.core.machineFile#m5|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_R`|org.eventb.core.guard#*" org.eventb.core.theorem="false"/>
<org.eventb.core.scAction name="vip" org.eventb.core.assignment="RV1 ≔ RV1∪{r ↦ vio}" org.eventb.core.label="act1" org.eventb.core.source="/Test/m5.bum|org.eventb.core.machineFile#m5|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_R`|org.eventb.core.action#+"/>
<org.eventb.core.scParameter name="r" org.eventb.core.source="/Test/m5.bum|org.eventb.core.machineFile#m5|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_R`|org.eventb.core.parameter#'" org.eventb.core.type="RESOURCE"/>
<org.eventb.core.scParameter name="vio" org.eventb.core.source="/Test/m5.bum|org.eventb.core.machineFile#m5|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_R`|org.eventb.core.parameter#(" org.eventb.core.type="VIEW×ORG"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="Access_Requestep" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="Assign_View_to_Organization" org.eventb.core.source="/Test/m10.bum|org.eventb.core.machineFile#m10|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_SK">
<org.eventb.core.scRefinesEvent name="'" org.eventb.core.scTarget="/Test/m9.bcm|org.eventb.core.scMachineFile#m9|org.eventb.core.scEvent#Access_Requestep" org.eventb.core.source="/Test/m10.bum|org.eventb.core.machineFile#m10|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_SK|org.eventb.core.refinesEvent#'"/>
<org.eventb.core.scGuard name="(" org.eventb.core.label="grd1" org.eventb.core.predicate="v∈VIEW∧org∈ORG" org.eventb.core.source="/Test/m6.bum|org.eventb.core.machineFile#m6|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_Rp|org.eventb.core.guard#)" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name=")" org.eventb.core.label="grd2" org.eventb.core.predicate="v ↦ org∉ViO1" org.eventb.core.source="/Test/m6.bum|org.eventb.core.machineFile#m6|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_Rp|org.eventb.core.guard#*" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="*" org.eventb.core.label="grd3" org.eventb.core.predicate="v ↦ org∉ran(RV1)" org.eventb.core.source="/Test/m6.bum|org.eventb.core.machineFile#m6|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_Rp|org.eventb.core.guard#," org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="+" org.eventb.core.label="grd4" org.eventb.core.predicate="v ↦ org∉ran(AV1)" org.eventb.core.source="/Test/m6.bum|org.eventb.core.machineFile#m6|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_Rp|org.eventb.core.guard#-" org.eventb.core.theorem="false"/>
<org.eventb.core.scAction name="orh" org.eventb.core.assignment="ViO1 ≔ ViO1∪{v ↦ org}" org.eventb.core.label="act1" org.eventb.core.source="/Test/m6.bum|org.eventb.core.machineFile#m6|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_Rp|org.eventb.core.action#+"/>
<org.eventb.core.scParameter name="org" org.eventb.core.source="/Test/m6.bum|org.eventb.core.machineFile#m6|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_Rp|org.eventb.core.parameter#(" org.eventb.core.type="ORG"/>
<org.eventb.core.scParameter name="v" org.eventb.core.source="/Test/m6.bum|org.eventb.core.machineFile#m6|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_Rp|org.eventb.core.parameter#'" org.eventb.core.type="VIEW"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="Access_Requesteq" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="Assign_activity_to_Organization" org.eventb.core.source="/Test/m10.bum|org.eventb.core.machineFile#m10|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_SL">
<org.eventb.core.scRefinesEvent name="'" org.eventb.core.scTarget="/Test/m9.bcm|org.eventb.core.scMachineFile#m9|org.eventb.core.scEvent#Access_Requesteq" org.eventb.core.source="/Test/m10.bum|org.eventb.core.machineFile#m10|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_SL|org.eventb.core.refinesEvent#'"/>
<org.eventb.core.scGuard name="'" org.eventb.core.label="grd1" org.eventb.core.predicate="a∈ACTIVITY∧org∈ORG" org.eventb.core.source="/Test/m6.bum|org.eventb.core.machineFile#m6|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_Rq|org.eventb.core.guard#)" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="(" org.eventb.core.label="grd2" org.eventb.core.predicate="a ↦ org∉AiO1" org.eventb.core.source="/Test/m6.bum|org.eventb.core.machineFile#m6|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_Rq|org.eventb.core.guard#*" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name=")" org.eventb.core.label="grd3" org.eventb.core.predicate="a ↦ org∉ran(AA1)" org.eventb.core.source="/Test/m6.bum|org.eventb.core.machineFile#m6|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_Rq|org.eventb.core.guard#," org.eventb.core.theorem="false"/>
<org.eventb.core.scAction name="orh" org.eventb.core.assignment="AiO1 ≔ AiO1∪{a ↦ org}" org.eventb.core.label="act1" org.eventb.core.source="/Test/m6.bum|org.eventb.core.machineFile#m6|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_Rq|org.eventb.core.action#+"/>
<org.eventb.core.scParameter name="a" org.eventb.core.source="/Test/m6.bum|org.eventb.core.machineFile#m6|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_Rq|org.eventb.core.parameter#'" org.eventb.core.type="ACTIVITY"/>
<org.eventb.core.scParameter name="org" org.eventb.core.source="/Test/m6.bum|org.eventb.core.machineFile#m6|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_Rq|org.eventb.core.parameter#(" org.eventb.core.type="ORG"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="Access_Requester" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="Assign_Action_to_Activity" org.eventb.core.source="/Test/m10.bum|org.eventb.core.machineFile#m10|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_SM">
<org.eventb.core.scRefinesEvent name="'" org.eventb.core.scTarget="/Test/m9.bcm|org.eventb.core.scMachineFile#m9|org.eventb.core.scEvent#Access_Requester" org.eventb.core.source="/Test/m10.bum|org.eventb.core.machineFile#m10|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_SM|org.eventb.core.refinesEvent#'"/>
<org.eventb.core.scGuard name="'" org.eventb.core.label="grd1" org.eventb.core.predicate="a∈ACTION∧aio∈AiO1∧vio∈ViO1" org.eventb.core.source="/Test/m6.bum|org.eventb.core.machineFile#m6|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_Rr|org.eventb.core.guard#," org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="(" org.eventb.core.label="grd2" org.eventb.core.predicate="a ↦ aio∉AA1∧a ↦ vio∉AV1" org.eventb.core.source="/Test/m6.bum|org.eventb.core.machineFile#m6|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_Rr|org.eventb.core.guard#-" org.eventb.core.theorem="false"/>
<org.eventb.core.scAction name="vip" org.eventb.core.assignment="AA1 ≔ AA1∪{a ↦ aio}" org.eventb.core.label="act1" org.eventb.core.source="/Test/m6.bum|org.eventb.core.machineFile#m6|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_Rr|org.eventb.core.action#*"/>
<org.eventb.core.scAction name="viq" org.eventb.core.assignment="AV1 ≔ AV1∪{a ↦ vio}" org.eventb.core.label="act2" org.eventb.core.source="/Test/m6.bum|org.eventb.core.machineFile#m6|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_Rr|org.eventb.core.action#+"/>
<org.eventb.core.scParameter name="a" org.eventb.core.source="/Test/m6.bum|org.eventb.core.machineFile#m6|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_Rr|org.eventb.core.parameter#'" org.eventb.core.type="ACTION"/>
<org.eventb.core.scParameter name="aio" org.eventb.core.source="/Test/m6.bum|org.eventb.core.machineFile#m6|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_Rr|org.eventb.core.parameter#(" org.eventb.core.type="ACTIVITY×ORG"/>
<org.eventb.core.scParameter name="vio" org.eventb.core.source="/Test/m6.bum|org.eventb.core.machineFile#m6|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_Rr|org.eventb.core.parameter#)" org.eventb.core.type="VIEW×ORG"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="Access_Requestes" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="Assign_Context_to_Organization" org.eventb.core.source="/Test/m10.bum|org.eventb.core.machineFile#m10|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_SN">
<org.eventb.core.scRefinesEvent name="'" org.eventb.core.scTarget="/Test/m9.bcm|org.eventb.core.scMachineFile#m9|org.eventb.core.scEvent#Access_Requestes" org.eventb.core.source="/Test/m10.bum|org.eventb.core.machineFile#m10|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_SN|org.eventb.core.refinesEvent#'"/>
<org.eventb.core.scGuard name="'" org.eventb.core.label="grd1" org.eventb.core.predicate="org∈ORG∧c∈CONTEXT" org.eventb.core.source="/Test/m7.bum|org.eventb.core.machineFile#m7|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_S,|org.eventb.core.guard#)" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="(" org.eventb.core.label="grd2" org.eventb.core.predicate="c ↦ org∉CiO1" org.eventb.core.source="/Test/m7.bum|org.eventb.core.machineFile#m7|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_S,|org.eventb.core.guard#*" org.eventb.core.theorem="false"/>
<org.eventb.core.scAction name="orh" org.eventb.core.assignment="CiO1 ≔ CiO1∪{c ↦ org}" org.eventb.core.label="act1" org.eventb.core.source="/Test/m7.bum|org.eventb.core.machineFile#m7|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_S,|org.eventb.core.action#+"/>
<org.eventb.core.scParameter name="c" org.eventb.core.source="/Test/m7.bum|org.eventb.core.machineFile#m7|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_S,|org.eventb.core.parameter#(" org.eventb.core.type="CONTEXT"/>
<org.eventb.core.scParameter name="org" org.eventb.core.source="/Test/m7.bum|org.eventb.core.machineFile#m7|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_S,|org.eventb.core.parameter#'" org.eventb.core.type="ORG"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="Access_Requestet" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="Request_Access" org.eventb.core.source="/Test/m10.bum|org.eventb.core.machineFile#m10|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_SO">
<org.eventb.core.scRefinesEvent name="'" org.eventb.core.scTarget="/Test/m9.bcm|org.eventb.core.scMachineFile#m9|org.eventb.core.scEvent#Access_Requestet" org.eventb.core.source="/Test/m10.bum|org.eventb.core.machineFile#m10|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_SO|org.eventb.core.refinesEvent#'"/>
<org.eventb.core.scGuard name="(" org.eventb.core.label="grd1" org.eventb.core.predicate="e∈EMPLOYEE∧a∈ACTION∧o∈RESOURCE∧t∈ℕ1" org.eventb.core.source="/Test/m9.bum|org.eventb.core.machineFile#m9|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_S>|org.eventb.core.guard#*" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name=")" org.eventb.core.label="grd3" org.eventb.core.predicate="dist∈ran(PDistA)" org.eventb.core.source="/Test/m9.bum|org.eventb.core.machineFile#m9|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_S>|org.eventb.core.guard#\/" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="*" org.eventb.core.label="grd5" org.eventb.core.predicate="ac∈CONTEXT" org.eventb.core.source="/Test/m9.bum|org.eventb.core.machineFile#m9|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_S>|org.eventb.core.guard#2" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="+" org.eventb.core.label="grd4" org.eventb.core.predicate="∀e1⦂EMPLOYEE,a1⦂ACTION,o1⦂RESOURCE,t1⦂ℤ,dl⦂ℤ,d1⦂ℤ,ctx⦂CONTEXT·t1 ↦ e1 ↦ a1 ↦ o1 ↦ dl ↦ d1 ↦ ctx∈Access_Requested⇒t>t1" org.eventb.core.source="/Test/m9.bum|org.eventb.core.machineFile#m9|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_S>|org.eventb.core.guard#0" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="," org.eventb.core.label="grd2" org.eventb.core.predicate="∃u⦂UNIT,r⦂ROLE,v⦂VIEW,p⦂PERMISSION,org⦂ORG,act⦂ACTIVITY,c⦂CONTEXT,rio⦂ROLE×ORG,aio⦂ACTIVITY×ORG,vio⦂VIEW×ORG,cio⦂CONTEXT×ORG,acio⦂CONTEXT×ORG·e ↦ u∈EA∧u ↦ org∈OU∧rio=r ↦ org∧rio∈RiO∧u ↦ rio∈UR∧p ↦ rio∈PRA∧vio=v ↦ org∧vio∈ViO∧o ↦ vio∈RV∧p ↦ vio∈PVA∧aio=act ↦ org∧p ↦ aio∈PAA∧a ↦ vio∈AV∧a ↦ aio∈AA∧cio=c ↦ org∧p ↦ cio∈PCxA∧p ↦ dist∈PDistA∧acio=ac ↦ org∧p ↦ acio∈PAcA" org.eventb.core.source="/Test/m9.bum|org.eventb.core.machineFile#m9|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_S>|org.eventb.core.guard#+" org.eventb.core.theorem="false"/>
<org.eventb.core.scAction name="disu" org.eventb.core.assignment="Access_Requested ≔ Access_Requested∪{t ↦ e ↦ a ↦ o ↦ GLOBAL_DEADLINE ↦ dist ↦ ac}" org.eventb.core.label="act1" org.eventb.core.source="/Test/m9.bum|org.eventb.core.machineFile#m9|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_S>|org.eventb.core.action#."/>
<org.eventb.core.scParameter name="a" org.eventb.core.source="/Test/m9.bum|org.eventb.core.machineFile#m9|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_S>|org.eventb.core.parameter#(" org.eventb.core.type="ACTION"/>
<org.eventb.core.scParameter name="ac" org.eventb.core.source="/Test/m9.bum|org.eventb.core.machineFile#m9|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_S>|org.eventb.core.parameter#1" org.eventb.core.type="CONTEXT"/>
<org.eventb.core.scParameter name="e" org.eventb.core.source="/Test/m9.bum|org.eventb.core.machineFile#m9|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_S>|org.eventb.core.parameter#'" org.eventb.core.type="EMPLOYEE"/>
<org.eventb.core.scParameter name="dist" org.eventb.core.source="/Test/m9.bum|org.eventb.core.machineFile#m9|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_S>|org.eventb.core.parameter#-" org.eventb.core.type="ℤ"/>
<org.eventb.core.scParameter name="o" org.eventb.core.source="/Test/m9.bum|org.eventb.core.machineFile#m9|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_S>|org.eventb.core.parameter#)" org.eventb.core.type="RESOURCE"/>
<org.eventb.core.scParameter name="t" org.eventb.core.source="/Test/m9.bum|org.eventb.core.machineFile#m9|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_S>|org.eventb.core.parameter#," org.eventb.core.type="ℤ"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="Access_Requesteu" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="Treat_Request" org.eventb.core.source="/Test/m10.bum|org.eventb.core.machineFile#m10|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_SP">
<org.eventb.core.scGuard name="'" org.eventb.core.label="grd1" org.eventb.core.predicate="r∈Access_Requested∧t∈ℕ1" org.eventb.core.source="/Test/m10.bum|org.eventb.core.machineFile#m10|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_SP|org.eventb.core.guard#*" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="(" org.eventb.core.label="grd5" org.eventb.core.predicate="dec∈0 ‥ 1" org.eventb.core.source="/Test/m10.bum|org.eventb.core.machineFile#m10|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_SP|org.eventb.core.guard#0" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name=")" org.eventb.core.label="grd3" org.eventb.core.predicate="∀t1⦂ℤ,s1⦂EMPLOYEE,dec1⦂ℤ·t1 ↦ r ↦ s1 ↦ dec1∈Request_Treated⇒t>t1∧s1≠s" org.eventb.core.source="/Test/m10.bum|org.eventb.core.machineFile#m10|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_SP|org.eventb.core.guard#-" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="*" org.eventb.core.label="grd4" org.eventb.core.predicate="∀u⦂UNIT,u1⦂UNIT,t1⦂ℤ,s1⦂EMPLOYEE,dec1⦂ℤ·s ↦ u∈EA∧s1 ↦ u1∈EA∧t1<t∧t1 ↦ r ↦ s1 ↦ dec1∈Request_Treated⇒u≠u1" org.eventb.core.source="/Test/m10.bum|org.eventb.core.machineFile#m10|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_SP|org.eventb.core.guard#." org.eventb.core.theorem="false"/>
<org.eventb.core.scParameter name="dec" org.eventb.core.source="/Test/m10.bum|org.eventb.core.machineFile#m10|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_SP|org.eventb.core.parameter#\/" org.eventb.core.type="ℤ"/>
<org.eventb.core.scParameter name="r" org.eventb.core.source="/Test/m10.bum|org.eventb.core.machineFile#m10|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_SP|org.eventb.core.parameter#'" org.eventb.core.type="ℤ×EMPLOYEE×ACTION×RESOURCE×ℤ×ℤ×CONTEXT"/>
<org.eventb.core.scParameter name="s" org.eventb.core.source="/Test/m10.bum|org.eventb.core.machineFile#m10|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_SP|org.eventb.core.parameter#(" org.eventb.core.type="EMPLOYEE"/>
<org.eventb.core.scParameter name="t" org.eventb.core.source="/Test/m10.bum|org.eventb.core.machineFile#m10|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_SP|org.eventb.core.parameter#)" org.eventb.core.type="ℤ"/>
<org.eventb.core.scAction name="ded" org.eventb.core.assignment="Request_Treated ≔ Request_Treated∪{t ↦ r ↦ s ↦ dec}" org.eventb.core.label="act1" org.eventb.core.source="/Test/m10.bum|org.eventb.core.machineFile#m10|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_SP|org.eventb.core.action#,"/>
</org.eventb.core.scEvent>
</org.eventb.core.scMachineFile>