-
Notifications
You must be signed in to change notification settings - Fork 0
/
m8.bum
91 lines (91 loc) · 9.08 KB
/
m8.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
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<org.eventb.core.machineFile org.eventb.core.comment="Simple permission check without request" org.eventb.core.configuration="org.eventb.core.fwd;ch.ethz.eventb.qualprob.qpConfig" version="5">
<org.eventb.core.refinesMachine name="'" org.eventb.core.target="m7"/>
<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.variable name="_tdyf0hy0Ee61L_Ef0FP_R5" org.eventb.core.identifier="UR1"/>
<org.eventb.core.variable name="_tdyf0hy0Ee61L_Ef0FP_R9" org.eventb.core.identifier="RiO1"/>
<org.eventb.core.variable name="_tdyf0hy0Ee61L_Ef0FP_RC" org.eventb.core.identifier="EA1"/>
<org.eventb.core.variable name="_tdyf0hy0Ee61L_Ef0FP_RM" org.eventb.core.identifier="CA1"/>
<org.eventb.core.variable name="_tdyf0hy0Ee61L_Ef0FP_RQ" org.eventb.core.identifier="PRA1"/>
<org.eventb.core.variable name="_tdyf0hy0Ee61L_Ef0FP_RR" org.eventb.core.identifier="PAA1"/>
<org.eventb.core.variable name="_tdyf0hy0Ee61L_Ef0FP_RS" org.eventb.core.identifier="PVA1"/>
<org.eventb.core.variable name="_tdyf0hy0Ee61L_Ef0FP_RT" org.eventb.core.identifier="PCA1"/>
<org.eventb.core.variable name="_tdyf0hy0Ee61L_Ef0FP_RU" org.eventb.core.identifier="PCxA1"/>
<org.eventb.core.variable name="_tdyf0hy0Ee61L_Ef0FP_Ra" org.eventb.core.identifier="ViO1"/>
<org.eventb.core.variable name="_tdyf0hy0Ee61L_Ef0FP_Rd" org.eventb.core.identifier="RV1"/>
<org.eventb.core.variable name="_tdyf0hy0Ee61L_Ef0FP_Rs" org.eventb.core.identifier="AiO1"/>
<org.eventb.core.variable name="_tdyf0hy0Ee61L_Ef0FP_Rt" org.eventb.core.identifier="AA1"/>
<org.eventb.core.variable name="_tdyf0hy0Ee61L_Ef0FP_Ru" org.eventb.core.identifier="AV1"/>
<org.eventb.core.variable name="_tdyf0hy0Ee61L_Ef0FP_S-" org.eventb.core.identifier="CiO1"/>
<org.eventb.core.event name="_tdyf0hy0Ee61L_Ef0FP_S." org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="INITIALISATION"/>
<org.eventb.core.event name="_tdyf0hy0Ee61L_Ef0FP_S/" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="Concrete_Model_Generation">
<org.eventb.core.refinesEvent name="'" org.eventb.core.target="Concrete_Model_Generation"/>
</org.eventb.core.event>
<org.eventb.core.event name="_tdyf0hy0Ee61L_Ef0FP_S0" 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_S1" 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_S2" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="Assign_Unit_to_Org">
<org.eventb.core.refinesEvent name="'" org.eventb.core.target="Assign_Unit_to_Org"/>
</org.eventb.core.event>
<org.eventb.core.event name="_tdyf0hy0Ee61L_Ef0FP_S3" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="Assign_Role_to_Unit">
<org.eventb.core.refinesEvent name="'" org.eventb.core.target="Assign_Role_to_Unit"/>
</org.eventb.core.event>
<org.eventb.core.event name="_tdyf0hy0Ee61L_Ef0FP_S4" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="Assign_Role_to_Organization">
<org.eventb.core.refinesEvent name="'" org.eventb.core.target="Assign_Role_to_Organization"/>
</org.eventb.core.event>
<org.eventb.core.event name="_tdyf0hy0Ee61L_Ef0FP_S5" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="Assign_Employee−to_Unit">
<org.eventb.core.refinesEvent name="'" org.eventb.core.target="Assign_Employee−to_Unit"/>
</org.eventb.core.event>
<org.eventb.core.event name="_tdyf0hy0Ee61L_Ef0FP_S6" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="Assign_Approver">
<org.eventb.core.refinesEvent name="'" org.eventb.core.target="Assign_Approver"/>
</org.eventb.core.event>
<org.eventb.core.event name="_tdyf0hy0Ee61L_Ef0FP_S7" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="Define_Security_Rule">
<org.eventb.core.refinesEvent name="'" org.eventb.core.target="Define_Security_Rule"/>
</org.eventb.core.event>
<org.eventb.core.event name="_tdyf0hy0Ee61L_Ef0FP_S8" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="Assign_Resource_to_View">
<org.eventb.core.refinesEvent name="'" org.eventb.core.target="Assign_Resource_to_View"/>
</org.eventb.core.event>
<org.eventb.core.event name="_tdyf0hy0Ee61L_Ef0FP_S9" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="Assign_View_to_Organization">
<org.eventb.core.refinesEvent name="'" org.eventb.core.target="Assign_View_to_Organization"/>
</org.eventb.core.event>
<org.eventb.core.event name="_tdyf0hy0Ee61L_Ef0FP_S:" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="Assign_activity_to_Organization">
<org.eventb.core.refinesEvent name="'" org.eventb.core.target="Assign_activity_to_Organization"/>
</org.eventb.core.event>
<org.eventb.core.event name="_tdyf0hy0Ee61L_Ef0FP_S;" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="Assign_Action_to_Activity">
<org.eventb.core.refinesEvent name="'" org.eventb.core.target="Assign_Action_to_Activity"/>
</org.eventb.core.event>
<org.eventb.core.event name="_tdyf0hy0Ee61L_Ef0FP_S=" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="Assign_Context_to_Organization">
<org.eventb.core.refinesEvent name="'" org.eventb.core.target="Assign_Context_to_Organization"/>
</org.eventb.core.event>
<org.eventb.core.event name="_tdyf0hy0Ee61L_Ef0FP_S>" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="Can_Request_Access">
<org.eventb.core.parameter name="'" org.eventb.core.identifier="e"/>
<org.eventb.core.parameter name="(" org.eventb.core.identifier="a"/>
<org.eventb.core.parameter name=")" org.eventb.core.identifier="o"/>
<org.eventb.core.guard name="*" org.eventb.core.label="grd1" org.eventb.core.predicate="e∈EMPLOYEE ∧ a ∈ ACTION ∧ o ∈ RESOURCE"/>
<org.eventb.core.guard name="+" org.eventb.core.label="grd2" org.eventb.core.predicate="∃u, r, v, p, org, act, c, rio, aio, vio, cio · (e↦u) ∈ EA1 ∧ (u↦org) ∈ OU1 ∧ rio = (r↦org) ∧ rio ∈ RiO1 ∧ (u↦rio) ∈ UR1 ∧ (p↦rio) ∈ PRA1 ∧ vio = (v↦org) ∧ (o↦vio) ∈ RV1 ∧ (p↦vio) ∈ PVA1 ∧ aio = (act↦org) ∧ (p↦aio) ∈ PAA1 ∧ (a↦vio) ∈ AV ∧ (a↦aio) ∈ AA1 ∧ cio = (c↦org) ∧ (p↦cio) ∈ PCxA1 "/>
</org.eventb.core.event>
</org.eventb.core.machineFile>