-
Notifications
You must be signed in to change notification settings - Fork 0
/
fourtRef.bum
128 lines (128 loc) · 18.3 KB
/
fourtRef.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
121
122
123
124
125
126
127
128
<?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="1587926126312" org.eventb.texttools.text_representation="machine fourtRef refines thirdRef sees secondRef_ctx firstRef_ctx thirdRef_ctx sum_ctx variables max_busy_slots busy_slots max_bs_p // maximum espace/pont bs_p // espaces occupés/pont lift_level bs_m // busy_slot for lift reservations // all reservations reserved_spaces // function of space/floor auth_on_ids in_lift_ids boarded_ids queue1 queue2 lift_vehicles id_is_left lift_in // lift to bridges lift_out // ground to lift lvl_1_access lvl_2_access lvl_3_access lift_access invariants @inv1 lift_in ∈ BOOL @inv2 lift_out ∈ BOOL @inv3 lvl_1_access ∈ BOOL @inv4 lvl_2_access ∈ BOOL @inv5 lvl_3_access ∈ BOOL @inv6 lift_access ∈ BOOL events event INITIALISATION extends INITIALISATION then @act3 lift_in ≔ FALSE @act4 lift_out ≔ FALSE @act5 lvl_1_access ≔ FALSE @act6 lvl_2_access ≔ FALSE @act7 lvl_3_access ≔ FALSE @act8 lift_access ≔ FALSE end event Boat_ready extends Boat_ready end event Boat_leave extends Boat_leave end event Board extends Board end event Unboard extends Unboard end event MoveLift extends MoveLift where @grd1 lift_access = FALSE @grd2 lift_in = FALSE @grd3 lift_out = FALSE @grd4 lvl_1_access = FALSE @grd5 lvl_2_access = FALSE @grd6 lvl_3_access = FALSE end event BoardLift extends BoardLift end event LeaveLift extends LeaveLift end event Reserve extends Reserve end event Vehicle_auth_on extends Vehicle_auth_on end event Vehicle_in extends Vehicle_in end event Vehicle_out extends Vehicle_out end event Switch_lift_in any boolean where @grd1 (lift_in = TRUE) ⇒ boolean = FALSE @grd2 (lift_in = FALSE) ⇒ boolean = TRUE then @act1 lift_in ≔ boolean end event Switch_lift_out any boolean where @grd1 lift_level = 1 @grd2 (auth_on_ids = ∅) ⇒ boolean = FALSE @grd3 (auth_on_ids ≠ ∅) ⇒ boolean = TRUE @grd4 boolean ≠ lift_out then @act1 lift_out ≔ boolean end event Switch_lvl_1_access any boolean where @grd1 (lvl_1_access = FALSE) ⇒ boolean = TRUE @grd2 (lvl_1_access = TRUE) ⇒ boolean = FALSE @grd3 lift_level = 1 then @act1 lvl_1_access ≔ boolean end event Switch_lvl_2_access any boolean where @grd1 (lvl_2_access = FALSE) ⇒ boolean = TRUE @grd2 (lvl_2_access = TRUE) ⇒ boolean = FALSE @grd3 lift_level = 2 then @act1 lvl_2_access ≔ boolean end event Switch_lvl_3_access any boolean where @grd1 (lvl_3_access = FALSE) ⇒ boolean = TRUE @grd2 (lvl_3_access = FALSE) ⇒ boolean = TRUE @grd3 lift_level = 3 then @act1 lvl_3_access ≔ boolean end event Switch_lift_access any boolean where @grd1 lift_level = 1 @grd2 (auth_on_ids = ∅) ⇒ boolean = FALSE @grd3 (auth_on_ids ≠ ∅) ⇒ boolean = TRUE @grd4 boolean ≠ lift_access then @act1 lift_access ≔ boolean end end " version="5">
<org.eventb.core.refinesMachine name="'" org.eventb.core.target="thirdRef"/>
<org.eventb.core.seesContext name="V" org.eventb.core.target="secondRef_ctx"/>
<org.eventb.core.seesContext name="`" org.eventb.core.target="firstRef_ctx"/>
<org.eventb.core.seesContext name="}" org.eventb.core.target="thirdRef_ctx"/>
<org.eventb.core.variable name="(" org.eventb.core.generated="false" org.eventb.core.identifier="max_busy_slots"/>
<org.eventb.core.variable name="+" org.eventb.core.generated="false" org.eventb.core.identifier="busy_slots"/>
<org.eventb.core.variable name="1" org.eventb.core.comment="maximum espace/pont" org.eventb.core.generated="false" org.eventb.core.identifier="max_bs_p"/>
<org.eventb.core.variable name="@" org.eventb.core.comment="espaces occupés/pont" org.eventb.core.generated="false" org.eventb.core.identifier="bs_p"/>
<org.eventb.core.variable name="E" org.eventb.core.generated="false" org.eventb.core.identifier="lift_level"/>
<org.eventb.core.variable name="K" org.eventb.core.comment="busy_slot for lift" org.eventb.core.generated="false" org.eventb.core.identifier="bs_m"/>
<org.eventb.core.variable name="W" org.eventb.core.comment="all reservations" org.eventb.core.generated="false" org.eventb.core.identifier="reservations"/>
<org.eventb.core.variable name="a" org.eventb.core.comment="function of space/floor" org.eventb.core.generated="false" org.eventb.core.identifier="reserved_spaces"/>
<org.eventb.core.variable name="d" org.eventb.core.generated="false" org.eventb.core.identifier="auth_on_ids"/>
<org.eventb.core.variable name="~" org.eventb.core.generated="false" org.eventb.core.identifier="in_lift_ids"/>
<org.eventb.core.variable name="o" org.eventb.core.generated="false" org.eventb.core.identifier="boarded_ids"/>
<org.eventb.core.variable name="q" org.eventb.core.generated="false" org.eventb.core.identifier="queue1"/>
<org.eventb.core.variable name="s" org.eventb.core.generated="false" org.eventb.core.identifier="queue2"/>
<org.eventb.core.variable name="w" org.eventb.core.generated="false" org.eventb.core.identifier="lift_vehicles"/>
<org.eventb.core.variable name="{" org.eventb.core.generated="false" org.eventb.core.identifier="id_is_left"/>
<org.eventb.core.event name="''" 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="'" org.eventb.core.assignment="lift_in ≔ FALSE" org.eventb.core.generated="false" org.eventb.core.label="act3"/>
<org.eventb.core.action name="(" org.eventb.core.assignment="lift_out ≔ FALSE" org.eventb.core.generated="false" org.eventb.core.label="act4"/>
<org.eventb.core.action name=")" org.eventb.core.assignment="lvl_1_access ≔ FALSE" org.eventb.core.generated="false" org.eventb.core.label="act5"/>
<org.eventb.core.action name="*" org.eventb.core.assignment="lvl_2_access ≔ FALSE" org.eventb.core.generated="false" org.eventb.core.label="act6"/>
<org.eventb.core.action name="+" org.eventb.core.assignment="lvl_3_access ≔ FALSE" org.eventb.core.generated="false" org.eventb.core.label="act7"/>
<org.eventb.core.action name="," org.eventb.core.assignment="lift_access ≔ FALSE" org.eventb.core.generated="false" org.eventb.core.label="act8"/>
</org.eventb.core.event>
<org.eventb.core.event name="'(" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.generated="false" org.eventb.core.label="Boat_ready">
<org.eventb.core.refinesEvent name="'" org.eventb.core.target="Boat_ready"/>
</org.eventb.core.event>
<org.eventb.core.event name="')" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.generated="false" org.eventb.core.label="Boat_leave">
<org.eventb.core.refinesEvent name="'" org.eventb.core.target="Boat_leave"/>
</org.eventb.core.event>
<org.eventb.core.event name="'*" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.generated="false" org.eventb.core.label="Board">
<org.eventb.core.refinesEvent name="'" org.eventb.core.target="Board"/>
<org.eventb.core.guard name="(" org.eventb.core.label="grd1" org.eventb.core.predicate="lift_out = TRUE"/>
<org.eventb.core.guard name=")" org.eventb.core.label="grd2" org.eventb.core.predicate="(lift_level = 1) ⇒ lvl_1_access = TRUE"/>
<org.eventb.core.guard name="*" org.eventb.core.label="grd3" org.eventb.core.predicate="(lift_level = 2) ⇒ lvl_2_access = TRUE"/>
<org.eventb.core.guard name="+" org.eventb.core.label="grd4" org.eventb.core.predicate="(lift_level = 3) ⇒ lvl_3_access = TRUE"/>
</org.eventb.core.event>
<org.eventb.core.event name="'+" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.generated="false" org.eventb.core.label="Unboard">
<org.eventb.core.refinesEvent name="'" org.eventb.core.target="Unboard"/>
<org.eventb.core.guard name="(" org.eventb.core.label="grd1" org.eventb.core.predicate="lift_out = TRUE"/>
<org.eventb.core.guard name=")" org.eventb.core.label="grd2" org.eventb.core.predicate="(lift_level = 1) ⇒ lvl_1_access = TRUE"/>
<org.eventb.core.guard name="*" org.eventb.core.label="grd3" org.eventb.core.predicate="(lift_level = 2) ⇒ lvl_2_access = TRUE"/>
<org.eventb.core.guard name="+" org.eventb.core.label="grd4" org.eventb.core.predicate="(lift_level = 3) ⇒ lvl_3_access = TRUE"/>
</org.eventb.core.event>
<org.eventb.core.event name="'," org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.generated="false" org.eventb.core.label="MoveLift">
<org.eventb.core.refinesEvent name="'" org.eventb.core.target="MoveLift"/>
<org.eventb.core.guard name="(" org.eventb.core.generated="false" org.eventb.core.label="grd1" org.eventb.core.predicate="lift_access = FALSE"/>
<org.eventb.core.guard name=")" org.eventb.core.generated="false" org.eventb.core.label="grd2" org.eventb.core.predicate="lift_in = FALSE"/>
<org.eventb.core.guard name="+" org.eventb.core.generated="false" org.eventb.core.label="grd3" org.eventb.core.predicate="lift_out = FALSE"/>
<org.eventb.core.guard name="," org.eventb.core.generated="false" org.eventb.core.label="grd4" org.eventb.core.predicate="lvl_1_access = FALSE"/>
<org.eventb.core.guard name="-" org.eventb.core.generated="false" org.eventb.core.label="grd5" org.eventb.core.predicate="lvl_2_access = FALSE"/>
<org.eventb.core.guard name="." org.eventb.core.generated="false" org.eventb.core.label="grd6" org.eventb.core.predicate="lvl_3_access = FALSE"/>
</org.eventb.core.event>
<org.eventb.core.event name="'-" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.generated="false" org.eventb.core.label="BoardLift">
<org.eventb.core.refinesEvent name="'" org.eventb.core.target="BoardLift"/>
<org.eventb.core.guard name="(" org.eventb.core.label="grd1" org.eventb.core.predicate="lift_access = TRUE"/>
<org.eventb.core.guard name=")" org.eventb.core.label="grd2" org.eventb.core.predicate="lift_in = TRUE"/>
</org.eventb.core.event>
<org.eventb.core.event name="'." org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.generated="false" org.eventb.core.label="LeaveLift">
<org.eventb.core.refinesEvent name="'" org.eventb.core.target="LeaveLift"/>
<org.eventb.core.guard name="(" org.eventb.core.label="grd1" org.eventb.core.predicate="lift_access = TRUE"/>
<org.eventb.core.guard name=")" org.eventb.core.label="grd2" org.eventb.core.predicate="lift_in = TRUE"/>
</org.eventb.core.event>
<org.eventb.core.event name="'/" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.generated="false" org.eventb.core.label="Reserve">
<org.eventb.core.refinesEvent name="'" org.eventb.core.target="Reserve"/>
</org.eventb.core.event>
<org.eventb.core.event name="'0" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.generated="false" org.eventb.core.label="Vehicle_auth_on">
<org.eventb.core.refinesEvent name="'" org.eventb.core.target="Vehicle_auth_on"/>
</org.eventb.core.event>
<org.eventb.core.event name="'1" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.generated="false" org.eventb.core.label="Vehicle_in">
<org.eventb.core.refinesEvent name="'" org.eventb.core.target="Vehicle_in"/>
</org.eventb.core.event>
<org.eventb.core.event name="'2" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.generated="false" org.eventb.core.label="Vehicle_out">
<org.eventb.core.refinesEvent name="'" org.eventb.core.target="Vehicle_out"/>
</org.eventb.core.event>
<org.eventb.core.variable name="'3" org.eventb.core.comment="ground to lift" org.eventb.core.generated="false" org.eventb.core.identifier="lift_in"/>
<org.eventb.core.variable name="'4" org.eventb.core.comment="lift to bridges" org.eventb.core.generated="false" org.eventb.core.identifier="lift_out"/>
<org.eventb.core.invariant name="'5" org.eventb.core.generated="false" org.eventb.core.label="inv1" org.eventb.core.predicate="lift_in ∈ BOOL"/>
<org.eventb.core.invariant name="'6" org.eventb.core.generated="false" org.eventb.core.label="inv2" org.eventb.core.predicate="lift_out ∈ BOOL"/>
<org.eventb.core.event name="'7" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.generated="false" org.eventb.core.label="Switch_lift_out">
<org.eventb.core.parameter name="'" org.eventb.core.generated="false" org.eventb.core.identifier="boolean"/>
<org.eventb.core.guard name="(" org.eventb.core.generated="false" org.eventb.core.label="grd1" org.eventb.core.predicate="boolean ≠ lift_out ∧ boolean ∈ BOOL"/>
<org.eventb.core.action name="*" org.eventb.core.assignment="lift_out ≔ boolean" org.eventb.core.generated="false" org.eventb.core.label="act1"/>
</org.eventb.core.event>
<org.eventb.core.event name="'8" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.generated="false" org.eventb.core.label="Switch_lift_in">
<org.eventb.core.parameter name="'" org.eventb.core.generated="false" org.eventb.core.identifier="boolean"/>
<org.eventb.core.guard name="(" org.eventb.core.generated="false" org.eventb.core.label="grd1" org.eventb.core.predicate="lift_level = 1"/>
<org.eventb.core.action name="+" org.eventb.core.assignment="lift_in ≔ boolean" org.eventb.core.generated="false" org.eventb.core.label="act1"/>
<org.eventb.core.guard name="," org.eventb.core.generated="false" org.eventb.core.label="grd2" org.eventb.core.predicate="boolean ≠ lift_in ∧ boolean ∈ BOOL"/>
</org.eventb.core.event>
<org.eventb.core.variable name="'9" org.eventb.core.generated="false" org.eventb.core.identifier="lvl_1_access"/>
<org.eventb.core.variable name="':" org.eventb.core.generated="false" org.eventb.core.identifier="lvl_2_access"/>
<org.eventb.core.variable name="';" org.eventb.core.generated="false" org.eventb.core.identifier="lvl_3_access"/>
<org.eventb.core.invariant name="'=" org.eventb.core.generated="false" org.eventb.core.label="inv3" org.eventb.core.predicate="lvl_1_access ∈ BOOL"/>
<org.eventb.core.invariant name="'>" org.eventb.core.generated="false" org.eventb.core.label="inv4" org.eventb.core.predicate="lvl_2_access ∈ BOOL"/>
<org.eventb.core.invariant name="'?" org.eventb.core.generated="false" org.eventb.core.label="inv5" org.eventb.core.predicate="lvl_3_access ∈ BOOL"/>
<org.eventb.core.event name="'@" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.generated="false" org.eventb.core.label="Switch_lvl_1_access">
<org.eventb.core.parameter name="'" org.eventb.core.generated="false" org.eventb.core.identifier="boolean"/>
<org.eventb.core.guard name="(" org.eventb.core.generated="false" org.eventb.core.label="grd1" org.eventb.core.predicate="boolean ∈ BOOL ∧ boolean ≠ lvl_1_access"/>
<org.eventb.core.action name="*" org.eventb.core.assignment="lvl_1_access ≔ boolean" org.eventb.core.generated="false" org.eventb.core.label="act1"/>
<org.eventb.core.guard name="+" org.eventb.core.generated="false" org.eventb.core.label="grd2" org.eventb.core.predicate="lift_level = 1"/>
</org.eventb.core.event>
<org.eventb.core.event name="'A" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.generated="false" org.eventb.core.label="Switch_lvl_2_access">
<org.eventb.core.parameter name="'" org.eventb.core.generated="false" org.eventb.core.identifier="boolean"/>
<org.eventb.core.guard name="(" org.eventb.core.generated="false" org.eventb.core.label="grd1" org.eventb.core.predicate="boolean ∈ BOOL ∧ boolean ≠ lvl_2_access"/>
<org.eventb.core.action name="*" org.eventb.core.assignment="lvl_2_access ≔ boolean" org.eventb.core.generated="false" org.eventb.core.label="act1"/>
<org.eventb.core.guard name="+" org.eventb.core.generated="false" org.eventb.core.label="grd2" org.eventb.core.predicate="lift_level = 2"/>
</org.eventb.core.event>
<org.eventb.core.event name="'B" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.generated="false" org.eventb.core.label="Switch_lvl_3_access">
<org.eventb.core.parameter name="'" org.eventb.core.generated="false" org.eventb.core.identifier="boolean"/>
<org.eventb.core.guard name="(" org.eventb.core.generated="false" org.eventb.core.label="grd1" org.eventb.core.predicate="boolean ∈ BOOL ∧ boolean ≠ lvl_3_access"/>
<org.eventb.core.action name="*" org.eventb.core.assignment="lvl_3_access ≔ boolean" org.eventb.core.generated="false" org.eventb.core.label="act1"/>
<org.eventb.core.guard name="+" org.eventb.core.generated="false" org.eventb.core.label="grd2" org.eventb.core.predicate="lift_level = 3"/>
</org.eventb.core.event>
<org.eventb.core.variable name="'C" org.eventb.core.generated="false" org.eventb.core.identifier="lift_access"/>
<org.eventb.core.invariant name="'D" org.eventb.core.generated="false" org.eventb.core.label="inv6" org.eventb.core.predicate="lift_access ∈ BOOL"/>
<org.eventb.core.event name="'E" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.generated="false" org.eventb.core.label="Switch_lift_access">
<org.eventb.core.parameter name="'" org.eventb.core.generated="false" org.eventb.core.identifier="boolean"/>
<org.eventb.core.guard name="(" org.eventb.core.generated="false" org.eventb.core.label="grd1" org.eventb.core.predicate="lift_level = 1"/>
<org.eventb.core.guard name="+" org.eventb.core.generated="false" org.eventb.core.label="grd2" org.eventb.core.predicate="boolean ∈ BOOL ∧ boolean ≠ lift_access"/>
<org.eventb.core.action name="," org.eventb.core.assignment="lift_access ≔ boolean" org.eventb.core.generated="false" org.eventb.core.label="act1"/>
</org.eventb.core.event>
</org.eventb.core.machineFile>