-
Notifications
You must be signed in to change notification settings - Fork 0
/
m4_prerequisites.bum
120 lines (120 loc) · 17.6 KB
/
m4_prerequisites.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
<?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="1588702599337" org.eventb.texttools.text_representation="machine m4_prerequisites refines m3_outcomes sees c3_outcomes variables registered logged_in programmes programme_leader administrators modules contains_module module_leader module_outcomes programme_outcomes outcome_mapping prerequisites credits_awarded published invariants @inv41 prerequisites ∈ modules ↔ modules @inv42 ∀p,m · p ∈ published ∧ m ∈ contains_module[{p}] ⇒ prerequisites[{m}] ⊆ contains_module[{p}] // PUB5 events event INITIALISATION extends INITIALISATION then @act41 prerequisites ≔ ∅ end event assign_prerequisite any u m1 m2 where @grd41 u ∈ logged_in @grd42 m1 ∈ modules @grd43 m2 ∈ modules @grd44 u = module_leader(m1) @grd47 m2 ∉ prerequisites[{m1}] @grd48 m1 ≠ m2 @grd49 m1 ∉ contains_module[published] @grd50 m1 ∉ prerequisites[{m2}] then @act41 prerequisites ≔ prerequisites ∪ {m1↦m2} end event unassign_prerequisite any u m1 m2 where @grd41 u ∈ logged_in @grd42 m1 ∈ modules @grd43 m2 ∈ modules @grd44 u = module_leader(m1) @grd47 m2 ∈ prerequisites[{m1}] @grd48 m1 ∉ contains_module[published] then @act41 prerequisites ≔ prerequisites ∖ {m1↦m2} end event publish_programme extends publish_programme where @grd41 ∀m · m ∈ contains_module[{p}] ⇒ prerequisites[{m}] ⊆ contains_module[{p}] end event unpublish_programme extends unpublish_programme end event assign_programme_outcome extends assign_programme_outcome end event unassign_programme_outcome extends unassign_programme_outcome end event assign_module_outcome extends assign_module_outcome end event unassign_module_outcome extends unassign_module_outcome end event map_outcome extends map_outcome end event unmap_outcome extends unmap_outcome end event create_module extends create_module then @act41 prerequisites ≔ ({m} ⩤ prerequisites) ⩥ {m} end event delete_module extends delete_module 	where @grd41 m ∉ ran(prerequisites) then @act41 prerequisites ≔ {m} ⩤ prerequisites end event assign_module extends assign_module end event unassign_module extends unassign_module end event transfer_module_ownership extends transfer_module_ownership end event create_programme extends create_programme end event delete_programme extends delete_programme 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="m3_outcomes"/>
<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.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.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="__qLSkEJyEeqHCPZ-G665YQ" org.eventb.core.assignment="prerequisites ≔ ∅" org.eventb.core.generated="false" org.eventb.core.label="act41"/>
</org.eventb.core.event>
<org.eventb.core.event name="_D-LeYEJzEeqHCPZ-G665YQ" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.generated="false" org.eventb.core.label="assign_prerequisite">
<org.eventb.core.parameter name="_4vXnIEJzEeqHCPZ-G665YQ" org.eventb.core.generated="false" org.eventb.core.identifier="u"/>
<org.eventb.core.parameter name="_4vXnIUJzEeqHCPZ-G665YQ" org.eventb.core.generated="false" org.eventb.core.identifier="m1"/>
<org.eventb.core.parameter name="_4vXnIkJzEeqHCPZ-G665YQ" org.eventb.core.generated="false" org.eventb.core.identifier="m2"/>
<org.eventb.core.guard name="_4vYOMEJzEeqHCPZ-G665YQ" org.eventb.core.generated="false" org.eventb.core.label="grd41" org.eventb.core.predicate="u ∈ logged_in"/>
<org.eventb.core.guard name="_4vYOMUJzEeqHCPZ-G665YQ" org.eventb.core.generated="false" org.eventb.core.label="grd42" org.eventb.core.predicate="m1 ∈ modules"/>
<org.eventb.core.guard name="_4vY1QEJzEeqHCPZ-G665YQ" org.eventb.core.generated="false" org.eventb.core.label="grd43" org.eventb.core.predicate="m2 ∈ modules"/>
<org.eventb.core.guard name="_4vY1QUJzEeqHCPZ-G665YQ" org.eventb.core.generated="false" org.eventb.core.label="grd44" org.eventb.core.predicate="u = module_leader(m1)"/>
<org.eventb.core.guard name="_MckKgEJ0EeqHCPZ-G665YQ" org.eventb.core.generated="false" org.eventb.core.label="grd47" org.eventb.core.predicate="m2 ∉ prerequisites[{m1}]"/>
<org.eventb.core.action name="_MckKgUJ0EeqHCPZ-G665YQ" org.eventb.core.assignment="prerequisites ≔ prerequisites ∪ {m1↦m2}" org.eventb.core.generated="false" org.eventb.core.label="act41"/>
<org.eventb.core.guard name="_Tmo70EKFEeqP-97FScFUgw" org.eventb.core.generated="false" org.eventb.core.label="grd48" org.eventb.core.predicate="m1 ≠ m2"/>
<org.eventb.core.guard name="_S7ILgEgpEeqeqbGZOOBkaQ" org.eventb.core.generated="false" org.eventb.core.label="grd49" org.eventb.core.predicate="m1 ∉ contains_module[published]"/>
<org.eventb.core.guard name="_LqBnUI70Eeq1J8HIGUp2sw" org.eventb.core.generated="false" org.eventb.core.label="grd50" org.eventb.core.predicate="m1 ∉ prerequisites[{m2}]"/>
</org.eventb.core.event>
<org.eventb.core.event name="_D-MFcEJzEeqHCPZ-G665YQ" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.generated="false" org.eventb.core.label="unassign_prerequisite">
<org.eventb.core.parameter name="_70QfAEJ0EeqHCPZ-G665YQ" org.eventb.core.generated="false" org.eventb.core.identifier="u"/>
<org.eventb.core.parameter name="_70QfAUJ0EeqHCPZ-G665YQ" org.eventb.core.generated="false" org.eventb.core.identifier="m1"/>
<org.eventb.core.parameter name="_70QfAkJ0EeqHCPZ-G665YQ" org.eventb.core.generated="false" org.eventb.core.identifier="m2"/>
<org.eventb.core.guard name="_70RGEEJ0EeqHCPZ-G665YQ" org.eventb.core.generated="false" org.eventb.core.label="grd41" org.eventb.core.predicate="u ∈ logged_in"/>
<org.eventb.core.guard name="_70RGEUJ0EeqHCPZ-G665YQ" org.eventb.core.generated="false" org.eventb.core.label="grd42" org.eventb.core.predicate="m1 ∈ modules"/>
<org.eventb.core.guard name="_70RGEkJ0EeqHCPZ-G665YQ" org.eventb.core.generated="false" org.eventb.core.label="grd43" org.eventb.core.predicate="m2 ∈ modules"/>
<org.eventb.core.guard name="_70RtIEJ0EeqHCPZ-G665YQ" org.eventb.core.generated="false" org.eventb.core.label="grd44" org.eventb.core.predicate="u = module_leader(m1)"/>
<org.eventb.core.guard name="_70RtIUJ0EeqHCPZ-G665YQ" org.eventb.core.generated="false" org.eventb.core.label="grd47" org.eventb.core.predicate="m2 ∈ prerequisites[{m1}]"/>
<org.eventb.core.action name="_70RtIkJ0EeqHCPZ-G665YQ" org.eventb.core.assignment="prerequisites ≔ prerequisites ∖ {m1↦m2}" org.eventb.core.generated="false" org.eventb.core.label="act41"/>
<org.eventb.core.guard name="_UiGJUEgpEeqeqbGZOOBkaQ" org.eventb.core.generated="false" org.eventb.core.label="grd48" org.eventb.core.predicate="m1 ∉ contains_module[published]"/>
</org.eventb.core.event>
<org.eventb.core.event name="_EVzGYEgUEeqeqbGZOOBkaQ" 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="_EVzGYUgUEeqeqbGZOOBkaQ" org.eventb.core.target="publish_programme"/>
<org.eventb.core.guard name="_IanikEJ1EeqHCPZ-G665YQ" org.eventb.core.generated="false" org.eventb.core.label="grd41" org.eventb.core.predicate="∀m · m ∈ contains_module[{p}] ⇒ prerequisites[{m}] ⊆ contains_module[{p}]"/>
</org.eventb.core.event>
<org.eventb.core.event name="_EVzGYkgUEeqeqbGZOOBkaQ" 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="_EVzGY0gUEeqeqbGZOOBkaQ" 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="assign_programme_outcome">
<org.eventb.core.refinesEvent name="'" org.eventb.core.target="assign_programme_outcome"/>
</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="unassign_programme_outcome">
<org.eventb.core.refinesEvent name="'" org.eventb.core.target="unassign_programme_outcome"/>
</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_outcome">
<org.eventb.core.refinesEvent name="'" org.eventb.core.target="assign_module_outcome"/>
</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_outcome">
<org.eventb.core.refinesEvent name="'" org.eventb.core.target="unassign_module_outcome"/>
</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="map_outcome">
<org.eventb.core.refinesEvent name="'" org.eventb.core.target="map_outcome"/>
</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="unmap_outcome">
<org.eventb.core.refinesEvent name="'" org.eventb.core.target="unmap_outcome"/>
</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="create_module">
<org.eventb.core.refinesEvent name="'" org.eventb.core.target="create_module"/>
<org.eventb.core.action name="_AqyJEEJ1EeqHCPZ-G665YQ" org.eventb.core.assignment="prerequisites ≔ ({m} ⩤ prerequisites) ⩥ {m}" org.eventb.core.generated="false" org.eventb.core.label="act41"/>
</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="delete_module">
<org.eventb.core.refinesEvent name="'" org.eventb.core.target="delete_module"/>
<org.eventb.core.action name="_eq37wEJ5EeqHCPZ-G665YQ" org.eventb.core.assignment="prerequisites ≔ {m} ⩤ prerequisites" org.eventb.core.generated="false" org.eventb.core.label="act41"/>
<org.eventb.core.guard name="_zr33AI7xEeq1J8HIGUp2sw" org.eventb.core.generated="false" org.eventb.core.label="grd41" org.eventb.core.predicate="m ∉ ran(prerequisites)"/>
</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="assign_module">
<org.eventb.core.refinesEvent name="'" org.eventb.core.target="assign_module"/>
</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="unassign_module">
<org.eventb.core.refinesEvent name="'" org.eventb.core.target="unassign_module"/>
</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="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_gIUHGEeqHd7PiYTbxHt" 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_gIUHGEeqHd7PiYTbxHu" 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.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="add_administrator">
<org.eventb.core.refinesEvent name="'" org.eventb.core.target="add_administrator"/>
</org.eventb.core.event>
<org.eventb.core.event name="_vN_gIUHGEeqHd7PiYTbxHw" 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_gIUHGEeqHd7PiYTbxHx" 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_gIUHGEeqHd7PiYTbxHy" 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_gIUHGEeqHd7PiYTbxHz" 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_gIUHGEeqHd7PiYTbxH{" 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_gIUHGEeqHd7PiYTbxH|" 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="_80wkoEJyEeqHCPZ-G665YQ" org.eventb.core.generated="false" org.eventb.core.identifier="prerequisites"/>
<org.eventb.core.invariant name="_80wkoUJyEeqHCPZ-G665YQ" org.eventb.core.generated="false" org.eventb.core.label="inv41" org.eventb.core.predicate="prerequisites ∈ modules ↔ modules"/>
<org.eventb.core.invariant name="_lUfGUEJ0EeqHCPZ-G665YQ" org.eventb.core.comment="PUB5" org.eventb.core.generated="false" org.eventb.core.label="inv42" org.eventb.core.predicate="∀p,m · p ∈ published ∧ m ∈ contains_module[{p}] ⇒ prerequisites[{m}] ⊆ contains_module[{p}]"/>
<org.eventb.core.variable name="_HgJY8EgIEeqeqbGZOOBkaQ" org.eventb.core.generated="false" org.eventb.core.identifier="credits_awarded"/>
<org.eventb.core.variable name="_C7-zwEgUEeqeqbGZOOBkaQ" org.eventb.core.generated="false" org.eventb.core.identifier="published"/>
</org.eventb.core.machineFile>