-
Notifications
You must be signed in to change notification settings - Fork 0
/
m1_programmes.bum
112 lines (112 loc) · 19.4 KB
/
m1_programmes.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
<?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="1588610642320" org.eventb.texttools.text_representation="machine m1_programmes refines m0_users sees c1_programmes variables registered logged_in programmes programme_leader administrators published invariants @inv11 programmes ⊆ PROGRAMME @inv12 programme_leader ∈ programmes → registered // PRG9 @inv13 administrators ∈ programmes ↔ registered // PRG10 @inv14 published ⊆ programmes events event INITIALISATION extends INITIALISATION then @act11 programmes ≔ ∅ @act12 programme_leader ≔ ∅ @act13 administrators ≔ ∅ @act14 published ≔ ∅ end event publish_programme // PUB1 any u p where @grd1 u ∈ logged_in @grd2 p ∈ programmes @grd3 u = programme_leader(p) @grd4 p ∉ published then @act1 published ≔ published ∪ {p} end event unpublish_programme // PUB3 any u p where @grd1 u ∈ logged_in @grd2 p ∈ programmes @grd3 u = programme_leader(p) @grd4 p ∈ published then @act1 published ≔ published ∖ {p} end event create_programme // USR5 any u p where @grd1 u ∈ logged_in @grd2 p ∈ PROGRAMME @grd3 p ∉ programmes then @act1 programmes ≔ programmes ∪ {p} @act2 programme_leader(p) ≔ u // USR15 @act3 administrators ≔ administrators ∪ {p↦u} // USR16 end event delete_programme // PRG11 any u p where @grd1 u ∈ logged_in @grd2 p ∈ programmes @grd3 programme_leader(p) = u // PRG11.1 @grd4 p ∉ published then @act1 programmes ≔ programmes ∖ {p} @act2 programme_leader ≔ {p} ⩤ programme_leader @act3 administrators ≔ {p} ⩤ administrators end event add_administrator any u1 u2 p where @grd1 u1 ∈ logged_in @grd2 u2 ∈ registered @grd3 p ∈ programmes @grd4 programme_leader(p) = u1 @grd5 u2 ∉ administrators[{p}] @grd6 p ∉ published then @act1 administrators ≔ administrators ∪ {p↦u2} end event remove_administrator any u1 u2 p where @grd1 u1 ∈ logged_in @grd2 u2 ∈ registered @grd3 p ∈ programmes @grd4 programme_leader(p) = u1 @grd5 u2 ∈ administrators[{p}] @grd6 u1 ≠ u2 @grd7 p ∉ published then @act1 administrators ≔ administrators ∖ {p↦u2} end event transfer_ownership // USR7 any u1 u2 p where @grd1 u1 ∈ logged_in @grd2 u2 ∈ registered @grd3 p ∈ programmes @grd4 programme_leader(p) = u1 @grd5 u2 ∈ administrators[{p}] // USR7.1 @grd6 u1 ≠ u2 @grd7 p ∉ published then @act1 programme_leader(p) ≔ u2 end event register extends register end event unregister extends unregister where @grd11 u ∉ ran(programme_leader) // USR9.2 @grd12 u ∉ ran(administrators) // USR9.1 end event login extends login end event logout extends logout end end " version="5">
<org.eventb.core.refinesMachine name="'" org.eventb.core.target="m0_users"/>
<org.eventb.core.seesContext name="_c5qNIEHGEeqHd7PiYTbxHg" org.eventb.core.target="c1_programmes"/>
<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.event name="_MTJYwEHEEeqKzaOTi1o2gh" 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="_0s5_4EHGEeqHd7PiYTbxHg" org.eventb.core.assignment="programmes ≔ ∅" org.eventb.core.generated="false" org.eventb.core.label="act11"/>
<org.eventb.core.action name="_0s5_4UHGEeqHd7PiYTbxHg" org.eventb.core.assignment="programme_leader ≔ ∅" org.eventb.core.generated="false" org.eventb.core.label="act12"/>
<org.eventb.core.action name="_0s5_4kHGEeqHd7PiYTbxHg" org.eventb.core.assignment="administrators ≔ ∅" org.eventb.core.generated="false" org.eventb.core.label="act13"/>
<org.eventb.core.action name="_3ZnrMEgQEeqeqbGZOOBkaQ" org.eventb.core.assignment="published ≔ ∅" org.eventb.core.generated="false" org.eventb.core.label="act14"/>
</org.eventb.core.event>
<org.eventb.core.event name="_gpYtQEgTEeqeqbGZOOBkaQ" org.eventb.core.comment="PUB1" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.generated="false" org.eventb.core.label="publish_programme">
<org.eventb.core.parameter name="_JVqMkUHHEeqHd7PiYTbxHg" org.eventb.core.generated="false" org.eventb.core.identifier="u"/>
<org.eventb.core.parameter name="_JVqMkkHHEeqHd7PiYTbxHg" org.eventb.core.generated="false" org.eventb.core.identifier="p"/>
<org.eventb.core.guard name="_JVqzoEHHEeqHd7PiYTbxHg" org.eventb.core.generated="false" org.eventb.core.label="grd1" org.eventb.core.predicate="u ∈ logged_in"/>
<org.eventb.core.guard name="_JVqzoUHHEeqHd7PiYTbxHg" org.eventb.core.generated="false" org.eventb.core.label="grd2" org.eventb.core.predicate="p ∈ programmes"/>
<org.eventb.core.guard name="_JVqzokHHEeqHd7PiYTbxHg" org.eventb.core.generated="false" org.eventb.core.label="grd3" org.eventb.core.predicate="u = programme_leader(p)"/>
<org.eventb.core.guard name="_sioQokHHEeqHd7PiYTbxHg" org.eventb.core.generated="false" org.eventb.core.label="grd4" org.eventb.core.predicate="p ∉ published"/>
<org.eventb.core.action name="_JVrasEHHEeqHd7PiYTbxHg" org.eventb.core.assignment="published ≔ published ∪ {p}" org.eventb.core.generated="false" org.eventb.core.label="act1"/>
</org.eventb.core.event>
<org.eventb.core.event name="_gpaicEgTEeqeqbGZOOBkaQ" org.eventb.core.comment="PUB3" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.generated="false" org.eventb.core.label="unpublish_programme">
<org.eventb.core.parameter name="_RONdMEHHEeqHd7PiYTbxHg" org.eventb.core.generated="false" org.eventb.core.identifier="u"/>
<org.eventb.core.parameter name="_ROOEQEHHEeqHd7PiYTbxHg" org.eventb.core.generated="false" org.eventb.core.identifier="p"/>
<org.eventb.core.guard name="_g_lrQEHHEeqHd7PiYTbxHg" org.eventb.core.generated="false" org.eventb.core.label="grd1" org.eventb.core.predicate="u ∈ logged_in"/>
<org.eventb.core.guard name="_g_mSUEHHEeqHd7PiYTbxHg" org.eventb.core.generated="false" org.eventb.core.label="grd2" org.eventb.core.predicate="p ∈ programmes"/>
<org.eventb.core.guard name="_g_mSUUHHEeqHd7PiYTbxHg" org.eventb.core.generated="false" org.eventb.core.label="grd3" org.eventb.core.predicate="u = programme_leader(p)"/>
<org.eventb.core.guard name="_3BElcEHHEeqHd7PiYTbxHg" org.eventb.core.generated="false" org.eventb.core.label="grd4" org.eventb.core.predicate="p ∈ published"/>
<org.eventb.core.action name="_g_m5YEHHEeqHd7PiYTbxHg" org.eventb.core.assignment="published ≔ published ∖ {p}" org.eventb.core.generated="false" org.eventb.core.label="act1"/>
</org.eventb.core.event>
<org.eventb.core.event name="_JVqMkEHHEeqHd7PiYTbxHg" org.eventb.core.comment="USR5" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.generated="false" org.eventb.core.label="create_programme">
<org.eventb.core.action name="_x9OREEHHEeqHd7PiYTbxHg" org.eventb.core.assignment="programmes ≔ programmes ∪ {p}" org.eventb.core.generated="false" org.eventb.core.label="act1"/>
<org.eventb.core.action name="_JVrasUHHEeqHd7PiYTbxHg" org.eventb.core.assignment="programme_leader(p) ≔ u" org.eventb.core.comment="USR15" org.eventb.core.generated="false" org.eventb.core.label="act2"/>
<org.eventb.core.action name="_ROM2IEHHEeqHd7PiYTbxHg" org.eventb.core.assignment="administrators ≔ administrators ∪ {p↦u}" org.eventb.core.comment="USR16" org.eventb.core.generated="false" org.eventb.core.label="act3"/>
<org.eventb.core.parameter name="_gpeM0EgTEeqeqbGZOOBkaQ" org.eventb.core.generated="false" org.eventb.core.identifier="u"/>
<org.eventb.core.parameter name="_sinpkEHHEeqHd7PiYTbxHg" org.eventb.core.generated="false" org.eventb.core.identifier="p"/>
<org.eventb.core.guard name="_sinpkUHHEeqHd7PiYTbxHg" org.eventb.core.generated="false" org.eventb.core.label="grd1" org.eventb.core.predicate="u ∈ logged_in"/>
<org.eventb.core.guard name="_sioQoEHHEeqHd7PiYTbxHg" org.eventb.core.generated="false" org.eventb.core.label="grd2" org.eventb.core.predicate="p ∈ PROGRAMME"/>
<org.eventb.core.guard name="_sioQoUHHEeqHd7PiYTbxHg" org.eventb.core.generated="false" org.eventb.core.label="grd3" org.eventb.core.predicate="p ∉ programmes"/>
</org.eventb.core.event>
<org.eventb.core.event name="_JVsBwEHHEeqHd7PiYTbxHg" org.eventb.core.comment="PRG11" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.generated="false" org.eventb.core.label="delete_programme">
<org.eventb.core.action name="_3BFMgEHHEeqHd7PiYTbxHg" org.eventb.core.assignment="programmes ≔ programmes ∖ {p}" org.eventb.core.generated="false" org.eventb.core.label="act1"/>
<org.eventb.core.action name="_g_m5YUHHEeqHd7PiYTbxHg" org.eventb.core.assignment="programme_leader ≔ {p} ⩤ programme_leader" org.eventb.core.generated="false" org.eventb.core.label="act2"/>
<org.eventb.core.action name="_g_ngcEHHEeqHd7PiYTbxHg" org.eventb.core.assignment="administrators ≔ {p} ⩤ administrators" org.eventb.core.generated="false" org.eventb.core.label="act3"/>
<org.eventb.core.parameter name="_oWwBkEgTEeqeqbGZOOBkaQ" org.eventb.core.generated="false" org.eventb.core.identifier="u"/>
<org.eventb.core.parameter name="_3BDXUkHHEeqHd7PiYTbxHg" org.eventb.core.generated="false" org.eventb.core.identifier="p"/>
<org.eventb.core.guard name="_3BD-YEHHEeqHd7PiYTbxHg" org.eventb.core.generated="false" org.eventb.core.label="grd1" org.eventb.core.predicate="u ∈ logged_in"/>
<org.eventb.core.guard name="_3BD-YUHHEeqHd7PiYTbxHg" org.eventb.core.generated="false" org.eventb.core.label="grd2" org.eventb.core.predicate="p ∈ programmes"/>
<org.eventb.core.guard name="_3BD-YkHHEeqHd7PiYTbxHg" org.eventb.core.comment="PRG11.1" org.eventb.core.generated="false" org.eventb.core.label="grd3" org.eventb.core.predicate="programme_leader(p) = u"/>
<org.eventb.core.guard name="_7nL08UHHEeqHd7PiYTbxHg" org.eventb.core.generated="false" org.eventb.core.label="grd4" org.eventb.core.predicate="p ∉ published"/>
</org.eventb.core.event>
<org.eventb.core.event name="_JVsBwUHHEeqHd7PiYTbxHg" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.generated="false" org.eventb.core.label="add_administrator">
<org.eventb.core.parameter name="_sinCgEHHEeqHd7PiYTbxHg" org.eventb.core.generated="false" org.eventb.core.identifier="u1"/>
<org.eventb.core.parameter name="_sinCgUHHEeqHd7PiYTbxHg" org.eventb.core.generated="false" org.eventb.core.identifier="u2"/>
<org.eventb.core.guard name="_7nLN4UHHEeqHd7PiYTbxHg" org.eventb.core.generated="false" org.eventb.core.label="grd1" org.eventb.core.predicate="u1 ∈ logged_in"/>
<org.eventb.core.guard name="_7nLN4kHHEeqHd7PiYTbxHg" org.eventb.core.generated="false" org.eventb.core.label="grd2" org.eventb.core.predicate="u2 ∈ registered"/>
<org.eventb.core.guard name="_7nL08EHHEeqHd7PiYTbxHg" org.eventb.core.generated="false" org.eventb.core.label="grd3" org.eventb.core.predicate="p ∈ programmes"/>
<org.eventb.core.guard name="_gpmIoEgTEeqeqbGZOOBkaQ" org.eventb.core.generated="false" org.eventb.core.label="grd4" org.eventb.core.predicate="programme_leader(p) = u1"/>
<org.eventb.core.guard name="_sio3sEHHEeqHd7PiYTbxHg" org.eventb.core.generated="false" org.eventb.core.label="grd5" org.eventb.core.predicate="u2 ∉ administrators[{p}]"/>
<org.eventb.core.parameter name="_7nLN4EHHEeqHd7PiYTbxHg" org.eventb.core.generated="false" org.eventb.core.identifier="p"/>
<org.eventb.core.action name="_7nMcAUHHEeqHd7PiYTbxHg" org.eventb.core.assignment="administrators ≔ administrators ∪ {p↦u2}" org.eventb.core.generated="false" org.eventb.core.label="act1"/>
<org.eventb.core.guard name="_cDwN8EHIEeqHd7PiYTbxHg" 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="_JVsBwkHHEeqHd7PiYTbxHg" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.generated="false" org.eventb.core.label="remove_administrator">
<org.eventb.core.parameter name="_3BDXUEHHEeqHd7PiYTbxHg" org.eventb.core.generated="false" org.eventb.core.identifier="u1"/>
<org.eventb.core.parameter name="_3BDXUUHHEeqHd7PiYTbxHg" org.eventb.core.generated="false" org.eventb.core.identifier="u2"/>
<org.eventb.core.guard name="_gpk6gEgTEeqeqbGZOOBkaQ" org.eventb.core.generated="false" org.eventb.core.label="grd1" org.eventb.core.predicate="u1 ∈ logged_in"/>
<org.eventb.core.guard name="_gplhkEgTEeqeqbGZOOBkaQ" org.eventb.core.generated="false" org.eventb.core.label="grd2" org.eventb.core.predicate="u2 ∈ registered"/>
<org.eventb.core.guard name="_gplhkUgTEeqeqbGZOOBkaQ" org.eventb.core.generated="false" org.eventb.core.label="grd3" org.eventb.core.predicate="p ∈ programmes"/>
<org.eventb.core.guard name="_oW1hIkgTEeqeqbGZOOBkaQ" org.eventb.core.generated="false" org.eventb.core.label="grd4" org.eventb.core.predicate="programme_leader(p) = u1"/>
<org.eventb.core.guard name="_3BElcUHHEeqHd7PiYTbxHg" org.eventb.core.generated="false" org.eventb.core.label="grd5" org.eventb.core.predicate="u2 ∈ administrators[{p}]"/>
<org.eventb.core.parameter name="_gpmvsEgTEeqeqbGZOOBkaQ" org.eventb.core.generated="false" org.eventb.core.identifier="p"/>
<org.eventb.core.action name="_gpmvsUgTEeqeqbGZOOBkaQ" org.eventb.core.assignment="administrators ≔ administrators ∖ {p↦u2}" org.eventb.core.generated="false" org.eventb.core.label="act1"/>
<org.eventb.core.guard name="_eZxgUEc9EeqCJoBEKqsuQA" org.eventb.core.generated="false" org.eventb.core.label="grd6" org.eventb.core.predicate="u1 ≠ u2"/>
<org.eventb.core.guard name="_WXhJ8EgVEeqeqbGZOOBkaQ" org.eventb.core.generated="false" org.eventb.core.label="grd7" org.eventb.core.predicate="p ∉ published"/>
</org.eventb.core.event>
<org.eventb.core.event name="_JVso0EHHEeqHd7PiYTbxHg" org.eventb.core.comment="USR7" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.generated="false" org.eventb.core.label="transfer_ownership">
<org.eventb.core.parameter name="_7nKm0EHHEeqHd7PiYTbxHg" org.eventb.core.generated="false" org.eventb.core.identifier="u1"/>
<org.eventb.core.parameter name="_7nKm0UHHEeqHd7PiYTbxHg" org.eventb.core.generated="false" org.eventb.core.identifier="u2"/>
<org.eventb.core.guard name="_oW06EEgTEeqeqbGZOOBkaQ" org.eventb.core.generated="false" org.eventb.core.label="grd1" org.eventb.core.predicate="u1 ∈ logged_in"/>
<org.eventb.core.guard name="_oW1hIEgTEeqeqbGZOOBkaQ" org.eventb.core.generated="false" org.eventb.core.label="grd2" org.eventb.core.predicate="u2 ∈ registered"/>
<org.eventb.core.guard name="_oW1hIUgTEeqeqbGZOOBkaQ" org.eventb.core.generated="false" org.eventb.core.label="grd3" org.eventb.core.predicate="p ∈ programmes"/>
<org.eventb.core.guard name="_aUM3YEgUEeqeqbGZOOBkaQ" org.eventb.core.generated="false" org.eventb.core.label="grd4" org.eventb.core.predicate="programme_leader(p) = u1"/>
<org.eventb.core.guard name="_7nMcAEHHEeqHd7PiYTbxHg" org.eventb.core.comment="USR7.1" org.eventb.core.generated="false" org.eventb.core.label="grd5" org.eventb.core.predicate="u2 ∈ administrators[{p}]"/>
<org.eventb.core.parameter name="_oW2IMEgTEeqeqbGZOOBkaQ" org.eventb.core.generated="false" org.eventb.core.identifier="p"/>
<org.eventb.core.action name="_oW2IMUgTEeqeqbGZOOBkaQ" org.eventb.core.assignment="programme_leader(p) ≔ u2" org.eventb.core.generated="false" org.eventb.core.label="act1"/>
<org.eventb.core.guard name="_bx1dkEgVEeqeqbGZOOBkaQ" org.eventb.core.generated="false" org.eventb.core.label="grd6" org.eventb.core.predicate="u1 ≠ u2"/>
<org.eventb.core.guard name="_bx1dkUgVEeqeqbGZOOBkaQ" org.eventb.core.generated="false" org.eventb.core.label="grd7" org.eventb.core.predicate="p ∉ published"/>
</org.eventb.core.event>
<org.eventb.core.event name="_MTJYwEHEEeqKzaOTi1o2gi" 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="_MTJYwEHEEeqKzaOTi1o2gj" 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.guard name="_CWPG4EHIEeqHd7PiYTbxHg" org.eventb.core.comment="USR9.2" org.eventb.core.generated="false" org.eventb.core.label="grd11" org.eventb.core.predicate="u ∉ ran(programme_leader)"/>
<org.eventb.core.guard name="_CWPG4UHIEeqHd7PiYTbxHg" org.eventb.core.comment="USR9.1" org.eventb.core.generated="false" org.eventb.core.label="grd12" org.eventb.core.predicate="u ∉ ran(administrators)"/>
</org.eventb.core.event>
<org.eventb.core.event name="_MTJYwEHEEeqKzaOTi1o2gk" 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="_MTJYwEHEEeqKzaOTi1o2gl" 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="_iY418EHGEeqHd7PiYTbxHg" org.eventb.core.generated="false" org.eventb.core.identifier="programmes"/>
<org.eventb.core.invariant name="_liiugEHGEeqHd7PiYTbxHg" org.eventb.core.generated="false" org.eventb.core.label="inv11" org.eventb.core.predicate="programmes ⊆ PROGRAMME"/>
<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.invariant name="_vOAHMEHGEeqHd7PiYTbxHg" org.eventb.core.comment="PRG9" org.eventb.core.generated="false" org.eventb.core.label="inv12" org.eventb.core.predicate="programme_leader ∈ programmes → registered"/>
<org.eventb.core.invariant name="_vOAHMUHGEeqHd7PiYTbxHg" org.eventb.core.comment="PRG10" org.eventb.core.generated="false" org.eventb.core.label="inv13" org.eventb.core.predicate="administrators ∈ programmes ↔ registered"/>
<org.eventb.core.variable name="_Uat4UEgQEeqeqbGZOOBkaQ" org.eventb.core.generated="false" org.eventb.core.identifier="published"/>
<org.eventb.core.invariant name="_Uat4UUgQEeqeqbGZOOBkaQ" org.eventb.core.generated="false" org.eventb.core.label="inv14" org.eventb.core.predicate="published ⊆ programmes"/>
</org.eventb.core.machineFile>