-
Notifications
You must be signed in to change notification settings - Fork 0
/
m2.bcm
213 lines (213 loc) · 54.9 KB
/
m2.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
<?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/m1.bcm" org.eventb.core.source="/Test/m2.bum|org.eventb.core.machineFile#m2|org.eventb.core.refinesMachine#'"/>
<org.eventb.core.scSeesContext name="(" org.eventb.core.scTarget="/Test/c0.bcc" org.eventb.core.source="/Test/m2.bum|org.eventb.core.machineFile#m2|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.scVariable name="AA" org.eventb.core.abstract="true" org.eventb.core.concrete="true" org.eventb.core.source="/Test/m2.bum|org.eventb.core.machineFile#m2|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/m2.bum|org.eventb.core.machineFile#m2|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/m2.bum|org.eventb.core.machineFile#m2|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/m2.bum|org.eventb.core.machineFile#m2|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/m2.bum|org.eventb.core.machineFile#m2|org.eventb.core.variable#_tdxRshy0Ee61L_Ef0FP_Qw" org.eventb.core.type="ℙ(EMPLOYEE×UNIT)"/>
<org.eventb.core.scVariable name="root" org.eventb.core.abstract="true" org.eventb.core.concrete="true" org.eventb.core.source="/Test/m2.bum|org.eventb.core.machineFile#m2|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/m2.bum|org.eventb.core.machineFile#m2|org.eventb.core.variable#_tdxRsBy0Ee61L_Ef0FP_Qw" org.eventb.core.type="ℙ(ROLE×ORG)"/>
<org.eventb.core.scVariable name="AiO" org.eventb.core.abstract="true" org.eventb.core.concrete="true" org.eventb.core.source="/Test/m2.bum|org.eventb.core.machineFile#m2|org.eventb.core.variable#_tdx4wBy0Ee61L_Ef0FP_Qw" org.eventb.core.type="ℙ(ACTIVITY×ORG)"/>
<org.eventb.core.scVariable name="UR1" org.eventb.core.abstract="false" org.eventb.core.concrete="true" org.eventb.core.source="/Test/m2.bum|org.eventb.core.machineFile#m2|org.eventb.core.variable#_tdyf0hy0Ee61L_Ef0FP_R5" org.eventb.core.type="ℙ(UNIT×(ROLE×ORG))"/>
<org.eventb.core.scVariable name="OU" org.eventb.core.abstract="true" org.eventb.core.concrete="true" org.eventb.core.source="/Test/m2.bum|org.eventb.core.machineFile#m2|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/m2.bum|org.eventb.core.machineFile#m2|org.eventb.core.variable#_tdyf0By0Ee61L_Ef0FP_Qw" org.eventb.core.type="ℙ(RESOURCE×(VIEW×ORG))"/>
<org.eventb.core.scVariable name="RiO1" org.eventb.core.abstract="false" org.eventb.core.concrete="true" org.eventb.core.source="/Test/m2.bum|org.eventb.core.machineFile#m2|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/m2.bum|org.eventb.core.machineFile#m2|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/m2.bum|org.eventb.core.machineFile#m2|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/m2.bum|org.eventb.core.machineFile#m2|org.eventb.core.variable#_tdyf0hy0Ee61L_Ef0FP_R." org.eventb.core.type="ℙ(UNIT×ORG)"/>
<org.eventb.core.scVariable name="PAA" org.eventb.core.abstract="true" org.eventb.core.concrete="true" org.eventb.core.source="/Test/m2.bum|org.eventb.core.machineFile#m2|org.eventb.core.variable#_tdx4wRy0Ee61L_Ef0FP_Qw" org.eventb.core.type="ℙ(PERMISSION×(ACTIVITY×ORG))"/>
<org.eventb.core.scVariable name="PCA" org.eventb.core.abstract="true" org.eventb.core.concrete="true" org.eventb.core.source="/Test/m2.bum|org.eventb.core.machineFile#m2|org.eventb.core.variable#_tdwqohy0Ee61L_Ef0FP_Qw" org.eventb.core.type="ℙ(PERMISSION×COR)"/>
<org.eventb.core.scVariable name="root1" org.eventb.core.abstract="true" org.eventb.core.concrete="true" org.eventb.core.source="/Test/m2.bum|org.eventb.core.machineFile#m2|org.eventb.core.variable#_tdyf0hy0Ee61L_Ef0FP_Q{" org.eventb.core.type="ℙ(ORG×UNIT)"/>
<org.eventb.core.scVariable name="PRA" org.eventb.core.abstract="true" org.eventb.core.concrete="true" org.eventb.core.source="/Test/m2.bum|org.eventb.core.machineFile#m2|org.eventb.core.variable#_tdxRsRy0Ee61L_Ef0FP_Qw" org.eventb.core.type="ℙ(PERMISSION×(ROLE×ORG))"/>
<org.eventb.core.scVariable name="PVA" org.eventb.core.abstract="true" org.eventb.core.concrete="true" org.eventb.core.source="/Test/m2.bum|org.eventb.core.machineFile#m2|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/m2.bum|org.eventb.core.machineFile#m2|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/m2.bum|org.eventb.core.machineFile#m2|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/m2.bum|org.eventb.core.machineFile#m2|org.eventb.core.variable#_tdyf0hy0Ee61L_Ef0FP_R(" org.eventb.core.type="ℙ(UNIT×UNIT)"/>
<org.eventb.core.scEvent name="root2" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="INITIALISATION" org.eventb.core.source="/Test/m2.bum|org.eventb.core.machineFile#m2|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_R\/">
<org.eventb.core.scRefinesEvent name="'" org.eventb.core.scTarget="/Test/m1.bcm|org.eventb.core.scMachineFile#m1|org.eventb.core.scEvent#root2" org.eventb.core.source="/Test/m2.bum|org.eventb.core.machineFile#m2|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_R\/"/>
<org.eventb.core.scAction name="(" org.eventb.core.assignment="CiO ≔ ∅ ⦂ ℙ(CONTEXT×ORG)" org.eventb.core.label="act1" org.eventb.core.source="/Test/m1.bum|org.eventb.core.machineFile#m1|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_Qx|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/m1.bum|org.eventb.core.machineFile#m1|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_Qx|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/m1.bum|org.eventb.core.machineFile#m1|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_Qx|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/m1.bum|org.eventb.core.machineFile#m1|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_Qx|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/m1.bum|org.eventb.core.machineFile#m1|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_Qx|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/m1.bum|org.eventb.core.machineFile#m1|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_Qx|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/m1.bum|org.eventb.core.machineFile#m1|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_Qx|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/m1.bum|org.eventb.core.machineFile#m1|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_Qx|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/m1.bum|org.eventb.core.machineFile#m1|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_Qx|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/m1.bum|org.eventb.core.machineFile#m1|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_Qx|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/m1.bum|org.eventb.core.machineFile#m1|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_Qx|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/m1.bum|org.eventb.core.machineFile#m1|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_Qx|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/m1.bum|org.eventb.core.machineFile#m1|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_Qx|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/m1.bum|org.eventb.core.machineFile#m1|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_Qx|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/m1.bum|org.eventb.core.machineFile#m1|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_Qx|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/m1.bum|org.eventb.core.machineFile#m1|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_Qx|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/m1.bum|org.eventb.core.machineFile#m1|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_Qx|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/m1.bum|org.eventb.core.machineFile#m1|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_Qx|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/m1.bum|org.eventb.core.machineFile#m1|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_Qx|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/m1.bum|org.eventb.core.machineFile#m1|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_Qx|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/m1.bum|org.eventb.core.machineFile#m1|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_Qx|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/m2.bum|org.eventb.core.machineFile#m2|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_R\/|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/m2.bum|org.eventb.core.machineFile#m2|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_R\/|org.eventb.core.action#_tdwDkhy0Ee61L_Ef0FP_Q}"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="root3" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="Abstract_Model_Generation" org.eventb.core.source="/Test/m2.bum|org.eventb.core.machineFile#m2|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_R0">
<org.eventb.core.scRefinesEvent name="'" org.eventb.core.scTarget="/Test/m1.bcm|org.eventb.core.scMachineFile#m1|org.eventb.core.scEvent#root3" org.eventb.core.source="/Test/m2.bum|org.eventb.core.machineFile#m2|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_R0|org.eventb.core.refinesEvent#'"/>
<org.eventb.core.scGuard name="(" org.eventb.core.label="grd4" org.eventb.core.predicate="aio∈ℙ(ACTIVITY × ORG)" org.eventb.core.source="/Test/m2.bum|org.eventb.core.machineFile#m2|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_R0|org.eventb.core.guard#_td1jIhy0Ee61L_Ef0FP_R\/" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name=")" org.eventb.core.label="grd5" org.eventb.core.predicate="vio⊆VIEW × ORG" org.eventb.core.source="/Test/m2.bum|org.eventb.core.machineFile#m2|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_R0|org.eventb.core.guard#_td1jIhy0Ee61L_Ef0FP_R2" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="*" org.eventb.core.label="grd6" org.eventb.core.predicate="cio⊆CONTEXT × ORG" org.eventb.core.source="/Test/m2.bum|org.eventb.core.machineFile#m2|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_R0|org.eventb.core.guard#_td1jIhy0Ee61L_Ef0FP_R6" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="+" org.eventb.core.label="grd8" org.eventb.core.predicate="ea⊆EMPLOYEE × UNIT" org.eventb.core.source="/Test/m2.bum|org.eventb.core.machineFile#m2|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_R0|org.eventb.core.guard#_td1jIhy0Ee61L_Ef0FP_R>" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="," org.eventb.core.label="grd10" org.eventb.core.predicate="cio⊆CONTEXT × ORG" org.eventb.core.source="/Test/m2.bum|org.eventb.core.machineFile#m2|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_R0|org.eventb.core.guard#_td1jIhy0Ee61L_Ef0FP_R@" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="-" org.eventb.core.label="grd13" org.eventb.core.predicate="av⊆ACTION × vio" org.eventb.core.source="/Test/m2.bum|org.eventb.core.machineFile#m2|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_R0|org.eventb.core.guard#_td1jIhy0Ee61L_Ef0FP_RI" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="." org.eventb.core.label="grd14" org.eventb.core.predicate="aa⊆ACTION × aio" org.eventb.core.source="/Test/m2.bum|org.eventb.core.machineFile#m2|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_R0|org.eventb.core.guard#_td1jIhy0Ee61L_Ef0FP_RJ" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="/" org.eventb.core.label="grd15" org.eventb.core.predicate="rv⊆RESOURCE × vio" org.eventb.core.source="/Test/m2.bum|org.eventb.core.machineFile#m2|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_R0|org.eventb.core.guard#_td1jIhy0Ee61L_Ef0FP_RK" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="0" org.eventb.core.label="grd17" org.eventb.core.predicate="pra∈PERMISSION ⇸ RiO1" org.eventb.core.source="/Test/m2.bum|org.eventb.core.machineFile#m2|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_R0|org.eventb.core.guard#_td1jIhy0Ee61L_Ef0FP_RQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="1" org.eventb.core.label="grd18" org.eventb.core.predicate="paa∈PERMISSION ⇸ aio" org.eventb.core.source="/Test/m2.bum|org.eventb.core.machineFile#m2|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_R0|org.eventb.core.guard#_td1jIhy0Ee61L_Ef0FP_RR" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="2" org.eventb.core.label="grd19" org.eventb.core.predicate="pva∈PERMISSION ⇸ vio" org.eventb.core.source="/Test/m2.bum|org.eventb.core.machineFile#m2|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_R0|org.eventb.core.guard#internal1" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="3" org.eventb.core.label="grd20" org.eventb.core.predicate="pcxa∈PERMISSION ⇸ cio" org.eventb.core.source="/Test/m2.bum|org.eventb.core.machineFile#m2|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_R0|org.eventb.core.guard#_td1jIhy0Ee61L_Ef0FP_RT" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="4" org.eventb.core.label="grd21" org.eventb.core.predicate="pca∈PERMISSION ⇸ COR" org.eventb.core.source="/Test/m2.bum|org.eventb.core.machineFile#m2|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_R0|org.eventb.core.guard#_td1jIhy0Ee61L_Ef0FP_RU" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="5" org.eventb.core.label="grd16" org.eventb.core.predicate="ca⊆COR × UNIT × POSITION × DEADLINE" org.eventb.core.source="/Test/m2.bum|org.eventb.core.machineFile#m2|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_R0|org.eventb.core.guard#_td1jIhy0Ee61L_Ef0FP_RS" org.eventb.core.theorem="false"/>
<org.eventb.core.scParameter name="aa" org.eventb.core.source="/Test/m2.bum|org.eventb.core.machineFile#m2|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_R0|org.eventb.core.parameter#_td1jIhy0Ee61L_Ef0FP_RL" org.eventb.core.type="ℙ(ACTION×(ACTIVITY×ORG))"/>
<org.eventb.core.scParameter name="rv" org.eventb.core.source="/Test/m2.bum|org.eventb.core.machineFile#m2|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_R0|org.eventb.core.parameter#_td1jIhy0Ee61L_Ef0FP_RN" org.eventb.core.type="ℙ(RESOURCE×(VIEW×ORG))"/>
<org.eventb.core.scParameter name="aio" org.eventb.core.source="/Test/m2.bum|org.eventb.core.machineFile#m2|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_R0|org.eventb.core.parameter#_td1jIhy0Ee61L_Ef0FP_R." org.eventb.core.type="ℙ(ACTIVITY×ORG)"/>
<org.eventb.core.scParameter name="cio" org.eventb.core.source="/Test/m2.bum|org.eventb.core.machineFile#m2|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_R0|org.eventb.core.parameter#_td1jIhy0Ee61L_Ef0FP_R7" org.eventb.core.type="ℙ(CONTEXT×ORG)"/>
<org.eventb.core.scParameter name="pcxa" org.eventb.core.source="/Test/m2.bum|org.eventb.core.machineFile#m2|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_R0|org.eventb.core.parameter#_td1jIhy0Ee61L_Ef0FP_RZ" org.eventb.core.type="ℙ(PERMISSION×(CONTEXT×ORG))"/>
<org.eventb.core.scParameter name="pca" org.eventb.core.source="/Test/m2.bum|org.eventb.core.machineFile#m2|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_R0|org.eventb.core.parameter#_td1jIhy0Ee61L_Ef0FP_RY" org.eventb.core.type="ℙ(PERMISSION×COR)"/>
<org.eventb.core.scParameter name="paa" org.eventb.core.source="/Test/m2.bum|org.eventb.core.machineFile#m2|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_R0|org.eventb.core.parameter#_td1jIhy0Ee61L_Ef0FP_RW" org.eventb.core.type="ℙ(PERMISSION×(ACTIVITY×ORG))"/>
<org.eventb.core.scParameter name="av" org.eventb.core.source="/Test/m2.bum|org.eventb.core.machineFile#m2|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_R0|org.eventb.core.parameter#_td1jIhy0Ee61L_Ef0FP_RM" org.eventb.core.type="ℙ(ACTION×(VIEW×ORG))"/>
<org.eventb.core.scParameter name="pva" org.eventb.core.source="/Test/m2.bum|org.eventb.core.machineFile#m2|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_R0|org.eventb.core.parameter#_td1jIhy0Ee61L_Ef0FP_RX" org.eventb.core.type="ℙ(PERMISSION×(VIEW×ORG))"/>
<org.eventb.core.scParameter name="ea" org.eventb.core.source="/Test/m2.bum|org.eventb.core.machineFile#m2|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_R0|org.eventb.core.parameter#_td1jIhy0Ee61L_Ef0FP_RC" org.eventb.core.type="ℙ(EMPLOYEE×UNIT)"/>
<org.eventb.core.scParameter name="vio" org.eventb.core.source="/Test/m2.bum|org.eventb.core.machineFile#m2|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_R0|org.eventb.core.parameter#_td1jIhy0Ee61L_Ef0FP_R3" org.eventb.core.type="ℙ(VIEW×ORG)"/>
<org.eventb.core.scParameter name="ca" org.eventb.core.source="/Test/m2.bum|org.eventb.core.machineFile#m2|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_R0|org.eventb.core.parameter#_td1jIhy0Ee61L_Ef0FP_RP" org.eventb.core.type="ℙ(COR×UNIT×ℤ×ℤ)"/>
<org.eventb.core.scParameter name="pra" org.eventb.core.source="/Test/m2.bum|org.eventb.core.machineFile#m2|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_R0|org.eventb.core.parameter#_td1jIhy0Ee61L_Ef0FP_RV" org.eventb.core.type="ℙ(PERMISSION×(ROLE×ORG))"/>
<org.eventb.core.scAction name="pcxb" org.eventb.core.assignment="CiO ≔ cio" org.eventb.core.label="act1" org.eventb.core.source="/Test/m2.bum|org.eventb.core.machineFile#m2|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_R0|org.eventb.core.action#_td1jIBy0Ee61L_Ef0FP_Qw"/>
<org.eventb.core.scAction name="pcxc" org.eventb.core.assignment="AiO ≔ aio" org.eventb.core.label="act4" org.eventb.core.source="/Test/m2.bum|org.eventb.core.machineFile#m2|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_R0|org.eventb.core.action#__StoEBy2Ee61L_Ef0FP_Qw"/>
<org.eventb.core.scAction name="pcxd" org.eventb.core.assignment="ViO ≔ vio" org.eventb.core.label="act6" org.eventb.core.source="/Test/m2.bum|org.eventb.core.machineFile#m2|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_R0|org.eventb.core.action#_D2pGQBy3Ee61L_Ef0FP_Qw"/>
<org.eventb.core.scAction name="pcxe" org.eventb.core.assignment="PCA ≔ pca" org.eventb.core.label="act9" org.eventb.core.source="/Test/m2.bum|org.eventb.core.machineFile#m2|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_R0|org.eventb.core.action#internal4"/>
<org.eventb.core.scAction name="pcxf" org.eventb.core.assignment="PRA ≔ pra" org.eventb.core.label="act10" org.eventb.core.source="/Test/m2.bum|org.eventb.core.machineFile#m2|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_R0|org.eventb.core.action#internal5"/>
<org.eventb.core.scAction name="pcxg" org.eventb.core.assignment="EA ≔ ea" org.eventb.core.label="act11" org.eventb.core.source="/Test/m2.bum|org.eventb.core.machineFile#m2|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_R0|org.eventb.core.action#_td1jIhy0Ee61L_Ef0FP_R+"/>
<org.eventb.core.scAction name="pcxh" org.eventb.core.assignment="PAA ≔ paa" org.eventb.core.label="act13" org.eventb.core.source="/Test/m2.bum|org.eventb.core.machineFile#m2|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_R0|org.eventb.core.action#internal7"/>
<org.eventb.core.scAction name="pcxi" org.eventb.core.assignment="PVA ≔ pva" org.eventb.core.label="act14" org.eventb.core.source="/Test/m2.bum|org.eventb.core.machineFile#m2|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_R0|org.eventb.core.action#internal8"/>
<org.eventb.core.scAction name="pcxj" org.eventb.core.assignment="PCxA ≔ pcxa" org.eventb.core.label="act15" org.eventb.core.source="/Test/m2.bum|org.eventb.core.machineFile#m2|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_R0|org.eventb.core.action#internal9"/>
<org.eventb.core.scAction name="pcxk" org.eventb.core.assignment="AV ≔ av" org.eventb.core.label="act16" org.eventb.core.source="/Test/m2.bum|org.eventb.core.machineFile#m2|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_R0|org.eventb.core.action#_td1jIhy0Ee61L_Ef0FP_R9"/>
<org.eventb.core.scAction name="pcxl" org.eventb.core.assignment="AA ≔ aa" org.eventb.core.label="act17" org.eventb.core.source="/Test/m2.bum|org.eventb.core.machineFile#m2|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_R0|org.eventb.core.action#_td1jIhy0Ee61L_Ef0FP_R:"/>
<org.eventb.core.scAction name="pcxm" org.eventb.core.assignment="RV ≔ rv" org.eventb.core.label="act18" org.eventb.core.source="/Test/m2.bum|org.eventb.core.machineFile#m2|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_R0|org.eventb.core.action#_td1jIhy0Ee61L_Ef0FP_R;"/>
<org.eventb.core.scAction name="pcxn" org.eventb.core.assignment="root ≔ root1" org.eventb.core.label="act2" org.eventb.core.source="/Test/m2.bum|org.eventb.core.machineFile#m2|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_R0|org.eventb.core.action#_td1jIRy0Ee61L_Ef0FP_Qw"/>
<org.eventb.core.scAction name="pcxo" org.eventb.core.assignment="UH ≔ UH1" org.eventb.core.label="act5" org.eventb.core.source="/Test/m2.bum|org.eventb.core.machineFile#m2|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_R0|org.eventb.core.action#_BFqMYBy3Ee61L_Ef0FP_Qw"/>
<org.eventb.core.scAction name="pcxp" org.eventb.core.assignment="CA ≔ ca" org.eventb.core.label="act8" org.eventb.core.source="/Test/m2.bum|org.eventb.core.machineFile#m2|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_R0|org.eventb.core.action#_PSi28By5Ee61L_Ef0FP_Qw"/>
<org.eventb.core.scAction name="pcxq" org.eventb.core.assignment="OU ≔ OU1" org.eventb.core.label="act3" org.eventb.core.source="/Test/m2.bum|org.eventb.core.machineFile#m2|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_R0|org.eventb.core.action#_td1jIhy0Ee61L_Ef0FP_Qw"/>
<org.eventb.core.scAction name="pcxr" org.eventb.core.assignment="RiO ≔ RiO1" org.eventb.core.label="act7" org.eventb.core.source="/Test/m2.bum|org.eventb.core.machineFile#m2|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_R0|org.eventb.core.action#_aKm3kBy3Ee61L_Ef0FP_Qw"/>
<org.eventb.core.scAction name="pcxs" org.eventb.core.assignment="UR ≔ UR1" org.eventb.core.label="act12" org.eventb.core.source="/Test/m2.bum|org.eventb.core.machineFile#m2|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_R0|org.eventb.core.action#_td1jIhy0Ee61L_Ef0FP_R,"/>
<org.eventb.core.scWitness name="pcxt" org.eventb.core.label="ur" org.eventb.core.predicate="ur=UR1" org.eventb.core.source="/Test/m2.bum|org.eventb.core.machineFile#m2|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_R0|org.eventb.core.witness#_td1jIhy0Ee61L_Ef0FP_RO"/>
<org.eventb.core.scWitness name="pcxu" org.eventb.core.label="rio" org.eventb.core.predicate="rio=RiO1" org.eventb.core.source="/Test/m2.bum|org.eventb.core.machineFile#m2|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_R0|org.eventb.core.witness#_td1jIhy0Ee61L_Ef0FP_RP"/>
<org.eventb.core.scWitness name="pcxv" org.eventb.core.label="ou" org.eventb.core.predicate="ou=OU1" org.eventb.core.source="/Test/m2.bum|org.eventb.core.machineFile#m2|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_R0|org.eventb.core.witness#_td1jIhy0Ee61L_Ef0FP_RQ"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="root4" 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/m2.bum|org.eventb.core.machineFile#m2|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_R1">
<org.eventb.core.scRefinesEvent name="'" org.eventb.core.scTarget="/Test/m1.bcm|org.eventb.core.scMachineFile#m1|org.eventb.core.scEvent#root4" org.eventb.core.source="/Test/m2.bum|org.eventb.core.machineFile#m2|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_R1|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="root5" 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/m2.bum|org.eventb.core.machineFile#m2|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_R2">
<org.eventb.core.scRefinesEvent name="'" org.eventb.core.scTarget="/Test/m1.bcm|org.eventb.core.scMachineFile#m1|org.eventb.core.scEvent#root5" org.eventb.core.source="/Test/m2.bum|org.eventb.core.machineFile#m2|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_R2|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/m1.bum|org.eventb.core.machineFile#m1|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/m1.bum|org.eventb.core.machineFile#m1|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/m1.bum|org.eventb.core.machineFile#m1|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/m1.bum|org.eventb.core.machineFile#m1|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/m1.bum|org.eventb.core.machineFile#m1|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/m1.bum|org.eventb.core.machineFile#m1|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/m1.bum|org.eventb.core.machineFile#m1|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="u1∈dom(OU1)∧u2∈dom(OU1)" org.eventb.core.source="/Test/m1.bum|org.eventb.core.machineFile#m1|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_R+|org.eventb.core.guard#2" 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/m1.bum|org.eventb.core.machineFile#m1|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_R+|org.eventb.core.action#+"/>
<org.eventb.core.scParameter name="u1" org.eventb.core.source="/Test/m1.bum|org.eventb.core.machineFile#m1|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/m1.bum|org.eventb.core.machineFile#m1|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="root6" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="Assign_Unit_to_Org" org.eventb.core.source="/Test/m2.bum|org.eventb.core.machineFile#m2|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_R3">
<org.eventb.core.scRefinesEvent name="'" org.eventb.core.scTarget="/Test/m1.bcm|org.eventb.core.scMachineFile#m1|org.eventb.core.scEvent#root6" org.eventb.core.source="/Test/m2.bum|org.eventb.core.machineFile#m2|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_R3|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.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.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.scEvent>
<org.eventb.core.scEvent name="root7" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="Assign_Role_to_Unit" org.eventb.core.source="/Test/m2.bum|org.eventb.core.machineFile#m2|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_R4">
<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.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.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.scEvent>
<org.eventb.core.scEvent name="root8" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="Assign_Role_to_Organization" org.eventb.core.source="/Test/m2.bum|org.eventb.core.machineFile#m2|org.eventb.core.event#_tdyf0hy0Ee61L_Ef0FP_R8">
<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.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.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.scEvent>
</org.eventb.core.scMachineFile>