-
Notifications
You must be signed in to change notification settings - Fork 0
/
m2.bum
115 lines (115 loc) · 13.2 KB
/
m2.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
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<org.eventb.core.machineFile org.eventb.core.comment="Assign Role to organization and unit to role" org.eventb.core.configuration="org.eventb.core.fwd;ch.ethz.eventb.qualprob.qpConfig" version="5">
<org.eventb.core.refinesMachine name="'" org.eventb.core.target="m1"/>
<org.eventb.core.seesContext name="_tdtnUBy0Ee61L_Ef0FP_Qw" org.eventb.core.target="c0"/>
<org.eventb.core.variable name="_tdwqoRy0Ee61L_Ef0FP_Qw" org.eventb.core.identifier="CA"/>
<org.eventb.core.variable name="_tdwqohy0Ee61L_Ef0FP_Qw" org.eventb.core.identifier="PCA"/>
<org.eventb.core.variable name="_tdwqoxy0Ee61L_Ef0FP_Qw" org.eventb.core.identifier="root"/>
<org.eventb.core.variable name="_tdwqpBy0Ee61L_Ef0FP_Qw" org.eventb.core.identifier="OU"/>
<org.eventb.core.variable name="_tdxRsBy0Ee61L_Ef0FP_Qw" org.eventb.core.identifier="RiO"/>
<org.eventb.core.variable name="_tdyf0hy0Ee61L_Ef0FP_R*" org.eventb.core.identifier="UH"/>
<org.eventb.core.variable name="_tdxRsRy0Ee61L_Ef0FP_Qw" org.eventb.core.identifier="PRA"/>
<org.eventb.core.variable name="_tdxRshy0Ee61L_Ef0FP_Qw" org.eventb.core.identifier="EA"/>
<org.eventb.core.variable name="_tdxRtBy0Ee61L_Ef0FP_Qw" org.eventb.core.identifier="ViO"/>
<org.eventb.core.variable name="_tdx4wBy0Ee61L_Ef0FP_Qw" org.eventb.core.identifier="AiO"/>
<org.eventb.core.variable name="_tdyf0hy0Ee61L_Ef0FP_R7" org.eventb.core.identifier="UR"/>
<org.eventb.core.variable name="_tdx4wRy0Ee61L_Ef0FP_Qw" org.eventb.core.identifier="PAA"/>
<org.eventb.core.variable name="_tdx4why0Ee61L_Ef0FP_Qw" org.eventb.core.identifier="PVA"/>
<org.eventb.core.variable name="_tdx4wxy0Ee61L_Ef0FP_Qw" org.eventb.core.identifier="CiO"/>
<org.eventb.core.variable name="_tdx4xBy0Ee61L_Ef0FP_Qw" org.eventb.core.identifier="PCxA"/>
<org.eventb.core.variable name="_tdyf0By0Ee61L_Ef0FP_Qw" org.eventb.core.identifier="RV"/>
<org.eventb.core.variable name="_tdyf0Ry0Ee61L_Ef0FP_Qw" org.eventb.core.identifier="AV"/>
<org.eventb.core.variable name="_tdyf0hy0Ee61L_Ef0FP_Qw" org.eventb.core.identifier="AA"/>
<org.eventb.core.variable name="_tdyf0hy0Ee61L_Ef0FP_Q{" org.eventb.core.identifier="root1"/>
<org.eventb.core.variable name="_tdyf0hy0Ee61L_Ef0FP_R(" org.eventb.core.identifier="UH1"/>
<org.eventb.core.variable name="_tdyf0hy0Ee61L_Ef0FP_R." org.eventb.core.identifier="OU1"/>
<org.eventb.core.event name="_tdyf0hy0Ee61L_Ef0FP_R/" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="INITIALISATION">
<org.eventb.core.action name="_tdwDkhy0Ee61L_Ef0FP_Q|" org.eventb.core.assignment="UR1 ≔ ∅" org.eventb.core.label="act24"/>
<org.eventb.core.action name="_tdwDkhy0Ee61L_Ef0FP_Q}" org.eventb.core.assignment="RiO1 ≔ ∅" org.eventb.core.label="act25"/>
</org.eventb.core.event>
<org.eventb.core.event name="_tdyf0hy0Ee61L_Ef0FP_R0" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="Abstract_Model_Generation">
<org.eventb.core.refinesEvent name="'" org.eventb.core.target="Abstract_Model_Generation"/>
<org.eventb.core.action name="_td1jIBy0Ee61L_Ef0FP_Qw" org.eventb.core.assignment="CiO ≔ cio" org.eventb.core.generated="false" org.eventb.core.label="act1"/>
<org.eventb.core.action name="__StoEBy2Ee61L_Ef0FP_Qw" org.eventb.core.assignment="AiO ≔ aio" org.eventb.core.generated="false" org.eventb.core.label="act4"/>
<org.eventb.core.action name="_D2pGQBy3Ee61L_Ef0FP_Qw" org.eventb.core.assignment="ViO ≔ vio" org.eventb.core.generated="false" org.eventb.core.label="act6"/>
<org.eventb.core.action name="internal4" org.eventb.core.assignment="PCA ≔ pca" org.eventb.core.label="act9"/>
<org.eventb.core.action name="internal5" org.eventb.core.assignment="PRA ≔ pra" org.eventb.core.label="act10"/>
<org.eventb.core.action name="_td1jIhy0Ee61L_Ef0FP_R+" org.eventb.core.assignment="EA ≔ ea" org.eventb.core.label="act11"/>
<org.eventb.core.action name="internal7" org.eventb.core.assignment="PAA ≔ paa" org.eventb.core.label="act13"/>
<org.eventb.core.parameter name="_td1jIhy0Ee61L_Ef0FP_R." org.eventb.core.identifier="aio"/>
<org.eventb.core.guard name="_td1jIhy0Ee61L_Ef0FP_R/" org.eventb.core.label="grd4" org.eventb.core.predicate="aio ∈ ℙ(ACTIVITY × ORG)"/>
<org.eventb.core.action name="internal8" org.eventb.core.assignment="PVA ≔ pva" org.eventb.core.label="act14"/>
<org.eventb.core.guard name="_td1jIhy0Ee61L_Ef0FP_R2" org.eventb.core.label="grd5" org.eventb.core.predicate="vio ⊆ VIEW × ORG"/>
<org.eventb.core.parameter name="_td1jIhy0Ee61L_Ef0FP_R3" org.eventb.core.identifier="vio"/>
<org.eventb.core.action name="internal9" org.eventb.core.assignment="PCxA ≔ pcxa" org.eventb.core.label="act15"/>
<org.eventb.core.guard name="_td1jIhy0Ee61L_Ef0FP_R6" org.eventb.core.label="grd6" org.eventb.core.predicate="cio ⊆ CONTEXT × ORG"/>
<org.eventb.core.parameter name="_td1jIhy0Ee61L_Ef0FP_R7" org.eventb.core.identifier="cio"/>
<org.eventb.core.action name="_td1jIhy0Ee61L_Ef0FP_R9" org.eventb.core.assignment="AV ≔ av" org.eventb.core.label="act16"/>
<org.eventb.core.action name="_td1jIhy0Ee61L_Ef0FP_R:" org.eventb.core.assignment="AA ≔ aa" org.eventb.core.label="act17"/>
<org.eventb.core.action name="_td1jIhy0Ee61L_Ef0FP_R;" org.eventb.core.assignment="RV ≔ rv" org.eventb.core.label="act18"/>
<org.eventb.core.guard name="_td1jIhy0Ee61L_Ef0FP_R>" org.eventb.core.label="grd8" org.eventb.core.predicate="ea ⊆ EMPLOYEE × UNIT"/>
<org.eventb.core.guard name="_td1jIhy0Ee61L_Ef0FP_R@" org.eventb.core.label="grd10" org.eventb.core.predicate="cio ⊆ CONTEXT × ORG"/>
<org.eventb.core.parameter name="_td1jIhy0Ee61L_Ef0FP_RC" org.eventb.core.identifier="ea"/>
<org.eventb.core.guard name="_td1jIhy0Ee61L_Ef0FP_RI" org.eventb.core.label="grd13" org.eventb.core.predicate="av ⊆ ACTION × vio"/>
<org.eventb.core.guard name="_td1jIhy0Ee61L_Ef0FP_RJ" org.eventb.core.label="grd14" org.eventb.core.predicate="aa ⊆ ACTION × aio"/>
<org.eventb.core.guard name="_td1jIhy0Ee61L_Ef0FP_RK" org.eventb.core.label="grd15" org.eventb.core.predicate="rv ⊆ RESOURCE × vio"/>
<org.eventb.core.parameter name="_td1jIhy0Ee61L_Ef0FP_RL" org.eventb.core.identifier="aa"/>
<org.eventb.core.parameter name="_td1jIhy0Ee61L_Ef0FP_RM" org.eventb.core.identifier="av"/>
<org.eventb.core.parameter name="_td1jIhy0Ee61L_Ef0FP_RN" org.eventb.core.identifier="rv"/>
<org.eventb.core.parameter name="_td1jIhy0Ee61L_Ef0FP_RP" org.eventb.core.identifier="ca"/>
<org.eventb.core.guard name="_td1jIhy0Ee61L_Ef0FP_RQ" org.eventb.core.label="grd17" org.eventb.core.predicate="pra ∈ PERMISSION ⇸ RiO1"/>
<org.eventb.core.guard name="_td1jIhy0Ee61L_Ef0FP_RR" org.eventb.core.label="grd18" org.eventb.core.predicate="paa ∈ PERMISSION ⇸ aio"/>
<org.eventb.core.guard name="internal1" org.eventb.core.label="grd19" org.eventb.core.predicate="pva ∈ PERMISSION ⇸ vio"/>
<org.eventb.core.guard name="_td1jIhy0Ee61L_Ef0FP_RT" org.eventb.core.label="grd20" org.eventb.core.predicate="pcxa ∈ PERMISSION ⇸ cio"/>
<org.eventb.core.guard name="_td1jIhy0Ee61L_Ef0FP_RU" org.eventb.core.label="grd21" org.eventb.core.predicate="pca ∈ PERMISSION ⇸ COR"/>
<org.eventb.core.parameter name="_td1jIhy0Ee61L_Ef0FP_RV" org.eventb.core.identifier="pra"/>
<org.eventb.core.parameter name="_td1jIhy0Ee61L_Ef0FP_RW" org.eventb.core.identifier="paa"/>
<org.eventb.core.parameter name="_td1jIhy0Ee61L_Ef0FP_RX" org.eventb.core.identifier="pva"/>
<org.eventb.core.parameter name="_td1jIhy0Ee61L_Ef0FP_RY" org.eventb.core.identifier="pca"/>
<org.eventb.core.parameter name="_td1jIhy0Ee61L_Ef0FP_RZ" org.eventb.core.identifier="pcxa"/>
<org.eventb.core.action name="_td1jIRy0Ee61L_Ef0FP_Qw" org.eventb.core.assignment="root ≔ root1" org.eventb.core.generated="false" org.eventb.core.label="act2"/>
<org.eventb.core.action name="_BFqMYBy3Ee61L_Ef0FP_Qw" org.eventb.core.assignment="UH ≔ UH1" org.eventb.core.generated="false" org.eventb.core.label="act5"/>
<org.eventb.core.action name="_PSi28By5Ee61L_Ef0FP_Qw" org.eventb.core.assignment="CA ≔ ca" org.eventb.core.generated="false" org.eventb.core.label="act8"/>
<org.eventb.core.action name="_td1jIhy0Ee61L_Ef0FP_Qw" org.eventb.core.assignment="OU ≔ OU1" org.eventb.core.generated="false" org.eventb.core.label="act3"/>
<org.eventb.core.action name="_aKm3kBy3Ee61L_Ef0FP_Qw" org.eventb.core.assignment="RiO ≔ RiO1" org.eventb.core.generated="false" org.eventb.core.label="act7"/>
<org.eventb.core.action name="_td1jIhy0Ee61L_Ef0FP_R," org.eventb.core.assignment="UR ≔ UR1" org.eventb.core.label="act12"/>
<org.eventb.core.witness name="_td1jIhy0Ee61L_Ef0FP_RO" org.eventb.core.label="ur" org.eventb.core.predicate="ur = UR1 "/>
<org.eventb.core.witness name="_td1jIhy0Ee61L_Ef0FP_RP" org.eventb.core.comment="parameter susbtitution using witness" org.eventb.core.label="rio" org.eventb.core.predicate="rio = RiO1"/>
<org.eventb.core.witness name="_td1jIhy0Ee61L_Ef0FP_RQ" org.eventb.core.label="ou" org.eventb.core.predicate="ou = OU1"/>
<org.eventb.core.guard name="_td1jIhy0Ee61L_Ef0FP_RS" org.eventb.core.label="grd16" org.eventb.core.predicate="ca ⊆ COR × UNIT × POSITION × DEADLINE"/>
</org.eventb.core.event>
<org.eventb.core.event name="_tdyf0hy0Ee61L_Ef0FP_R1" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="Assign_Oragnization_Root">
<org.eventb.core.refinesEvent name="'" org.eventb.core.target="Assign_Oragnization_Root"/>
</org.eventb.core.event>
<org.eventb.core.event name="_tdyf0hy0Ee61L_Ef0FP_R2" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="Add_Unit_Hierarchy">
<org.eventb.core.refinesEvent name="'" org.eventb.core.target="Add_Unit_Hierarchy"/>
</org.eventb.core.event>
<org.eventb.core.event name="_tdyf0hy0Ee61L_Ef0FP_R3" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="Assign_Unit_to_Org">
<org.eventb.core.refinesEvent name="'" org.eventb.core.target="Assign_Unit_to_Org"/>
<org.eventb.core.parameter name="'" org.eventb.core.identifier="u"/>
<org.eventb.core.parameter name="(" org.eventb.core.identifier="org"/>
<org.eventb.core.guard name=")" org.eventb.core.label="grd1" org.eventb.core.predicate="u ↦ org ∉ OU1 "/>
<org.eventb.core.action name="*" org.eventb.core.assignment="OU1 ≔ OU1 ∪ {u↦org}" org.eventb.core.label="act1"/>
<org.eventb.core.guard name="+" org.eventb.core.label="grd2" org.eventb.core.predicate="u ∉ dom(OU1)"/>
<org.eventb.core.guard name="," org.eventb.core.label="grd3" org.eventb.core.predicate="∀ org1 , role · u↦(role↦org1) ∈ UR1 ⇒ org = org1"/>
</org.eventb.core.event>
<org.eventb.core.event name="_tdyf0hy0Ee61L_Ef0FP_R4" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="Assign_Role_to_Unit">
<org.eventb.core.parameter name="'" org.eventb.core.identifier="r"/>
<org.eventb.core.parameter name="(" org.eventb.core.identifier="u"/>
<org.eventb.core.action name=")" org.eventb.core.assignment="UR1 ≔ UR1 ∪ {(u↦r)}" org.eventb.core.label="act1"/>
<org.eventb.core.guard name="*" org.eventb.core.label="grd1" org.eventb.core.predicate="r ∈ RiO1 ∧ u ∈ UNIT ∧ (u↦r) ∉ UR1"/>
<org.eventb.core.guard name="." org.eventb.core.label="grd2" org.eventb.core.predicate="∀ role, org · r = role ↦ org ⇒ (OU1[{u}] ≠ ∅ ⇒ OU1(u) = org)"/>
</org.eventb.core.event>
<org.eventb.core.variable name="_tdyf0hy0Ee61L_Ef0FP_R5" org.eventb.core.identifier="UR1"/>
<org.eventb.core.invariant name="_tdyf0hy0Ee61L_Ef0FP_R:" org.eventb.core.label="inv1" org.eventb.core.predicate="RiO1 ⊆ ROLE × ORG"/>
<org.eventb.core.invariant name="_tdyf0hy0Ee61L_Ef0FP_R6" org.eventb.core.label="inv2" org.eventb.core.predicate="UR1 ⊆ UNIT × RiO1"/>
<org.eventb.core.event name="_tdyf0hy0Ee61L_Ef0FP_R8" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="Assign_Role_to_Organization">
<org.eventb.core.parameter name="'" org.eventb.core.identifier="r"/>
<org.eventb.core.parameter name="(" org.eventb.core.identifier="org"/>
<org.eventb.core.guard name=")" org.eventb.core.label="grd1" org.eventb.core.predicate="r ∈ ROLE ∧ org∈ORG "/>
<org.eventb.core.action name="*" org.eventb.core.assignment="RiO1 ≔ RiO1 ∪ {r↦org}" org.eventb.core.label="act1"/>
<org.eventb.core.guard name="+" org.eventb.core.label="grd2" org.eventb.core.predicate="r↦org ∉ RiO1"/>
</org.eventb.core.event>
<org.eventb.core.variable name="_tdyf0hy0Ee61L_Ef0FP_R9" org.eventb.core.identifier="RiO1"/>
<org.eventb.core.invariant name="_tdyf0hy0Ee61L_Ef0FP_R;" org.eventb.core.comment="organization conservation" org.eventb.core.label="inv3" org.eventb.core.predicate="∀ u, org, role· u↦(role↦org) ∈ UR1 ⇒(OU1[{u}] ≠ ∅ ⇒ OU1(u) = org)"/>
</org.eventb.core.machineFile>