-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathm1_programmes.bcm
140 lines (140 loc) · 37.6 KB
/
m1_programmes.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
<?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">
<org.eventb.core.scRefinesMachine name="'" org.eventb.core.scTarget="/progmanmodel/m0_users.bcm" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.refinesMachine#'"/>
<org.eventb.core.scSeesContext name="(" org.eventb.core.scTarget="/progmanmodel/c1_programmes.bcc" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.seesContext#_c5qNIEHGEeqHd7PiYTbxHg"/>
<org.eventb.core.scInternalContext name="c0_users">
<org.eventb.core.scCarrierSet name="USER" org.eventb.core.source="/progmanmodel/c0_users.buc|org.eventb.core.contextFile#c0_users|org.eventb.core.carrierSet#_swFc0EHSEeqHCPZ-G665YQ" org.eventb.core.type="ℙ(USER)"/>
</org.eventb.core.scInternalContext>
<org.eventb.core.scInternalContext name="c1_programmes">
<org.eventb.core.scExtendsContext name="'" org.eventb.core.scTarget="/progmanmodel/c0_users.bcc|org.eventb.core.scContextFile#c0_users" org.eventb.core.source="/progmanmodel/c1_programmes.buc|org.eventb.core.contextFile#c1_programmes|org.eventb.core.extendsContext#_qcMHkEHSEeqHCPZ-G665YQ"/>
<org.eventb.core.scCarrierSet name="PROGRAMME" org.eventb.core.source="/progmanmodel/c1_programmes.buc|org.eventb.core.contextFile#c1_programmes|org.eventb.core.carrierSet#_qcMuoEHSEeqHCPZ-G665YQ" org.eventb.core.type="ℙ(PROGRAMME)"/>
</org.eventb.core.scInternalContext>
<org.eventb.core.scInvariant name="c0_usert" org.eventb.core.label="inv1" org.eventb.core.predicate="registered⊆USER" org.eventb.core.source="/progmanmodel/m0_users.bum|org.eventb.core.machineFile#m0_users|org.eventb.core.invariant#_QUDCYEHEEeqKzaOTi1o2gg" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="c0_useru" org.eventb.core.label="inv2" org.eventb.core.predicate="logged_in⊆registered" org.eventb.core.source="/progmanmodel/m0_users.bum|org.eventb.core.machineFile#m0_users|org.eventb.core.invariant#_QUDpcEHEEeqKzaOTi1o2gg" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="c1_programmet" org.eventb.core.label="inv11" org.eventb.core.predicate="programmes⊆PROGRAMME" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.invariant#_liiugEHGEeqHd7PiYTbxHg" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="c1_programmeu" org.eventb.core.label="inv12" org.eventb.core.predicate="programme_leader∈programmes → registered" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.invariant#_vOAHMEHGEeqHd7PiYTbxHg" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="c1_programmev" org.eventb.core.label="inv13" org.eventb.core.predicate="administrators∈programmes ↔ registered" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.invariant#_vOAHMUHGEeqHd7PiYTbxHg" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="c1_programmew" org.eventb.core.label="inv14" org.eventb.core.predicate="published⊆programmes" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.invariant#_Uat4UUgQEeqeqbGZOOBkaQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scVariable name="administrators" org.eventb.core.abstract="false" org.eventb.core.concrete="true" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.variable#_vN_gIUHGEeqHd7PiYTbxHg" org.eventb.core.type="ℙ(PROGRAMME×USER)"/>
<org.eventb.core.scVariable name="logged_in" org.eventb.core.abstract="true" org.eventb.core.concrete="true" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.variable#_MTJYwEHEEeqKzaOTi1o2gg" org.eventb.core.type="ℙ(USER)"/>
<org.eventb.core.scVariable name="programme_leader" org.eventb.core.abstract="false" org.eventb.core.concrete="true" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.variable#_vN_gIEHGEeqHd7PiYTbxHg" org.eventb.core.type="ℙ(PROGRAMME×USER)"/>
<org.eventb.core.scVariable name="programmes" org.eventb.core.abstract="false" org.eventb.core.concrete="true" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.variable#_iY418EHGEeqHd7PiYTbxHg" org.eventb.core.type="ℙ(PROGRAMME)"/>
<org.eventb.core.scVariable name="published" org.eventb.core.abstract="false" org.eventb.core.concrete="true" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.variable#_Uat4UEgQEeqeqbGZOOBkaQ" org.eventb.core.type="ℙ(PROGRAMME)"/>
<org.eventb.core.scVariable name="registered" org.eventb.core.abstract="true" org.eventb.core.concrete="true" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.variable#_MTIxsEHEEeqKzaOTi1o2gg" org.eventb.core.type="ℙ(USER)"/>
<org.eventb.core.scEvent name="programme_leades" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="INITIALISATION" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_MTJYwEHEEeqKzaOTi1o2gh">
<org.eventb.core.scRefinesEvent name="'" org.eventb.core.scTarget="/progmanmodel/m0_users.bcm|org.eventb.core.scMachineFile#m0_users|org.eventb.core.scEvent#registeree" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_MTJYwEHEEeqKzaOTi1o2gh"/>
<org.eventb.core.scAction name="'" org.eventb.core.assignment="registered ≔ ∅ ⦂ ℙ(USER)" org.eventb.core.label="act1" org.eventb.core.source="/progmanmodel/m0_users.bum|org.eventb.core.machineFile#m0_users|org.eventb.core.event#'|org.eventb.core.action#_TSDroEHEEeqKzaOTi1o2gg"/>
<org.eventb.core.scAction name="(" org.eventb.core.assignment="logged_in ≔ ∅ ⦂ ℙ(USER)" org.eventb.core.label="act2" org.eventb.core.source="/progmanmodel/m0_users.bum|org.eventb.core.machineFile#m0_users|org.eventb.core.event#'|org.eventb.core.action#_TSESsEHEEeqKzaOTi1o2gg"/>
<org.eventb.core.scAction name=")" org.eventb.core.assignment="programmes ≔ ∅ ⦂ ℙ(PROGRAMME)" org.eventb.core.label="act11" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_MTJYwEHEEeqKzaOTi1o2gh|org.eventb.core.action#_0s5_4EHGEeqHd7PiYTbxHg"/>
<org.eventb.core.scAction name="*" org.eventb.core.assignment="programme_leader ≔ ∅ ⦂ ℙ(PROGRAMME×USER)" org.eventb.core.label="act12" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_MTJYwEHEEeqKzaOTi1o2gh|org.eventb.core.action#_0s5_4UHGEeqHd7PiYTbxHg"/>
<org.eventb.core.scAction name="+" org.eventb.core.assignment="administrators ≔ ∅ ⦂ ℙ(PROGRAMME×USER)" org.eventb.core.label="act13" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_MTJYwEHEEeqKzaOTi1o2gh|org.eventb.core.action#_0s5_4kHGEeqHd7PiYTbxHg"/>
<org.eventb.core.scAction name="," org.eventb.core.assignment="published ≔ ∅ ⦂ ℙ(PROGRAMME)" org.eventb.core.label="act14" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_MTJYwEHEEeqKzaOTi1o2gh|org.eventb.core.action#_3ZnrMEgQEeqeqbGZOOBkaQ"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="programme_leadet" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="publish_programme" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_gpYtQEgTEeqeqbGZOOBkaQ">
<org.eventb.core.scGuard name="'" org.eventb.core.label="grd1" org.eventb.core.predicate="u∈logged_in" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_gpYtQEgTEeqeqbGZOOBkaQ|org.eventb.core.guard#_JVqzoEHHEeqHd7PiYTbxHg" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="(" org.eventb.core.label="grd2" org.eventb.core.predicate="p∈programmes" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_gpYtQEgTEeqeqbGZOOBkaQ|org.eventb.core.guard#_JVqzoUHHEeqHd7PiYTbxHg" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name=")" org.eventb.core.label="grd3" org.eventb.core.predicate="u=programme_leader(p)" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_gpYtQEgTEeqeqbGZOOBkaQ|org.eventb.core.guard#_JVqzokHHEeqHd7PiYTbxHg" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="*" org.eventb.core.label="grd4" org.eventb.core.predicate="p∉published" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_gpYtQEgTEeqeqbGZOOBkaQ|org.eventb.core.guard#_sioQokHHEeqHd7PiYTbxHg" org.eventb.core.theorem="false"/>
<org.eventb.core.scParameter name="p" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_gpYtQEgTEeqeqbGZOOBkaQ|org.eventb.core.parameter#_JVqMkkHHEeqHd7PiYTbxHg" org.eventb.core.type="PROGRAMME"/>
<org.eventb.core.scParameter name="u" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_gpYtQEgTEeqeqbGZOOBkaQ|org.eventb.core.parameter#_JVqMkUHHEeqHd7PiYTbxHg" org.eventb.core.type="USER"/>
<org.eventb.core.scAction name="v" org.eventb.core.assignment="published ≔ published∪{p}" org.eventb.core.label="act1" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_gpYtQEgTEeqeqbGZOOBkaQ|org.eventb.core.action#_JVrasEHHEeqHd7PiYTbxHg"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="programme_leadeu" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="unpublish_programme" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_gpaicEgTEeqeqbGZOOBkaQ">
<org.eventb.core.scGuard name="'" org.eventb.core.label="grd1" org.eventb.core.predicate="u∈logged_in" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_gpaicEgTEeqeqbGZOOBkaQ|org.eventb.core.guard#_g_lrQEHHEeqHd7PiYTbxHg" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="(" org.eventb.core.label="grd2" org.eventb.core.predicate="p∈programmes" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_gpaicEgTEeqeqbGZOOBkaQ|org.eventb.core.guard#_g_mSUEHHEeqHd7PiYTbxHg" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name=")" org.eventb.core.label="grd3" org.eventb.core.predicate="u=programme_leader(p)" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_gpaicEgTEeqeqbGZOOBkaQ|org.eventb.core.guard#_g_mSUUHHEeqHd7PiYTbxHg" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="*" org.eventb.core.label="grd4" org.eventb.core.predicate="p∈published" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_gpaicEgTEeqeqbGZOOBkaQ|org.eventb.core.guard#_3BElcEHHEeqHd7PiYTbxHg" org.eventb.core.theorem="false"/>
<org.eventb.core.scParameter name="p" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_gpaicEgTEeqeqbGZOOBkaQ|org.eventb.core.parameter#_ROOEQEHHEeqHd7PiYTbxHg" org.eventb.core.type="PROGRAMME"/>
<org.eventb.core.scParameter name="u" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_gpaicEgTEeqeqbGZOOBkaQ|org.eventb.core.parameter#_RONdMEHHEeqHd7PiYTbxHg" org.eventb.core.type="USER"/>
<org.eventb.core.scAction name="v" org.eventb.core.assignment="published ≔ published ∖ {p}" org.eventb.core.label="act1" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_gpaicEgTEeqeqbGZOOBkaQ|org.eventb.core.action#_g_m5YEHHEeqHd7PiYTbxHg"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="programme_leadev" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="create_programme" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVqMkEHHEeqHd7PiYTbxHg">
<org.eventb.core.scGuard name="'" org.eventb.core.label="grd1" org.eventb.core.predicate="u∈logged_in" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVqMkEHHEeqHd7PiYTbxHg|org.eventb.core.guard#_sinpkUHHEeqHd7PiYTbxHg" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="(" org.eventb.core.label="grd2" org.eventb.core.predicate="p∈PROGRAMME" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVqMkEHHEeqHd7PiYTbxHg|org.eventb.core.guard#_sioQoEHHEeqHd7PiYTbxHg" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name=")" org.eventb.core.label="grd3" org.eventb.core.predicate="p∉programmes" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVqMkEHHEeqHd7PiYTbxHg|org.eventb.core.guard#_sioQoUHHEeqHd7PiYTbxHg" org.eventb.core.theorem="false"/>
<org.eventb.core.scParameter name="p" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVqMkEHHEeqHd7PiYTbxHg|org.eventb.core.parameter#_sinpkEHHEeqHd7PiYTbxHg" org.eventb.core.type="PROGRAMME"/>
<org.eventb.core.scParameter name="u" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVqMkEHHEeqHd7PiYTbxHg|org.eventb.core.parameter#_gpeM0EgTEeqeqbGZOOBkaQ" org.eventb.core.type="USER"/>
<org.eventb.core.scAction name="v" org.eventb.core.assignment="programmes ≔ programmes∪{p}" org.eventb.core.label="act1" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVqMkEHHEeqHd7PiYTbxHg|org.eventb.core.action#_x9OREEHHEeqHd7PiYTbxHg"/>
<org.eventb.core.scAction name="w" org.eventb.core.assignment="programme_leader ≔ programme_leader{p ↦ u}" org.eventb.core.label="act2" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVqMkEHHEeqHd7PiYTbxHg|org.eventb.core.action#_JVrasUHHEeqHd7PiYTbxHg"/>
<org.eventb.core.scAction name="x" org.eventb.core.assignment="administrators ≔ administrators∪{p ↦ u}" org.eventb.core.label="act3" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVqMkEHHEeqHd7PiYTbxHg|org.eventb.core.action#_ROM2IEHHEeqHd7PiYTbxHg"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="programme_leadew" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="delete_programme" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVsBwEHHEeqHd7PiYTbxHg">
<org.eventb.core.scGuard name="'" org.eventb.core.label="grd1" org.eventb.core.predicate="u∈logged_in" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVsBwEHHEeqHd7PiYTbxHg|org.eventb.core.guard#_3BD-YEHHEeqHd7PiYTbxHg" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="(" org.eventb.core.label="grd2" org.eventb.core.predicate="p∈programmes" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVsBwEHHEeqHd7PiYTbxHg|org.eventb.core.guard#_3BD-YUHHEeqHd7PiYTbxHg" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name=")" org.eventb.core.label="grd3" org.eventb.core.predicate="programme_leader(p)=u" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVsBwEHHEeqHd7PiYTbxHg|org.eventb.core.guard#_3BD-YkHHEeqHd7PiYTbxHg" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="*" org.eventb.core.label="grd4" org.eventb.core.predicate="p∉published" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVsBwEHHEeqHd7PiYTbxHg|org.eventb.core.guard#_7nL08UHHEeqHd7PiYTbxHg" org.eventb.core.theorem="false"/>
<org.eventb.core.scParameter name="p" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVsBwEHHEeqHd7PiYTbxHg|org.eventb.core.parameter#_3BDXUkHHEeqHd7PiYTbxHg" org.eventb.core.type="PROGRAMME"/>
<org.eventb.core.scParameter name="u" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVsBwEHHEeqHd7PiYTbxHg|org.eventb.core.parameter#_oWwBkEgTEeqeqbGZOOBkaQ" org.eventb.core.type="USER"/>
<org.eventb.core.scAction name="v" org.eventb.core.assignment="programmes ≔ programmes ∖ {p}" org.eventb.core.label="act1" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVsBwEHHEeqHd7PiYTbxHg|org.eventb.core.action#_3BFMgEHHEeqHd7PiYTbxHg"/>
<org.eventb.core.scAction name="w" org.eventb.core.assignment="programme_leader ≔ {p} ⩤ programme_leader" org.eventb.core.label="act2" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVsBwEHHEeqHd7PiYTbxHg|org.eventb.core.action#_g_m5YUHHEeqHd7PiYTbxHg"/>
<org.eventb.core.scAction name="x" org.eventb.core.assignment="administrators ≔ {p} ⩤ administrators" org.eventb.core.label="act3" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVsBwEHHEeqHd7PiYTbxHg|org.eventb.core.action#_g_ngcEHHEeqHd7PiYTbxHg"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="programme_leadex" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="add_administrator" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVsBwUHHEeqHd7PiYTbxHg">
<org.eventb.core.scGuard name="'" org.eventb.core.label="grd1" org.eventb.core.predicate="u1∈logged_in" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVsBwUHHEeqHd7PiYTbxHg|org.eventb.core.guard#_7nLN4UHHEeqHd7PiYTbxHg" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="(" org.eventb.core.label="grd2" org.eventb.core.predicate="u2∈registered" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVsBwUHHEeqHd7PiYTbxHg|org.eventb.core.guard#_7nLN4kHHEeqHd7PiYTbxHg" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name=")" org.eventb.core.label="grd3" org.eventb.core.predicate="p∈programmes" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVsBwUHHEeqHd7PiYTbxHg|org.eventb.core.guard#_7nL08EHHEeqHd7PiYTbxHg" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="*" org.eventb.core.label="grd4" org.eventb.core.predicate="programme_leader(p)=u1" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVsBwUHHEeqHd7PiYTbxHg|org.eventb.core.guard#_gpmIoEgTEeqeqbGZOOBkaQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="+" org.eventb.core.label="grd5" org.eventb.core.predicate="u2∉administrators[{p}]" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVsBwUHHEeqHd7PiYTbxHg|org.eventb.core.guard#_sio3sEHHEeqHd7PiYTbxHg" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="," org.eventb.core.label="grd6" org.eventb.core.predicate="p∉published" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVsBwUHHEeqHd7PiYTbxHg|org.eventb.core.guard#_cDwN8EHIEeqHd7PiYTbxHg" org.eventb.core.theorem="false"/>
<org.eventb.core.scParameter name="p" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVsBwUHHEeqHd7PiYTbxHg|org.eventb.core.parameter#_7nLN4EHHEeqHd7PiYTbxHg" org.eventb.core.type="PROGRAMME"/>
<org.eventb.core.scParameter name="u1" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVsBwUHHEeqHd7PiYTbxHg|org.eventb.core.parameter#_sinCgEHHEeqHd7PiYTbxHg" org.eventb.core.type="USER"/>
<org.eventb.core.scParameter name="u2" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVsBwUHHEeqHd7PiYTbxHg|org.eventb.core.parameter#_sinCgUHHEeqHd7PiYTbxHg" org.eventb.core.type="USER"/>
<org.eventb.core.scAction name="u3" org.eventb.core.assignment="administrators ≔ administrators∪{p ↦ u2}" org.eventb.core.label="act1" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVsBwUHHEeqHd7PiYTbxHg|org.eventb.core.action#_7nMcAUHHEeqHd7PiYTbxHg"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="programme_leadey" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="remove_administrator" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVsBwkHHEeqHd7PiYTbxHg">
<org.eventb.core.scGuard name="'" org.eventb.core.label="grd1" org.eventb.core.predicate="u1∈logged_in" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVsBwkHHEeqHd7PiYTbxHg|org.eventb.core.guard#_gpk6gEgTEeqeqbGZOOBkaQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="(" org.eventb.core.label="grd2" org.eventb.core.predicate="u2∈registered" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVsBwkHHEeqHd7PiYTbxHg|org.eventb.core.guard#_gplhkEgTEeqeqbGZOOBkaQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name=")" org.eventb.core.label="grd3" org.eventb.core.predicate="p∈programmes" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVsBwkHHEeqHd7PiYTbxHg|org.eventb.core.guard#_gplhkUgTEeqeqbGZOOBkaQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="*" org.eventb.core.label="grd4" org.eventb.core.predicate="programme_leader(p)=u1" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVsBwkHHEeqHd7PiYTbxHg|org.eventb.core.guard#_oW1hIkgTEeqeqbGZOOBkaQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="+" org.eventb.core.label="grd5" org.eventb.core.predicate="u2∈administrators[{p}]" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVsBwkHHEeqHd7PiYTbxHg|org.eventb.core.guard#_3BElcUHHEeqHd7PiYTbxHg" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="," org.eventb.core.label="grd6" org.eventb.core.predicate="u1≠u2" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVsBwkHHEeqHd7PiYTbxHg|org.eventb.core.guard#_eZxgUEc9EeqCJoBEKqsuQA" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="-" org.eventb.core.label="grd7" org.eventb.core.predicate="p∉published" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVsBwkHHEeqHd7PiYTbxHg|org.eventb.core.guard#_WXhJ8EgVEeqeqbGZOOBkaQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scParameter name="p" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVsBwkHHEeqHd7PiYTbxHg|org.eventb.core.parameter#_gpmvsEgTEeqeqbGZOOBkaQ" org.eventb.core.type="PROGRAMME"/>
<org.eventb.core.scParameter name="u1" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVsBwkHHEeqHd7PiYTbxHg|org.eventb.core.parameter#_3BDXUEHHEeqHd7PiYTbxHg" org.eventb.core.type="USER"/>
<org.eventb.core.scParameter name="u2" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVsBwkHHEeqHd7PiYTbxHg|org.eventb.core.parameter#_3BDXUUHHEeqHd7PiYTbxHg" org.eventb.core.type="USER"/>
<org.eventb.core.scAction name="u3" org.eventb.core.assignment="administrators ≔ administrators ∖ {p ↦ u2}" org.eventb.core.label="act1" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVsBwkHHEeqHd7PiYTbxHg|org.eventb.core.action#_gpmvsUgTEeqeqbGZOOBkaQ"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="programme_leadez" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="transfer_ownership" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVso0EHHEeqHd7PiYTbxHg">
<org.eventb.core.scGuard name="'" org.eventb.core.label="grd1" org.eventb.core.predicate="u1∈logged_in" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVso0EHHEeqHd7PiYTbxHg|org.eventb.core.guard#_oW06EEgTEeqeqbGZOOBkaQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="(" org.eventb.core.label="grd2" org.eventb.core.predicate="u2∈registered" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVso0EHHEeqHd7PiYTbxHg|org.eventb.core.guard#_oW1hIEgTEeqeqbGZOOBkaQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name=")" org.eventb.core.label="grd3" org.eventb.core.predicate="p∈programmes" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVso0EHHEeqHd7PiYTbxHg|org.eventb.core.guard#_oW1hIUgTEeqeqbGZOOBkaQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="*" org.eventb.core.label="grd4" org.eventb.core.predicate="programme_leader(p)=u1" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVso0EHHEeqHd7PiYTbxHg|org.eventb.core.guard#_aUM3YEgUEeqeqbGZOOBkaQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="+" org.eventb.core.label="grd5" org.eventb.core.predicate="u2∈administrators[{p}]" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVso0EHHEeqHd7PiYTbxHg|org.eventb.core.guard#_7nMcAEHHEeqHd7PiYTbxHg" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="," org.eventb.core.label="grd6" org.eventb.core.predicate="u1≠u2" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVso0EHHEeqHd7PiYTbxHg|org.eventb.core.guard#_bx1dkEgVEeqeqbGZOOBkaQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="-" org.eventb.core.label="grd7" org.eventb.core.predicate="p∉published" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVso0EHHEeqHd7PiYTbxHg|org.eventb.core.guard#_bx1dkUgVEeqeqbGZOOBkaQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scParameter name="p" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVso0EHHEeqHd7PiYTbxHg|org.eventb.core.parameter#_oW2IMEgTEeqeqbGZOOBkaQ" org.eventb.core.type="PROGRAMME"/>
<org.eventb.core.scParameter name="u1" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVso0EHHEeqHd7PiYTbxHg|org.eventb.core.parameter#_7nKm0EHHEeqHd7PiYTbxHg" org.eventb.core.type="USER"/>
<org.eventb.core.scParameter name="u2" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVso0EHHEeqHd7PiYTbxHg|org.eventb.core.parameter#_7nKm0UHHEeqHd7PiYTbxHg" org.eventb.core.type="USER"/>
<org.eventb.core.scAction name="u3" org.eventb.core.assignment="programme_leader ≔ programme_leader{p ↦ u2}" org.eventb.core.label="act1" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVso0EHHEeqHd7PiYTbxHg|org.eventb.core.action#_oW2IMUgTEeqeqbGZOOBkaQ"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="programme_leade{" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="register" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_MTJYwEHEEeqKzaOTi1o2gi">
<org.eventb.core.scRefinesEvent name="'" org.eventb.core.scTarget="/progmanmodel/m0_users.bcm|org.eventb.core.scMachineFile#m0_users|org.eventb.core.scEvent#registeref" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_MTJYwEHEEeqKzaOTi1o2gi|org.eventb.core.refinesEvent#'"/>
<org.eventb.core.scGuard name="'" org.eventb.core.label="grd1" org.eventb.core.predicate="u∈USER" org.eventb.core.source="/progmanmodel/m0_users.bum|org.eventb.core.machineFile#m0_users|org.eventb.core.event#_GnKGUEHEEeqKzaOTi1o2gg|org.eventb.core.guard#_eQiLYUHEEeqKzaOTi1o2gg" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="(" org.eventb.core.label="grd2" org.eventb.core.predicate="u∉registered" org.eventb.core.source="/progmanmodel/m0_users.bum|org.eventb.core.machineFile#m0_users|org.eventb.core.event#_GnKGUEHEEeqKzaOTi1o2gg|org.eventb.core.guard#_eQiycEHEEeqKzaOTi1o2gg" org.eventb.core.theorem="false"/>
<org.eventb.core.scAction name="v" org.eventb.core.assignment="registered ≔ registered∪{u}" org.eventb.core.label="act1" org.eventb.core.source="/progmanmodel/m0_users.bum|org.eventb.core.machineFile#m0_users|org.eventb.core.event#_GnKGUEHEEeqKzaOTi1o2gg|org.eventb.core.action#_eQiycUHEEeqKzaOTi1o2gg"/>
<org.eventb.core.scParameter name="u" org.eventb.core.source="/progmanmodel/m0_users.bum|org.eventb.core.machineFile#m0_users|org.eventb.core.event#_GnKGUEHEEeqKzaOTi1o2gg|org.eventb.core.parameter#_eQiLYEHEEeqKzaOTi1o2gg" org.eventb.core.type="USER"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="programme_leade|" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="unregister" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_MTJYwEHEEeqKzaOTi1o2gj">
<org.eventb.core.scRefinesEvent name="'" org.eventb.core.scTarget="/progmanmodel/m0_users.bcm|org.eventb.core.scMachineFile#m0_users|org.eventb.core.scEvent#registereg" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_MTJYwEHEEeqKzaOTi1o2gj|org.eventb.core.refinesEvent#'"/>
<org.eventb.core.scGuard name="'" org.eventb.core.label="grd1" org.eventb.core.predicate="u∈registered" org.eventb.core.source="/progmanmodel/m0_users.bum|org.eventb.core.machineFile#m0_users|org.eventb.core.event#_GnKtYEHEEeqKzaOTi1o2gg|org.eventb.core.guard#_eQjZgUHEEeqKzaOTi1o2gg" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="(" org.eventb.core.label="grd2" org.eventb.core.predicate="u∉logged_in" org.eventb.core.source="/progmanmodel/m0_users.bum|org.eventb.core.machineFile#m0_users|org.eventb.core.event#_GnKtYEHEEeqKzaOTi1o2gg|org.eventb.core.guard#_eQkAkEHEEeqKzaOTi1o2gg" org.eventb.core.theorem="false"/>
<org.eventb.core.scAction name="v" org.eventb.core.assignment="registered ≔ registered ∖ {u}" org.eventb.core.label="act1" org.eventb.core.source="/progmanmodel/m0_users.bum|org.eventb.core.machineFile#m0_users|org.eventb.core.event#_GnKtYEHEEeqKzaOTi1o2gg|org.eventb.core.action#_eQknoEHEEeqKzaOTi1o2gg"/>
<org.eventb.core.scParameter name="u" org.eventb.core.source="/progmanmodel/m0_users.bum|org.eventb.core.machineFile#m0_users|org.eventb.core.event#_GnKtYEHEEeqKzaOTi1o2gg|org.eventb.core.parameter#_eQjZgEHEEeqKzaOTi1o2gg" org.eventb.core.type="USER"/>
<org.eventb.core.scGuard name="w" org.eventb.core.label="grd11" org.eventb.core.predicate="u∉ran(programme_leader)" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_MTJYwEHEEeqKzaOTi1o2gj|org.eventb.core.guard#_CWPG4EHIEeqHd7PiYTbxHg" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="x" org.eventb.core.label="grd12" org.eventb.core.predicate="u∉ran(administrators)" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_MTJYwEHEEeqKzaOTi1o2gj|org.eventb.core.guard#_CWPG4UHIEeqHd7PiYTbxHg" org.eventb.core.theorem="false"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="programme_leade}" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="login" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_MTJYwEHEEeqKzaOTi1o2gk">
<org.eventb.core.scRefinesEvent name="'" org.eventb.core.scTarget="/progmanmodel/m0_users.bcm|org.eventb.core.scMachineFile#m0_users|org.eventb.core.scEvent#registereh" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_MTJYwEHEEeqKzaOTi1o2gk|org.eventb.core.refinesEvent#'"/>
<org.eventb.core.scGuard name="'" org.eventb.core.label="grd1" org.eventb.core.predicate="u∈registered" org.eventb.core.source="/progmanmodel/m0_users.bum|org.eventb.core.machineFile#m0_users|org.eventb.core.event#_GnL7gEHEEeqKzaOTi1o2gg|org.eventb.core.guard#_iqZHkUHEEeqKzaOTi1o2gg" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="(" org.eventb.core.label="grd2" org.eventb.core.predicate="u∉logged_in" org.eventb.core.source="/progmanmodel/m0_users.bum|org.eventb.core.machineFile#m0_users|org.eventb.core.event#_GnL7gEHEEeqKzaOTi1o2gg|org.eventb.core.guard#_iqZuoEHEEeqKzaOTi1o2gg" org.eventb.core.theorem="false"/>
<org.eventb.core.scAction name="v" org.eventb.core.assignment="logged_in ≔ logged_in∪{u}" org.eventb.core.label="act1" org.eventb.core.source="/progmanmodel/m0_users.bum|org.eventb.core.machineFile#m0_users|org.eventb.core.event#_GnL7gEHEEeqKzaOTi1o2gg|org.eventb.core.action#_iqZuoUHEEeqKzaOTi1o2gg"/>
<org.eventb.core.scParameter name="u" org.eventb.core.source="/progmanmodel/m0_users.bum|org.eventb.core.machineFile#m0_users|org.eventb.core.event#_GnL7gEHEEeqKzaOTi1o2gg|org.eventb.core.parameter#_iqZHkEHEEeqKzaOTi1o2gg" org.eventb.core.type="USER"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="programme_leade~" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="logout" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_MTJYwEHEEeqKzaOTi1o2gl">
<org.eventb.core.scRefinesEvent name="'" org.eventb.core.scTarget="/progmanmodel/m0_users.bcm|org.eventb.core.scMachineFile#m0_users|org.eventb.core.scEvent#registerei" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_MTJYwEHEEeqKzaOTi1o2gl|org.eventb.core.refinesEvent#'"/>
<org.eventb.core.scGuard name="'" org.eventb.core.label="grd1" org.eventb.core.predicate="u∈registered" org.eventb.core.source="/progmanmodel/m0_users.bum|org.eventb.core.machineFile#m0_users|org.eventb.core.event#_GnMikEHEEeqKzaOTi1o2gg|org.eventb.core.guard#_iqaVsUHEEeqKzaOTi1o2gg" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="(" org.eventb.core.label="grd2" org.eventb.core.predicate="u∈logged_in" org.eventb.core.source="/progmanmodel/m0_users.bum|org.eventb.core.machineFile#m0_users|org.eventb.core.event#_GnMikEHEEeqKzaOTi1o2gg|org.eventb.core.guard#_iqaVskHEEeqKzaOTi1o2gg" org.eventb.core.theorem="false"/>
<org.eventb.core.scAction name="v" org.eventb.core.assignment="logged_in ≔ logged_in ∖ {u}" org.eventb.core.label="act1" org.eventb.core.source="/progmanmodel/m0_users.bum|org.eventb.core.machineFile#m0_users|org.eventb.core.event#_GnMikEHEEeqKzaOTi1o2gg|org.eventb.core.action#_iqa8wEHEEeqKzaOTi1o2gg"/>
<org.eventb.core.scParameter name="u" org.eventb.core.source="/progmanmodel/m0_users.bum|org.eventb.core.machineFile#m0_users|org.eventb.core.event#_GnMikEHEEeqKzaOTi1o2gg|org.eventb.core.parameter#_iqaVsEHEEeqKzaOTi1o2gg" org.eventb.core.type="USER"/>
</org.eventb.core.scEvent>
</org.eventb.core.scMachineFile>