-
Notifications
You must be signed in to change notification settings - Fork 0
/
m7.bum
110 lines (110 loc) · 11.5 KB
/
m7.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
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<org.eventb.core.machineFile org.eventb.core.comment="Assign context to organization" org.eventb.core.configuration="org.eventb.core.fwd;ch.ethz.eventb.qualprob.qpConfig" version="5">
<org.eventb.core.refinesMachine name="'" org.eventb.core.target="m6"/>
<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.event name="_tdyf0hy0Ee61L_Ef0FP_Rv" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="INITIALISATION">
<org.eventb.core.action name="'" org.eventb.core.assignment="CiO1 ≔ ∅" org.eventb.core.label="act38"/>
</org.eventb.core.event>
<org.eventb.core.event name="_tdyf0hy0Ee61L_Ef0FP_Rw" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="Concrete_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 ≔ CiO1" org.eventb.core.generated="false" org.eventb.core.label="act1"/>
<org.eventb.core.action name="__StoEBy2Ee61L_Ef0FP_Qw" org.eventb.core.assignment="AiO ≔ AiO1" org.eventb.core.generated="false" org.eventb.core.label="act4"/>
<org.eventb.core.action name="_D2pGQBy3Ee61L_Ef0FP_Qw" org.eventb.core.assignment="ViO ≔ ViO1" org.eventb.core.generated="false" org.eventb.core.label="act6"/>
<org.eventb.core.action name="_td1jIhy0Ee61L_Ef0FP_R9" org.eventb.core.assignment="AV ≔ AV1" org.eventb.core.label="act16"/>
<org.eventb.core.action name="_td1jIhy0Ee61L_Ef0FP_R:" org.eventb.core.assignment="AA ≔ AA1" org.eventb.core.label="act17"/>
<org.eventb.core.action name="_td1jIhy0Ee61L_Ef0FP_R;" org.eventb.core.assignment="RV ≔ RV1" org.eventb.core.label="act18"/>
<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="_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.action name="_td1jIhy0Ee61L_Ef0FP_R+" org.eventb.core.assignment="EA ≔ EA1" org.eventb.core.label="act11"/>
<org.eventb.core.action name="_td1jIhy0Ee61L_Ef0FP_Q~" org.eventb.core.assignment="PCA ≔ PCA1" org.eventb.core.label="act9"/>
<org.eventb.core.action name="_td1jIhy0Ee61L_Ef0FP_R'" org.eventb.core.assignment="PRA ≔ PRA1" org.eventb.core.label="act10"/>
<org.eventb.core.action name="_td1jIhy0Ee61L_Ef0FP_R-" org.eventb.core.assignment="PAA ≔ PAA1" org.eventb.core.label="act13"/>
<org.eventb.core.action name="_td1jIhy0Ee61L_Ef0FP_R1" org.eventb.core.assignment="PVA ≔ PVA1" org.eventb.core.label="act14"/>
<org.eventb.core.action name="_td1jIhy0Ee61L_Ef0FP_R5" org.eventb.core.assignment="PCxA ≔ PCxA1" org.eventb.core.label="act15"/>
<org.eventb.core.action name="_PSi28By5Ee61L_Ef0FP_Qw" org.eventb.core.assignment="CA ≔ CA1" org.eventb.core.generated="false" org.eventb.core.label="act19"/>
<org.eventb.core.witness name="_td1jIhy0Ee61L_Ef0FP_RA" org.eventb.core.label="cio" org.eventb.core.predicate="cio = CiO1"/>
</org.eventb.core.event>
<org.eventb.core.event name="_tdyf0hy0Ee61L_Ef0FP_Rx" 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_Ry" 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_Rz" 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_R{" 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_R|" 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_R}" 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_R~" 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_S'" 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_S(" 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_S)" 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="false" org.eventb.core.label="Assign_Context_to_Organization">
<org.eventb.core.parameter name="'" org.eventb.core.identifier="org"/>
<org.eventb.core.parameter name="(" org.eventb.core.identifier="c"/>
<org.eventb.core.guard name=")" org.eventb.core.label="grd1" org.eventb.core.predicate="org ∈ ORG ∧ c ∈ CONTEXT"/>
<org.eventb.core.guard name="*" org.eventb.core.label="grd2" org.eventb.core.predicate="c↦org ∉ CiO1"/>
<org.eventb.core.action name="+" org.eventb.core.assignment="CiO1 ≔ CiO1 ∪ {c↦org}" org.eventb.core.label="act1"/>
</org.eventb.core.event>
<org.eventb.core.variable name="_tdyf0hy0Ee61L_Ef0FP_S-" org.eventb.core.identifier="CiO1"/>
<org.eventb.core.invariant name="_tdyf0hy0Ee61L_Ef0FP_S." org.eventb.core.label="inv1" org.eventb.core.predicate="CiO1 ⊆ CONTEXT × ORG"/>
</org.eventb.core.machineFile>