-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathm1.bum
148 lines (148 loc) · 19.1 KB
/
m1.bum
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
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<org.eventb.core.machineFile org.eventb.core.comment="This event defines organization hierarchy: root, unit to organization assigment and unit hierarahy" org.eventb.core.configuration="org.eventb.core.fwd;ch.ethz.eventb.qualprob.qpConfig" version="5">
<org.eventb.core.refinesMachine name="'" org.eventb.core.target="m0"/>
<org.eventb.core.seesContext name="_tdtnUBy0Ee61L_Ef0FP_Qw" org.eventb.core.target="c0"/>
<org.eventb.core.variable name="_tdwqohy0Ee61L_Ef0FP_Qw" org.eventb.core.identifier="PCA"/>
<org.eventb.core.variable name="_tdwqoxy0Ee61L_Ef0FP_Qw" org.eventb.core.identifier="root"/>
<org.eventb.core.variable name="_tdwqpBy0Ee61L_Ef0FP_Qw" org.eventb.core.identifier="OU"/>
<org.eventb.core.variable name="_tdxRsBy0Ee61L_Ef0FP_Qw" org.eventb.core.identifier="RiO"/>
<org.eventb.core.variable name="_tdyf0hy0Ee61L_Ef0FP_R*" org.eventb.core.identifier="UH"/>
<org.eventb.core.variable name="_tdxRsRy0Ee61L_Ef0FP_Qw" org.eventb.core.identifier="PRA"/>
<org.eventb.core.variable name="_tdxRshy0Ee61L_Ef0FP_Qw" org.eventb.core.identifier="EA"/>
<org.eventb.core.variable name="_tdxRsxy0Ee61L_Ef0FP_Qw" org.eventb.core.identifier="UR"/>
<org.eventb.core.variable name="_tdxRtBy0Ee61L_Ef0FP_Qw" org.eventb.core.identifier="ViO"/>
<org.eventb.core.variable name="_tdx4wBy0Ee61L_Ef0FP_Qw" org.eventb.core.identifier="AiO"/>
<org.eventb.core.variable name="_tdx4wRy0Ee61L_Ef0FP_Qw" org.eventb.core.identifier="PAA"/>
<org.eventb.core.variable name="_tdx4why0Ee61L_Ef0FP_Qw" org.eventb.core.identifier="PVA"/>
<org.eventb.core.variable name="_tdx4wxy0Ee61L_Ef0FP_Qw" org.eventb.core.identifier="CiO"/>
<org.eventb.core.variable name="_tdx4xBy0Ee61L_Ef0FP_Qw" org.eventb.core.identifier="PCxA"/>
<org.eventb.core.variable name="_tdyf0By0Ee61L_Ef0FP_Qw" org.eventb.core.identifier="RV"/>
<org.eventb.core.variable name="_tdyf0Ry0Ee61L_Ef0FP_Qw" org.eventb.core.identifier="AV"/>
<org.eventb.core.variable name="_tdyf0hy0Ee61L_Ef0FP_Qw" org.eventb.core.identifier="AA"/>
<org.eventb.core.event name="_tdyf0hy0Ee61L_Ef0FP_Qx" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="INITIALISATION">
<org.eventb.core.action name="_tduOYBy0Ee61L_Ef0FP_Qw" org.eventb.core.assignment="CiO ≔ ∅" org.eventb.core.generated="false" org.eventb.core.label="act1"/>
<org.eventb.core.action name="_tduOYRy0Ee61L_Ef0FP_Qw" org.eventb.core.assignment="root :∈ ORG ⇸ UNIT" org.eventb.core.generated="false" org.eventb.core.label="act2"/>
<org.eventb.core.action name="_tdu1cBy0Ee61L_Ef0FP_Qw" org.eventb.core.assignment="OU :∈ UNIT ⇸ ORG" org.eventb.core.generated="false" org.eventb.core.label="act3"/>
<org.eventb.core.action name="_tdu1cRy0Ee61L_Ef0FP_Qw" org.eventb.core.assignment="AiO ≔ ∅" org.eventb.core.generated="false" org.eventb.core.label="act4"/>
<org.eventb.core.action name="_tdu1chy0Ee61L_Ef0FP_Qw" org.eventb.core.assignment="UH :∈ UNIT ⇸ UNIT" org.eventb.core.generated="false" org.eventb.core.label="act5"/>
<org.eventb.core.action name="_tdu1cxy0Ee61L_Ef0FP_Qw" org.eventb.core.assignment="ViO ≔ ∅" org.eventb.core.generated="false" org.eventb.core.label="act6"/>
<org.eventb.core.action name="_tdu1dBy0Ee61L_Ef0FP_Qw" org.eventb.core.assignment="RiO ≔ ∅" org.eventb.core.generated="false" org.eventb.core.label="act7"/>
<org.eventb.core.action name="_tdu1dhy0Ee61L_Ef0FP_Qw" org.eventb.core.assignment="PCA :∈ PERMISSION ⇸ COR" org.eventb.core.generated="false" org.eventb.core.label="act9"/>
<org.eventb.core.action name="_tdvcgBy0Ee61L_Ef0FP_Qw" org.eventb.core.assignment="PRA ≔ ∅" org.eventb.core.generated="false" org.eventb.core.label="act10"/>
<org.eventb.core.action name="_tdvcgRy0Ee61L_Ef0FP_Qw" org.eventb.core.assignment="EA ≔ ∅" org.eventb.core.generated="false" org.eventb.core.label="act11"/>
<org.eventb.core.action name="_tdvcghy0Ee61L_Ef0FP_Qw" org.eventb.core.assignment="UR ≔ ∅" org.eventb.core.generated="false" org.eventb.core.label="act12"/>
<org.eventb.core.action name="_tdvcgxy0Ee61L_Ef0FP_Qw" org.eventb.core.assignment="PAA ≔ ∅" org.eventb.core.generated="false" org.eventb.core.label="act13"/>
<org.eventb.core.action name="_tdvchBy0Ee61L_Ef0FP_Qw" org.eventb.core.assignment="PVA ≔ ∅" org.eventb.core.generated="false" org.eventb.core.label="act14"/>
<org.eventb.core.action name="_tdvchRy0Ee61L_Ef0FP_Qw" org.eventb.core.assignment="PCxA ≔ ∅" org.eventb.core.generated="false" org.eventb.core.label="act15"/>
<org.eventb.core.action name="_tdwDkBy0Ee61L_Ef0FP_Qw" org.eventb.core.assignment="AV ≔ ∅" org.eventb.core.generated="false" org.eventb.core.label="act16"/>
<org.eventb.core.action name="_tdwDkRy0Ee61L_Ef0FP_Qw" org.eventb.core.assignment="AA ≔ ∅" org.eventb.core.generated="false" org.eventb.core.label="act17"/>
<org.eventb.core.action name="_tdwDkhy0Ee61L_Ef0FP_Qw" org.eventb.core.assignment="RV ≔ ∅" org.eventb.core.generated="false" org.eventb.core.label="act18"/>
<org.eventb.core.action name="_tdwDkhy0Ee61L_Ef0FP_Qx" org.eventb.core.assignment="root1 ≔ ∅" org.eventb.core.label="act20"/>
<org.eventb.core.action name="_tdwDkhy0Ee61L_Ef0FP_Qy" org.eventb.core.assignment="OU1 :∈ UNIT ⇸ ORG" org.eventb.core.label="act21"/>
<org.eventb.core.action name="_tdwDkhy0Ee61L_Ef0FP_Qz" org.eventb.core.assignment="UH1 ≔ ∅" org.eventb.core.label="act22"/>
<org.eventb.core.action name="_tdwDkhy0Ee61L_Ef0FP_Q{" org.eventb.core.assignment="CA ≔ ∅" org.eventb.core.label="act23"/>
</org.eventb.core.event>
<org.eventb.core.event name="_tdyf0hy0Ee61L_Ef0FP_Qy" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="Abstract_Model_Generation">
<org.eventb.core.refinesEvent name="'" org.eventb.core.target="Abstract_Model_Generation"/>
<org.eventb.core.action name="_td1jIBy0Ee61L_Ef0FP_Qw" org.eventb.core.assignment="CiO ≔ cio" org.eventb.core.generated="false" org.eventb.core.label="act1"/>
<org.eventb.core.action name="_td1jIhy0Ee61L_Ef0FP_Qw" org.eventb.core.assignment="OU ≔ ou" org.eventb.core.generated="false" org.eventb.core.label="act3"/>
<org.eventb.core.action name="__StoEBy2Ee61L_Ef0FP_Qw" org.eventb.core.assignment="AiO ≔ aio" org.eventb.core.generated="false" org.eventb.core.label="act4"/>
<org.eventb.core.action name="_D2pGQBy3Ee61L_Ef0FP_Qw" org.eventb.core.assignment="ViO ≔ vio" org.eventb.core.generated="false" org.eventb.core.label="act6"/>
<org.eventb.core.action name="_aKm3kBy3Ee61L_Ef0FP_Qw" org.eventb.core.assignment="RiO ≔ rio" org.eventb.core.generated="false" org.eventb.core.label="act7"/>
<org.eventb.core.guard name="_td1jIhy0Ee61L_Ef0FP_R)" org.eventb.core.label="grd2" org.eventb.core.predicate="rio ⊆ ROLE × ORG"/>
<org.eventb.core.action name="internal4" org.eventb.core.assignment="PCA ≔ pca" org.eventb.core.label="act9"/>
<org.eventb.core.action name="internal5" org.eventb.core.assignment="PRA ≔ pra" org.eventb.core.label="act10"/>
<org.eventb.core.parameter name="_td1jIhy0Ee61L_Ef0FP_R(" org.eventb.core.identifier="rio"/>
<org.eventb.core.action name="_td1jIhy0Ee61L_Ef0FP_R+" org.eventb.core.assignment="EA ≔ ea" org.eventb.core.label="act11"/>
<org.eventb.core.action name="_td1jIhy0Ee61L_Ef0FP_R," org.eventb.core.assignment="UR ≔ ur" org.eventb.core.label="act12"/>
<org.eventb.core.action name="internal6" org.eventb.core.assignment="PAA ≔ paa" org.eventb.core.label="act13"/>
<org.eventb.core.parameter name="_td1jIhy0Ee61L_Ef0FP_R." org.eventb.core.identifier="aio"/>
<org.eventb.core.guard name="_td1jIhy0Ee61L_Ef0FP_R/" org.eventb.core.label="grd4" org.eventb.core.predicate="aio ∈ ℙ(ACTIVITY × ORG)"/>
<org.eventb.core.action name="internal7" org.eventb.core.assignment="PVA ≔ pva" org.eventb.core.label="act14"/>
<org.eventb.core.guard name="_td1jIhy0Ee61L_Ef0FP_R2" org.eventb.core.label="grd5" org.eventb.core.predicate="vio ⊆ VIEW × ORG"/>
<org.eventb.core.parameter name="_td1jIhy0Ee61L_Ef0FP_R3" org.eventb.core.identifier="vio"/>
<org.eventb.core.action name="internal8" org.eventb.core.assignment="PCxA ≔ pcxa" org.eventb.core.label="act15"/>
<org.eventb.core.guard name="_td1jIhy0Ee61L_Ef0FP_R6" org.eventb.core.label="grd6" org.eventb.core.predicate="cio ⊆ CONTEXT × ORG"/>
<org.eventb.core.parameter name="_td1jIhy0Ee61L_Ef0FP_R7" org.eventb.core.identifier="cio"/>
<org.eventb.core.action name="_td1jIhy0Ee61L_Ef0FP_R9" org.eventb.core.assignment="AV ≔ av" org.eventb.core.label="act16"/>
<org.eventb.core.action name="_td1jIhy0Ee61L_Ef0FP_R:" org.eventb.core.assignment="AA ≔ aa" org.eventb.core.label="act17"/>
<org.eventb.core.action name="_td1jIhy0Ee61L_Ef0FP_R;" org.eventb.core.assignment="RV ≔ rv" org.eventb.core.label="act18"/>
<org.eventb.core.guard name="_td1jIhy0Ee61L_Ef0FP_R>" org.eventb.core.label="grd8" org.eventb.core.predicate="ea ⊆ EMPLOYEE × UNIT"/>
<org.eventb.core.guard name="_td1jIhy0Ee61L_Ef0FP_R?" org.eventb.core.label="grd9" org.eventb.core.predicate="ou ∈ UNIT ⇸ ORG "/>
<org.eventb.core.guard name="_td1jIhy0Ee61L_Ef0FP_R@" org.eventb.core.label="grd10" org.eventb.core.predicate="cio ⊆ CONTEXT × ORG"/>
<org.eventb.core.parameter name="_td1jIhy0Ee61L_Ef0FP_RC" org.eventb.core.identifier="ea"/>
<org.eventb.core.parameter name="_td1jIhy0Ee61L_Ef0FP_RD" org.eventb.core.identifier="ou"/>
<org.eventb.core.guard name="_td1jIhy0Ee61L_Ef0FP_RG" org.eventb.core.label="grd12" org.eventb.core.predicate="ur ⊆ UNIT × rio"/>
<org.eventb.core.parameter name="_td1jIhy0Ee61L_Ef0FP_RH" org.eventb.core.identifier="ur"/>
<org.eventb.core.guard name="_td1jIhy0Ee61L_Ef0FP_RI" org.eventb.core.label="grd13" org.eventb.core.predicate="av ⊆ ACTION × vio"/>
<org.eventb.core.guard name="_td1jIhy0Ee61L_Ef0FP_RJ" org.eventb.core.label="grd14" org.eventb.core.predicate="aa ⊆ ACTION × aio"/>
<org.eventb.core.guard name="_td1jIhy0Ee61L_Ef0FP_RK" org.eventb.core.label="grd15" org.eventb.core.predicate="rv ⊆ RESOURCE × vio"/>
<org.eventb.core.parameter name="_td1jIhy0Ee61L_Ef0FP_RL" org.eventb.core.identifier="aa"/>
<org.eventb.core.parameter name="_td1jIhy0Ee61L_Ef0FP_RM" org.eventb.core.identifier="av"/>
<org.eventb.core.parameter name="_td1jIhy0Ee61L_Ef0FP_RN" org.eventb.core.identifier="rv"/>
<org.eventb.core.guard name="_td1jIhy0Ee61L_Ef0FP_RO" org.eventb.core.label="grd16" org.eventb.core.predicate="ca ⊆ COR × UNIT × POSITION × DEADLINE"/>
<org.eventb.core.parameter name="_td1jIhy0Ee61L_Ef0FP_RP" org.eventb.core.identifier="ca"/>
<org.eventb.core.guard name="_td1jIhy0Ee61L_Ef0FP_RQ" org.eventb.core.label="grd17" org.eventb.core.predicate="pra ∈ PERMISSION ⇸ rio"/>
<org.eventb.core.guard name="_td1jIhy0Ee61L_Ef0FP_RR" org.eventb.core.label="grd18" org.eventb.core.predicate="paa ∈ PERMISSION ⇸ aio"/>
<org.eventb.core.guard name="_td1jIhy0Ee61L_Ef0FP_RS" org.eventb.core.label="grd19" org.eventb.core.predicate="pva ∈ PERMISSION ⇸ vio"/>
<org.eventb.core.guard name="_td1jIhy0Ee61L_Ef0FP_RT" org.eventb.core.label="grd20" org.eventb.core.predicate="pcxa ∈ PERMISSION ⇸ cio"/>
<org.eventb.core.guard name="_td1jIhy0Ee61L_Ef0FP_RU" org.eventb.core.label="grd21" org.eventb.core.predicate="pca ∈ PERMISSION ⇸ COR"/>
<org.eventb.core.parameter name="_td1jIhy0Ee61L_Ef0FP_RV" org.eventb.core.identifier="pra"/>
<org.eventb.core.parameter name="_td1jIhy0Ee61L_Ef0FP_RW" org.eventb.core.identifier="paa"/>
<org.eventb.core.parameter name="_td1jIhy0Ee61L_Ef0FP_RX" org.eventb.core.identifier="pva"/>
<org.eventb.core.parameter name="_td1jIhy0Ee61L_Ef0FP_RY" org.eventb.core.identifier="pca"/>
<org.eventb.core.parameter name="_td1jIhy0Ee61L_Ef0FP_RZ" org.eventb.core.identifier="pcxa"/>
<org.eventb.core.action name="_td1jIRy0Ee61L_Ef0FP_Qw" org.eventb.core.assignment="root ≔ root1" org.eventb.core.generated="false" org.eventb.core.label="act2"/>
<org.eventb.core.action name="_BFqMYBy3Ee61L_Ef0FP_Qw" org.eventb.core.assignment="UH ≔ UH1" org.eventb.core.generated="false" org.eventb.core.label="act5"/>
<org.eventb.core.action name="_PSi28By5Ee61L_Ef0FP_Qw" org.eventb.core.assignment="CA ≔ ca" org.eventb.core.generated="false" org.eventb.core.label="act8"/>
<org.eventb.core.witness name="_td1jIhy0Ee61L_Ef0FP_RO" org.eventb.core.label="rt" org.eventb.core.predicate="rt = root1"/>
<org.eventb.core.witness name="_td1jIhy0Ee61L_Ef0FP_RP" org.eventb.core.label="uh" org.eventb.core.predicate="uh = UH1"/>
</org.eventb.core.event>
<org.eventb.core.event name="_tdyf0hy0Ee61L_Ef0FP_Qz" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="Assign_Oragnization_Root">
<org.eventb.core.parameter name="'" org.eventb.core.identifier="u"/>
<org.eventb.core.parameter name="(" org.eventb.core.identifier="org"/>
<org.eventb.core.guard name=")" org.eventb.core.label="grd1" org.eventb.core.predicate="org ∈ ORG ∧ u ∈ UNIT"/>
<org.eventb.core.action name="*" org.eventb.core.assignment="root1 ≔ root1 ∪ {org↦u}" org.eventb.core.label="act1"/>
<org.eventb.core.guard name="-" org.eventb.core.label="grd2" org.eventb.core.predicate="org ∉ dom(root1)"/>
<org.eventb.core.guard name="." org.eventb.core.label="grd3" org.eventb.core.predicate="u ∉ dom(UH1)"/>
<org.eventb.core.guard name="/" org.eventb.core.label="grd4" org.eventb.core.predicate="ran(root1 ∪ {org↦u}) ∩ dom(UH1) = ∅"/>
<org.eventb.core.guard name="0" org.eventb.core.label="grd5" org.eventb.core.predicate="u↦org ∈ OU1"/>
<org.eventb.core.guard name="1" org.eventb.core.label="grd6" org.eventb.core.predicate="u ∉ ran(root1)"/>
</org.eventb.core.event>
<org.eventb.core.variable name="_tdyf0hy0Ee61L_Ef0FP_Q{" org.eventb.core.identifier="root1"/>
<org.eventb.core.invariant name="_tdyf0hy0Ee61L_Ef0FP_R)" org.eventb.core.comment="The variable UH1 is a concrete variable of UH" org.eventb.core.label="inv2" org.eventb.core.predicate="UH1 ∈ UNIT ⇸ UNIT"/>
<org.eventb.core.invariant name="_tdyf0hy0Ee61L_Ef0FP_R," org.eventb.core.comment="unit hierarchy is not refllexive eg. u ↦ u ∉ UH1" org.eventb.core.label="inv3" org.eventb.core.predicate="UH1 ∩ id = ∅"/>
<org.eventb.core.invariant name="_tdyf0hy0Ee61L_Ef0FP_Q}" org.eventb.core.comment="hierarchy is asymmetric" org.eventb.core.label="inv4" org.eventb.core.predicate="UH1 ∩ UH1∼ = ∅"/>
<org.eventb.core.invariant name="_tdyf0hy0Ee61L_Ef0FP_Q~" org.eventb.core.comment="the hierarchy of a node is unique" org.eventb.core.label="inv5" org.eventb.core.predicate="∀ u1, u2, u3 · (u1 ↦ u2) ∈ UH1 ∧ (u1 ↦ u3) ∈ UH1 ⇒ u2 = u3 " org.eventb.core.theorem="true"/>
<org.eventb.core.invariant name="_tdyf0hy0Ee61L_Ef0FP_R/" org.eventb.core.comment="a unit is mapped to only one organization" org.eventb.core.label="inv7" org.eventb.core.predicate="OU1 ∈ UNIT ⇸ ORG"/>
<org.eventb.core.invariant name="_tdyf0hy0Ee61L_Ef0FP_Q|" org.eventb.core.comment="an organization root is mapped to only one unit" org.eventb.core.label="inv1" org.eventb.core.predicate="root1 ∈ ORG ⇸ dom(OU1)"/>
<org.eventb.core.invariant name="_tdyf0hy0Ee61L_Ef0FP_R3" org.eventb.core.comment="uniqueness of root unit" org.eventb.core.label="inv10" org.eventb.core.predicate="∀org1, org2, u · (org1 ↦ u) ∈ root1 ∧ (org2 ↦ u) ∈ root1 ⇒ org1 = org2"/>
<org.eventb.core.invariant name="_tdyf0hy0Ee61L_Ef0FP_R'" org.eventb.core.comment="a root unit is not subordinated" org.eventb.core.label="inv6" org.eventb.core.predicate="ran(root1) ∩ dom(UH1) = ∅"/>
<org.eventb.core.variable name="_tdyf0hy0Ee61L_Ef0FP_R(" org.eventb.core.identifier="UH1"/>
<org.eventb.core.event name="_tdyf0hy0Ee61L_Ef0FP_R+" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="Add_Unit_Hierarchy">
<org.eventb.core.parameter name="'" org.eventb.core.identifier="u1"/>
<org.eventb.core.parameter name="(" org.eventb.core.identifier="u2"/>
<org.eventb.core.guard name=")" org.eventb.core.label="grd1" org.eventb.core.predicate="u1 ∈ UNIT ∧ u2 ∈ UNIT"/>
<org.eventb.core.action name="+" org.eventb.core.assignment="UH1 ≔ UH1 ∪ {u1 ↦ u2}" org.eventb.core.label="act1"/>
<org.eventb.core.guard name="," org.eventb.core.label="grd3" org.eventb.core.predicate="u1 ∉ dom(UH1)"/>
<org.eventb.core.guard name="0" org.eventb.core.label="grd7" org.eventb.core.predicate="u1 ↦ u2 ∉ UH1"/>
<org.eventb.core.guard name="-" org.eventb.core.label="grd4" org.eventb.core.predicate="u1 ≠ u2"/>
<org.eventb.core.guard name="." org.eventb.core.label="grd5" org.eventb.core.predicate="u2 ↦ u1 ∉ UH1"/>
<org.eventb.core.guard name="/" org.eventb.core.label="grd6" org.eventb.core.predicate="u1 ∉ ran(root1)"/>
<org.eventb.core.guard name="1" org.eventb.core.label="grd8" org.eventb.core.predicate="OU1(u1) = OU1(u2)"/>
<org.eventb.core.guard name="2" org.eventb.core.label="grd9" org.eventb.core.predicate="u1 ∈ dom(OU1) ∧ u2 ∈ dom(OU1) "/>
</org.eventb.core.event>
<org.eventb.core.event name="_tdyf0hy0Ee61L_Ef0FP_R-" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="Assign_Unit_to_Org">
<org.eventb.core.parameter name="'" org.eventb.core.identifier="u"/>
<org.eventb.core.parameter name="(" org.eventb.core.identifier="org"/>
<org.eventb.core.guard name=")" org.eventb.core.label="grd1" org.eventb.core.predicate="u ↦ org ∉ OU1 "/>
<org.eventb.core.action name="*" org.eventb.core.assignment="OU1 ≔ OU1 ∪ {u↦org}" org.eventb.core.label="act1"/>
<org.eventb.core.guard name="+" org.eventb.core.label="grd2" org.eventb.core.predicate="u ∉ dom(OU1)"/>
<org.eventb.core.guard name="," org.eventb.core.label="grd3" org.eventb.core.predicate="u ∈ dom(UH1) ⇒ (OU1[{UH1(u)}] ≠ ∅ ⇒ OU1(UH1(u)) = org)"/>
<org.eventb.core.guard name="-" org.eventb.core.label="grd4" org.eventb.core.predicate="u ∈ ran(UH1) ⇒ (∀ u1 · u1 ↦ u ∈ UH1 ⇒ (OU1[{u1}] ≠ ∅ ⇒ OU1(u1) = org))"/>
</org.eventb.core.event>
<org.eventb.core.variable name="_tdyf0hy0Ee61L_Ef0FP_R." org.eventb.core.identifier="OU1"/>
<org.eventb.core.invariant name="_tdyf0hy0Ee61L_Ef0FP_R1" org.eventb.core.comment="root should belong to the organization" org.eventb.core.label="inv8" org.eventb.core.predicate="∀ u, org · org ↦ u ∈ root1 ⇒ u↦org ∈ OU1"/>
<org.eventb.core.invariant name="_tdyf0hy0Ee61L_Ef0FP_R0" org.eventb.core.comment="the hierarchy belongs to an organization" org.eventb.core.label="inv9" org.eventb.core.predicate="∀us, um · us↦um ∈ UH1 ⇒ (OU1[{us}] ≠ ∅ ∧ OU1[{um}] ≠ ∅ ⇒ OU1(us) = OU1(um))"/>
<org.eventb.core.variable name="_tdyf0hy0Ee61L_Ef0FP_R2" org.eventb.core.identifier="CA"/>
</org.eventb.core.machineFile>