-
Notifications
You must be signed in to change notification settings - Fork 0
/
m3_outcomes.bum
169 lines (169 loc) · 28.3 KB
/
m3_outcomes.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
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<org.eventb.core.machineFile org.eventb.core.configuration="org.eventb.core.fwd" org.eventb.core.generated="false" org.eventb.texttools.text_lastmodified="1584531918212" org.eventb.texttools.text_representation="machine m3_outcomes refines m2_modules sees c3_outcomes variables registered logged_in programmes programme_leader administrators modules contains_module module_leader module_outcomes programme_outcomes outcome_mapping credits_awarded published invariants @inv31 programme_outcomes ∈ programmes ↔ P_OUTCOME @inv32 module_outcomes ∈ modules ↔ M_OUTCOME @inv33 outcome_mapping ∈ module_outcomes ↔ programme_outcomes @inv34 ∀m · m ∈ dom(dom(outcome_mapping)) ⇒ dom(ran(({m} ◁ dom(outcome_mapping)) ◁outcome_mapping)) ⊆ contains_module∼[{m}] events event INITIALISATION extends INITIALISATION then @act31 programme_outcomes ≔ ∅ @act32 module_outcomes ≔ ∅ @act33 outcome_mapping ≔ ∅ end event assign_programme_outcome any u p o where @grd1 u ∈ logged_in @grd2 p ∈ programmes @grd3 o ∈ P_OUTCOME @grd4 u ∈ administrators[{p}] @grd5 o ∉ programme_outcomes[{p}] @grd6 p ∉ published then @act1 programme_outcomes ≔ programme_outcomes ∪ {p↦o} end event unassign_programme_outcome any u p o where @grd1 u ∈ logged_in @grd2 p ∈ programmes @grd3 o ∈ P_OUTCOME @grd4 u ∈ administrators[{p}] @grd5 o ∈ programme_outcomes[{p}] @grd6 p ∉ published then @act1 programme_outcomes ≔ programme_outcomes ∖ {p↦o} @act2 outcome_mapping ≔ outcome_mapping ⩥ (ran(outcome_mapping) ▷ {o}) end event assign_module_outcome any u m o where @grd1 u ∈ logged_in @grd2 m ∈ modules @grd3 o ∈ M_OUTCOME @grd4 u = module_leader(m) @grd5 o ∉ module_outcomes[{m}] @grd6 m ∉ contains_module[published] then @act1 module_outcomes ≔ module_outcomes ∪ {m↦o} end event unassign_module_outcome any u m o where @grd1 u ∈ logged_in @grd2 m ∈ modules @grd3 o ∈ M_OUTCOME @grd4 u = module_leader(m) @grd5 o ∈ module_outcomes[{m}] @grd6 m ∉ contains_module[published] then @act1 module_outcomes ≔ module_outcomes ∖ {m↦o} @act2 outcome_mapping ≔ (dom(outcome_mapping) ▷ {o}) ⩤ outcome_mapping end event map_outcome any u p po m mo where @grd1 u ∈ logged_in @grd2 p ∈ programmes @grd3 po ∈ P_OUTCOME @grd4 m ∈ modules @grd5 mo ∈ M_OUTCOME @grd6 m ∈ contains_module[{p}] @grd7 u ∈ administrators[{p}] @grd8 po ∈ programme_outcomes[{p}] @grd9 mo ∈ module_outcomes[{m}] @grd10 (m↦mo)↦ (p↦po) ∉ outcome_mapping @grd11 p ∉ published then @act1 outcome_mapping ≔ outcome_mapping ∪ {(m↦mo)↦ (p↦po)} end event unmap_outcome any u p po m mo where @grd1 u ∈ logged_in @grd2 p ∈ programmes @grd3 po ∈ P_OUTCOME @grd4 m ∈ modules @grd5 mo ∈ M_OUTCOME @grd6 m ∈ contains_module[{p}] @grd7 u ∈ administrators[{p}] @grd8 po ∈ programme_outcomes[{p}] @grd9 mo ∈ module_outcomes[{m}] @grd10 (m↦mo)↦ (p↦po) ∈ outcome_mapping @grd11 p ∉ published then @act1 outcome_mapping ≔ outcome_mapping ∖ {(m↦mo)↦ (p↦po)} end event publish_programme extends publish_programme where @grd31 ∀po · po ∈ programme_outcomes[{p}] ⇒ outcome_mapping ▷ {p↦po} ≠ ∅ end event unpublish_programme extends unpublish_programme end event create_module extends create_module end event delete_module extends delete_module then @act31 outcome_mapping ≔ ({m}◁module_outcomes) ⩤ outcome_mapping @act32 module_outcomes ≔ {m} ⩤ module_outcomes end event assign_module extends assign_module end event unassign_module extends unassign_module then @act31 outcome_mapping ≔ outcome_mapping ∖ ((({m} ◁ dom(outcome_mapping)) ◁ outcome_mapping) ▷ ({p}◁ran(outcome_mapping))) end event transfer_module_ownership extends transfer_module_ownership end event create_programme extends create_programme end event delete_programme extends delete_programme then @act31 outcome_mapping ≔ outcome_mapping ⩥ ({p}◁ran(outcome_mapping)) @act32 programme_outcomes ≔ {p} ⩤ programme_outcomes end event add_administrator extends add_administrator end event remove_administrator extends remove_administrator end event transfer_ownership extends transfer_ownership end event register extends register end event unregister extends unregister end event login extends login end event logout extends logout end end " version="5">
<org.eventb.core.refinesMachine name="'" org.eventb.core.target="m2_modules"/>
<org.eventb.core.seesContext name="_ksZoUEHUEeqHCPZ-G665YQ" org.eventb.core.target="c3_outcomes"/>
<org.eventb.core.variable name="_MTIxsEHEEeqKzaOTi1o2gg" org.eventb.core.generated="false" org.eventb.core.identifier="registered"/>
<org.eventb.core.variable name="_MTJYwEHEEeqKzaOTi1o2gg" org.eventb.core.generated="false" org.eventb.core.identifier="logged_in"/>
<org.eventb.core.variable name="_iY418EHGEeqHd7PiYTbxHg" org.eventb.core.generated="false" org.eventb.core.identifier="programmes"/>
<org.eventb.core.variable name="_vN_gIEHGEeqHd7PiYTbxHg" org.eventb.core.generated="false" org.eventb.core.identifier="programme_leader"/>
<org.eventb.core.variable name="_vN_gIUHGEeqHd7PiYTbxHg" org.eventb.core.generated="false" org.eventb.core.identifier="administrators"/>
<org.eventb.core.variable name="_AGHB4EHJEeqHd7PiYTbxHg" org.eventb.core.generated="false" org.eventb.core.identifier="modules"/>
<org.eventb.core.variable name="_AGHB4UHJEeqHd7PiYTbxHg" org.eventb.core.generated="false" org.eventb.core.identifier="contains_module"/>
<org.eventb.core.variable name="_AGHo8EHJEeqHd7PiYTbxHg" org.eventb.core.generated="false" org.eventb.core.identifier="module_leader"/>
<org.eventb.core.event name="_vN_gIUHGEeqHd7PiYTbxHh" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.generated="false" org.eventb.core.label="INITIALISATION">
<org.eventb.core.action name="_StTwEEHVEeqHCPZ-G665YQ" org.eventb.core.assignment="programme_outcomes ≔ ∅" org.eventb.core.generated="false" org.eventb.core.label="act31"/>
<org.eventb.core.action name="_StTwEUHVEeqHCPZ-G665YQ" org.eventb.core.assignment="module_outcomes ≔ ∅" org.eventb.core.generated="false" org.eventb.core.label="act32"/>
<org.eventb.core.action name="_StTwEkHVEeqHCPZ-G665YQ" org.eventb.core.assignment="outcome_mapping ≔ ∅" org.eventb.core.generated="false" org.eventb.core.label="act33"/>
</org.eventb.core.event>
<org.eventb.core.event name="_WOilsEHWEeqHCPZ-G665YQ" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.generated="false" org.eventb.core.label="assign_programme_outcome">
<org.eventb.core.parameter name="_WOjMwEHWEeqHCPZ-G665YQ" org.eventb.core.generated="false" org.eventb.core.identifier="u"/>
<org.eventb.core.parameter name="_WOjMwUHWEeqHCPZ-G665YQ" org.eventb.core.generated="false" org.eventb.core.identifier="p"/>
<org.eventb.core.parameter name="_WOjMwkHWEeqHCPZ-G665YQ" org.eventb.core.generated="false" org.eventb.core.identifier="o"/>
<org.eventb.core.guard name="_WOjMw0HWEeqHCPZ-G665YQ" org.eventb.core.generated="false" org.eventb.core.label="grd1" org.eventb.core.predicate="u ∈ logged_in"/>
<org.eventb.core.guard name="_WOka4EHWEeqHCPZ-G665YQ" org.eventb.core.generated="false" org.eventb.core.label="grd2" org.eventb.core.predicate="p ∈ programmes"/>
<org.eventb.core.guard name="_WOka4UHWEeqHCPZ-G665YQ" org.eventb.core.generated="false" org.eventb.core.label="grd3" org.eventb.core.predicate="o ∈ P_OUTCOME"/>
<org.eventb.core.guard name="_WOlB8EHWEeqHCPZ-G665YQ" org.eventb.core.generated="false" org.eventb.core.label="grd4" org.eventb.core.predicate="u ∈ administrators[{p}]"/>
<org.eventb.core.guard name="_WOlB8UHWEeqHCPZ-G665YQ" org.eventb.core.generated="false" org.eventb.core.label="grd5" org.eventb.core.predicate="o ∉ programme_outcomes[{p}]"/>
<org.eventb.core.action name="_WOlB8kHWEeqHCPZ-G665YQ" org.eventb.core.assignment="programme_outcomes ≔ programme_outcomes ∪ {p↦o}" org.eventb.core.generated="false" org.eventb.core.label="act1"/>
<org.eventb.core.guard name="_q4AGQEgnEeqeqbGZOOBkaQ" org.eventb.core.generated="false" org.eventb.core.label="grd6" org.eventb.core.predicate="p ∉ published"/>
</org.eventb.core.event>
<org.eventb.core.event name="_WOlB80HWEeqHCPZ-G665YQ" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.generated="false" org.eventb.core.label="unassign_programme_outcome">
<org.eventb.core.parameter name="_WOlpAEHWEeqHCPZ-G665YQ" org.eventb.core.generated="false" org.eventb.core.identifier="u"/>
<org.eventb.core.parameter name="_WOlpAUHWEeqHCPZ-G665YQ" org.eventb.core.generated="false" org.eventb.core.identifier="p"/>
<org.eventb.core.parameter name="_WOmQEEHWEeqHCPZ-G665YQ" org.eventb.core.generated="false" org.eventb.core.identifier="o"/>
<org.eventb.core.guard name="_WOmQEUHWEeqHCPZ-G665YQ" org.eventb.core.generated="false" org.eventb.core.label="grd1" org.eventb.core.predicate="u ∈ logged_in"/>
<org.eventb.core.guard name="_WOmQEkHWEeqHCPZ-G665YQ" org.eventb.core.generated="false" org.eventb.core.label="grd2" org.eventb.core.predicate="p ∈ programmes"/>
<org.eventb.core.guard name="_WOm3IEHWEeqHCPZ-G665YQ" org.eventb.core.generated="false" org.eventb.core.label="grd3" org.eventb.core.predicate="o ∈ P_OUTCOME"/>
<org.eventb.core.guard name="_WOm3IUHWEeqHCPZ-G665YQ" org.eventb.core.generated="false" org.eventb.core.label="grd4" org.eventb.core.predicate="u ∈ administrators[{p}]"/>
<org.eventb.core.guard name="_WOm3IkHWEeqHCPZ-G665YQ" org.eventb.core.generated="false" org.eventb.core.label="grd5" org.eventb.core.predicate="o ∈ programme_outcomes[{p}]"/>
<org.eventb.core.action name="_WOneMEHWEeqHCPZ-G665YQ" org.eventb.core.assignment="programme_outcomes ≔ programme_outcomes ∖ {p↦o}" org.eventb.core.generated="false" org.eventb.core.label="act1"/>
<org.eventb.core.guard name="_tHsQ8EgnEeqeqbGZOOBkaQ" org.eventb.core.generated="false" org.eventb.core.label="grd6" org.eventb.core.predicate="p ∉ published"/>
<org.eventb.core.action name="_Mf95EEmhEeqDwOH5c8gGmw" org.eventb.core.assignment="outcome_mapping ≔ outcome_mapping ⩥ (ran(outcome_mapping) ▷ {o})" org.eventb.core.generated="false" org.eventb.core.label="act2"/>
</org.eventb.core.event>
<org.eventb.core.event name="_WOneMUHWEeqHCPZ-G665YQ" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.generated="false" org.eventb.core.label="assign_module_outcome">
<org.eventb.core.parameter name="_WOneMkHWEeqHCPZ-G665YQ" org.eventb.core.generated="false" org.eventb.core.identifier="u"/>
<org.eventb.core.parameter name="_gsP6sEHWEeqHCPZ-G665YQ" org.eventb.core.generated="false" org.eventb.core.identifier="m"/>
<org.eventb.core.parameter name="_WOosUUHWEeqHCPZ-G665YQ" org.eventb.core.generated="false" org.eventb.core.identifier="o"/>
<org.eventb.core.guard name="_WOosUkHWEeqHCPZ-G665YQ" org.eventb.core.generated="false" org.eventb.core.label="grd1" org.eventb.core.predicate="u ∈ logged_in"/>
<org.eventb.core.guard name="_WOpTYEHWEeqHCPZ-G665YQ" org.eventb.core.generated="false" org.eventb.core.label="grd2" org.eventb.core.predicate="m ∈ modules"/>
<org.eventb.core.guard name="_WOpTYUHWEeqHCPZ-G665YQ" org.eventb.core.generated="false" org.eventb.core.label="grd3" org.eventb.core.predicate="o ∈ M_OUTCOME"/>
<org.eventb.core.guard name="_WOpTYkHWEeqHCPZ-G665YQ" org.eventb.core.generated="false" org.eventb.core.label="grd4" org.eventb.core.predicate="u = module_leader(m)"/>
<org.eventb.core.guard name="_WOpTY0HWEeqHCPZ-G665YQ" org.eventb.core.generated="false" org.eventb.core.label="grd5" org.eventb.core.predicate="o ∉ module_outcomes[{m}]"/>
<org.eventb.core.action name="_WOpTZEHWEeqHCPZ-G665YQ" org.eventb.core.assignment="module_outcomes ≔ module_outcomes ∪ {m↦o}" org.eventb.core.generated="false" org.eventb.core.label="act1"/>
<org.eventb.core.guard name="__Ke6AEjBEeqDwOH5c8gGmw" org.eventb.core.generated="false" org.eventb.core.label="grd6" org.eventb.core.predicate="m ∉ contains_module[published]"/>
</org.eventb.core.event>
<org.eventb.core.event name="_WOpTZUHWEeqHCPZ-G665YQ" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.generated="false" org.eventb.core.label="unassign_module_outcome">
<org.eventb.core.parameter name="_WOp6cEHWEeqHCPZ-G665YQ" org.eventb.core.generated="false" org.eventb.core.identifier="u"/>
<org.eventb.core.parameter name="_gsSW8EHWEeqHCPZ-G665YQ" org.eventb.core.generated="false" org.eventb.core.identifier="m"/>
<org.eventb.core.parameter name="_WOp6ckHWEeqHCPZ-G665YQ" org.eventb.core.generated="false" org.eventb.core.identifier="o"/>
<org.eventb.core.guard name="_WOp6c0HWEeqHCPZ-G665YQ" org.eventb.core.generated="false" org.eventb.core.label="grd1" org.eventb.core.predicate="u ∈ logged_in"/>
<org.eventb.core.guard name="_WOqhgEHWEeqHCPZ-G665YQ" org.eventb.core.generated="false" org.eventb.core.label="grd2" org.eventb.core.predicate="m ∈ modules"/>
<org.eventb.core.guard name="_WOqhgUHWEeqHCPZ-G665YQ" org.eventb.core.generated="false" org.eventb.core.label="grd3" org.eventb.core.predicate="o ∈ M_OUTCOME"/>
<org.eventb.core.guard name="_WOrIkEHWEeqHCPZ-G665YQ" org.eventb.core.generated="false" org.eventb.core.label="grd4" org.eventb.core.predicate="u = module_leader(m)"/>
<org.eventb.core.guard name="_WOrIkUHWEeqHCPZ-G665YQ" org.eventb.core.generated="false" org.eventb.core.label="grd5" org.eventb.core.predicate="o ∈ module_outcomes[{m}]"/>
<org.eventb.core.action name="_WOrIkkHWEeqHCPZ-G665YQ" org.eventb.core.assignment="module_outcomes ≔ module_outcomes ∖ {m↦o}" org.eventb.core.generated="false" org.eventb.core.label="act1"/>
<org.eventb.core.guard name="__KgvMEjBEeqDwOH5c8gGmw" org.eventb.core.generated="false" org.eventb.core.label="grd6" org.eventb.core.predicate="m ∉ contains_module[published]"/>
<org.eventb.core.action name="_qP2pYEmhEeqDwOH5c8gGmw" org.eventb.core.assignment="outcome_mapping ≔ (dom(outcome_mapping) ▷ {o}) ⩤ outcome_mapping" org.eventb.core.generated="false" org.eventb.core.label="act2"/>
</org.eventb.core.event>
<org.eventb.core.event name="_WOrvoEHWEeqHCPZ-G665YQ" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.generated="false" org.eventb.core.label="map_outcome">
<org.eventb.core.parameter name="_b8VxgEgiEeqeqbGZOOBkaQ" org.eventb.core.generated="false" org.eventb.core.identifier="u"/>
<org.eventb.core.parameter name="_KEBQgUmgEeqDwOH5c8gGmw" org.eventb.core.generated="false" org.eventb.core.identifier="p"/>
<org.eventb.core.parameter name="_3uyg4UHkEeqHCPZ-G665YQ" org.eventb.core.generated="false" org.eventb.core.identifier="po"/>
<org.eventb.core.parameter name="_KEBQgEmgEeqDwOH5c8gGmw" org.eventb.core.generated="false" org.eventb.core.identifier="m"/>
<org.eventb.core.parameter name="_3uyg4EHkEeqHCPZ-G665YQ" org.eventb.core.generated="false" org.eventb.core.identifier="mo"/>
<org.eventb.core.guard name="_t9rBQEgoEeqeqbGZOOBkaQ" org.eventb.core.generated="false" org.eventb.core.label="grd1" org.eventb.core.predicate="u ∈ logged_in"/>
<org.eventb.core.guard name="_t9roUEgoEeqeqbGZOOBkaQ" org.eventb.core.generated="false" org.eventb.core.label="grd2" org.eventb.core.predicate="p ∈ programmes"/>
<org.eventb.core.guard name="_t9roUUgoEeqeqbGZOOBkaQ" org.eventb.core.generated="false" org.eventb.core.label="grd3" org.eventb.core.predicate="po ∈ P_OUTCOME"/>
<org.eventb.core.guard name="_t9roUkgoEeqeqbGZOOBkaQ" org.eventb.core.generated="false" org.eventb.core.label="grd4" org.eventb.core.predicate="m ∈ modules"/>
<org.eventb.core.guard name="_t9sPYEgoEeqeqbGZOOBkaQ" org.eventb.core.generated="false" org.eventb.core.label="grd5" org.eventb.core.predicate="mo ∈ M_OUTCOME"/>
<org.eventb.core.action name="_t9sPYUgoEeqeqbGZOOBkaQ" org.eventb.core.assignment="outcome_mapping ≔ outcome_mapping ∪ {(m↦mo)↦ (p↦po)}" org.eventb.core.generated="false" org.eventb.core.label="act1"/>
<org.eventb.core.guard name="_KEDFsEmgEeqDwOH5c8gGmw" org.eventb.core.generated="false" org.eventb.core.label="grd6" org.eventb.core.predicate="m ∈ contains_module[{p}]"/>
<org.eventb.core.guard name="_KEDFsUmgEeqDwOH5c8gGmw" org.eventb.core.generated="false" org.eventb.core.label="grd7" org.eventb.core.predicate="u ∈ administrators[{p}]"/>
<org.eventb.core.guard name="_KEDFskmgEeqDwOH5c8gGmw" org.eventb.core.generated="false" org.eventb.core.label="grd8" org.eventb.core.predicate="po ∈ programme_outcomes[{p}]"/>
<org.eventb.core.guard name="_k8uYUEmgEeqDwOH5c8gGmw" org.eventb.core.generated="false" org.eventb.core.label="grd9" org.eventb.core.predicate="mo ∈ module_outcomes[{m}]"/>
<org.eventb.core.guard name="_Wj4i4GeOEeqknqZz0CExqw" org.eventb.core.generated="false" org.eventb.core.label="grd10" org.eventb.core.predicate="(m↦mo)↦ (p↦po) ∉ outcome_mapping"/>
<org.eventb.core.guard name="_hHHgsGkFEeqIPJEEodEg6Q" org.eventb.core.generated="false" org.eventb.core.label="grd11" org.eventb.core.predicate="p ∉ published"/>
</org.eventb.core.event>
<org.eventb.core.event name="_WOrvoUHWEeqHCPZ-G665YQ" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.generated="false" org.eventb.core.label="unmap_outcome">
<org.eventb.core.parameter name="_aUbj8EmgEeqDwOH5c8gGmw" org.eventb.core.generated="false" org.eventb.core.identifier="u"/>
<org.eventb.core.parameter name="_aUcLAEmgEeqDwOH5c8gGmw" org.eventb.core.generated="false" org.eventb.core.identifier="p"/>
<org.eventb.core.parameter name="_69KSoEHqEeqHCPZ-G665YQ" org.eventb.core.generated="false" org.eventb.core.identifier="po"/>
<org.eventb.core.parameter name="_aUbj8UmgEeqDwOH5c8gGmw" org.eventb.core.generated="false" org.eventb.core.identifier="m"/>
<org.eventb.core.parameter name="_69Jrk0HqEeqHCPZ-G665YQ" org.eventb.core.generated="false" org.eventb.core.identifier="mo"/>
<org.eventb.core.guard name="_wKL8IEgoEeqeqbGZOOBkaQ" org.eventb.core.generated="false" org.eventb.core.label="grd1" org.eventb.core.predicate="u ∈ logged_in"/>
<org.eventb.core.guard name="_wKL8IUgoEeqeqbGZOOBkaQ" org.eventb.core.generated="false" org.eventb.core.label="grd2" org.eventb.core.predicate="p ∈ programmes"/>
<org.eventb.core.guard name="_wKL8IkgoEeqeqbGZOOBkaQ" org.eventb.core.generated="false" org.eventb.core.label="grd3" org.eventb.core.predicate="po ∈ P_OUTCOME"/>
<org.eventb.core.guard name="_wKMjMEgoEeqeqbGZOOBkaQ" org.eventb.core.generated="false" org.eventb.core.label="grd4" org.eventb.core.predicate="m ∈ modules"/>
<org.eventb.core.guard name="_aUcyEEmgEeqDwOH5c8gGmw" org.eventb.core.generated="false" org.eventb.core.label="grd5" org.eventb.core.predicate="mo ∈ M_OUTCOME"/>
<org.eventb.core.guard name="_aUdZIEmgEeqDwOH5c8gGmw" org.eventb.core.generated="false" org.eventb.core.label="grd6" org.eventb.core.predicate="m ∈ contains_module[{p}]"/>
<org.eventb.core.guard name="_aUdZIUmgEeqDwOH5c8gGmw" org.eventb.core.generated="false" org.eventb.core.label="grd7" org.eventb.core.predicate="u ∈ administrators[{p}]"/>
<org.eventb.core.guard name="_aUdZIkmgEeqDwOH5c8gGmw" org.eventb.core.generated="false" org.eventb.core.label="grd8" org.eventb.core.predicate="po ∈ programme_outcomes[{p}]"/>
<org.eventb.core.action name="_aUeAMEmgEeqDwOH5c8gGmw" org.eventb.core.assignment="outcome_mapping ≔ outcome_mapping ∖ {(m↦mo)↦ (p↦po)}" org.eventb.core.generated="false" org.eventb.core.label="act1"/>
<org.eventb.core.guard name="_l__zMEmgEeqDwOH5c8gGmw" org.eventb.core.generated="false" org.eventb.core.label="grd9" org.eventb.core.predicate="mo ∈ module_outcomes[{m}]"/>
<org.eventb.core.guard name="_FPt28GePEeqknqZz0CExqw" org.eventb.core.generated="false" org.eventb.core.label="grd10" org.eventb.core.predicate="(m↦mo)↦ (p↦po) ∈ outcome_mapping"/>
<org.eventb.core.guard name="_j08Y4GkFEeqIPJEEodEg6Q" org.eventb.core.generated="false" org.eventb.core.label="grd11" org.eventb.core.predicate="p ∉ published"/>
</org.eventb.core.event>
<org.eventb.core.event name="_7Y1LYEgTEeqeqbGZOOBkaQ" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.generated="false" org.eventb.core.label="publish_programme">
<org.eventb.core.refinesEvent name="_7Y1ycEgTEeqeqbGZOOBkaQ" org.eventb.core.target="publish_programme"/>
<org.eventb.core.guard name="_biA3wEmoEeqDwOH5c8gGmw" org.eventb.core.generated="false" org.eventb.core.label="grd31" org.eventb.core.predicate="∀po · po ∈ programme_outcomes[{p}] ⇒ outcome_mapping ▷ {p↦po} ≠ ∅"/>
</org.eventb.core.event>
<org.eventb.core.event name="_7Y1ycUgTEeqeqbGZOOBkaQ" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.generated="false" org.eventb.core.label="unpublish_programme">
<org.eventb.core.refinesEvent name="_7Y1yckgTEeqeqbGZOOBkaQ" org.eventb.core.target="unpublish_programme"/>
</org.eventb.core.event>
<org.eventb.core.event name="_vN_gIUHGEeqHd7PiYTbxHi" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.generated="false" org.eventb.core.label="create_module">
<org.eventb.core.refinesEvent name="'" org.eventb.core.target="create_module"/>
</org.eventb.core.event>
<org.eventb.core.event name="_vN_gIUHGEeqHd7PiYTbxHj" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.generated="false" org.eventb.core.label="delete_module">
<org.eventb.core.refinesEvent name="'" org.eventb.core.target="delete_module"/>
<org.eventb.core.action name="_GAwEQEHdEeqHCPZ-G665YQ" org.eventb.core.assignment="outcome_mapping ≔ ({m}◁module_outcomes) ⩤ outcome_mapping" org.eventb.core.generated="false" org.eventb.core.label="act31"/>
<org.eventb.core.action name="_C8oFIEmiEeqDwOH5c8gGmw" org.eventb.core.assignment="module_outcomes ≔ {m} ⩤ module_outcomes" org.eventb.core.generated="false" org.eventb.core.label="act32"/>
</org.eventb.core.event>
<org.eventb.core.event name="_vN_gIUHGEeqHd7PiYTbxHk" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.generated="false" org.eventb.core.label="assign_module">
<org.eventb.core.refinesEvent name="'" org.eventb.core.target="assign_module"/>
</org.eventb.core.event>
<org.eventb.core.event name="_vN_gIUHGEeqHd7PiYTbxHl" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.generated="false" org.eventb.core.label="unassign_module">
<org.eventb.core.refinesEvent name="'" org.eventb.core.target="unassign_module"/>
<org.eventb.core.action name="_klfEkEJvEeqHCPZ-G665YQ" org.eventb.core.assignment="outcome_mapping ≔ outcome_mapping ∖ ((({m} ◁ dom(outcome_mapping)) ◁ outcome_mapping) ▷ ({p}◁ran(outcome_mapping)))" org.eventb.core.generated="false" org.eventb.core.label="act31"/>
</org.eventb.core.event>
<org.eventb.core.event name="_vN_gIUHGEeqHd7PiYTbxHm" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.generated="false" org.eventb.core.label="transfer_module_ownership">
<org.eventb.core.refinesEvent name="'" org.eventb.core.target="transfer_module_ownership"/>
</org.eventb.core.event>
<org.eventb.core.event name="_vN_gIUHGEeqHd7PiYTbxHn" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.generated="false" org.eventb.core.label="create_programme">
<org.eventb.core.refinesEvent name="'" org.eventb.core.target="create_programme"/>
</org.eventb.core.event>
<org.eventb.core.event name="_vN_gIUHGEeqHd7PiYTbxHo" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.generated="false" org.eventb.core.label="delete_programme">
<org.eventb.core.refinesEvent name="'" org.eventb.core.target="delete_programme"/>
<org.eventb.core.action name="_oBH5QEmnEeqDwOH5c8gGmw" org.eventb.core.assignment="outcome_mapping ≔ outcome_mapping ⩥ ({p}◁ran(outcome_mapping))" org.eventb.core.generated="false" org.eventb.core.label="act31"/>
<org.eventb.core.action name="_Mfs94EmiEeqDwOH5c8gGmw" org.eventb.core.assignment="programme_outcomes ≔ {p} ⩤ programme_outcomes" org.eventb.core.generated="false" org.eventb.core.label="act32"/>
</org.eventb.core.event>
<org.eventb.core.event name="_vN_gIUHGEeqHd7PiYTbxHp" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.generated="false" org.eventb.core.label="add_administrator">
<org.eventb.core.refinesEvent name="'" org.eventb.core.target="add_administrator"/>
</org.eventb.core.event>
<org.eventb.core.event name="_vN_gIUHGEeqHd7PiYTbxHq" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.generated="false" org.eventb.core.label="remove_administrator">
<org.eventb.core.refinesEvent name="'" org.eventb.core.target="remove_administrator"/>
</org.eventb.core.event>
<org.eventb.core.event name="_vN_gIUHGEeqHd7PiYTbxHr" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.generated="false" org.eventb.core.label="transfer_ownership">
<org.eventb.core.refinesEvent name="'" org.eventb.core.target="transfer_ownership"/>
</org.eventb.core.event>
<org.eventb.core.event name="_vN_gIUHGEeqHd7PiYTbxHs" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.generated="false" org.eventb.core.label="register">
<org.eventb.core.refinesEvent name="'" org.eventb.core.target="register"/>
</org.eventb.core.event>
<org.eventb.core.event name="_vN_gIUHGEeqHd7PiYTbxHt" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.generated="false" org.eventb.core.label="unregister">
<org.eventb.core.refinesEvent name="'" org.eventb.core.target="unregister"/>
</org.eventb.core.event>
<org.eventb.core.event name="_vN_gIUHGEeqHd7PiYTbxHu" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.generated="false" org.eventb.core.label="login">
<org.eventb.core.refinesEvent name="'" org.eventb.core.target="login"/>
</org.eventb.core.event>
<org.eventb.core.event name="_vN_gIUHGEeqHd7PiYTbxHv" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.generated="false" org.eventb.core.label="logout">
<org.eventb.core.refinesEvent name="'" org.eventb.core.target="logout"/>
</org.eventb.core.event>
<org.eventb.core.variable name="_ksiLMEHUEeqHCPZ-G665YQ" org.eventb.core.generated="false" org.eventb.core.identifier="module_outcomes"/>
<org.eventb.core.variable name="_ksiLMUHUEeqHCPZ-G665YQ" org.eventb.core.generated="false" org.eventb.core.identifier="programme_outcomes"/>
<org.eventb.core.variable name="_ksiLMkHUEeqHCPZ-G665YQ" org.eventb.core.generated="false" org.eventb.core.identifier="outcome_mapping"/>
<org.eventb.core.invariant name="_ksiyQEHUEeqHCPZ-G665YQ" org.eventb.core.generated="false" org.eventb.core.label="inv31" org.eventb.core.predicate="programme_outcomes ∈ programmes ↔ P_OUTCOME"/>
<org.eventb.core.invariant name="_Jmq7sEHVEeqHCPZ-G665YQ" org.eventb.core.generated="false" org.eventb.core.label="inv32" org.eventb.core.predicate="module_outcomes ∈ modules ↔ M_OUTCOME"/>
<org.eventb.core.invariant name="_Jmq7sUHVEeqHCPZ-G665YQ" org.eventb.core.generated="false" org.eventb.core.label="inv33" org.eventb.core.predicate="outcome_mapping ∈ module_outcomes ↔ programme_outcomes"/>
<org.eventb.core.variable name="_F0NbkEgIEeqeqbGZOOBkaQ" org.eventb.core.generated="false" org.eventb.core.identifier="credits_awarded"/>
<org.eventb.core.variable name="_5ohrYEgTEeqeqbGZOOBkaQ" org.eventb.core.generated="false" org.eventb.core.identifier="published"/>
<org.eventb.core.invariant name="_OHoTEEmkEeqDwOH5c8gGmw" org.eventb.core.generated="false" org.eventb.core.label="inv34" org.eventb.core.predicate="∀m · m ∈ dom(dom(outcome_mapping)) ⇒ dom(ran(({m} ◁ dom(outcome_mapping)) ◁outcome_mapping)) ⊆ contains_module∼[{m}]"/>
</org.eventb.core.machineFile>