-
Notifications
You must be signed in to change notification settings - Fork 1
/
Copy pathm4_buttons.bum
79 lines (79 loc) · 15.1 KB
/
m4_buttons.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
<?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="1590749506815" org.eventb.texttools.text_representation="machine m4_buttons refines m3_door sees m4_buttons_context variables floor shaft motor door cabin_schedule floor_schedule invariants @cabin_schedule_type cabin_schedule ∈ CABINS ↔ FLOORS //REQ 13 @floor_schedule_type floor_schedule ∈ FLOORS ↔ SHAFTS events event INITIALISATION extends INITIALISATION then @cabin_schedule_init cabin_schedule ≔ ∅ @floor_schedule_init floor_schedule ≔ ∅ end event CabinMovesUp extends CabinMovesUp where @request_exists cabin_schedule ≠ ∅ ∨ floor_schedule ≠ ∅ //there is some request @REQ14 (floor(cabin) ∉ cabin_schedule[{cabin}]) 	∧ ((∃f·f = floor(cabin) ∧ UP ∉ floor_schedule[{f}]) 		∨ (∃c·c ∈ dom(cabin_schedule) ∧ (∃f·f ∈ cabin_schedule[{c}] ∧ f ≥ floor(cabin)))) //the current floor is not requested from inside //..AND not requested from outside //....OR the cabin is blocking the path of another end event CabinMovesDown extends CabinMovesDown where @request_exists cabin_schedule ≠ ∅ ∨ floor_schedule ≠ ∅ //there is some request @REQ14 (floor(cabin) ∉ cabin_schedule[{cabin}]) 	∧ ((∃f·f = floor(cabin) ∧ DOWN ∉ floor_schedule[{f}]) 		∨ (∃c·c ∈ dom(cabin_schedule) ∧ (∃f·f ∈ cabin_schedule[{c}] ∧ f ≤ floor(cabin)))) //the current floor is not requested from inside //..AND not requested from outside //....OR the cabin is blocking the path of another end event CabinDownToUp extends CabinDownToUp where @REQ14 ∀c·c ∈ dom(cabin_schedule) ∧ shaft(c) = DOWN ⇒ 0 ∉ cabin_schedule[{c}] end event CabinUpToDown extends CabinUpToDown where @REQ14 ∀c·c ∈ dom(cabin_schedule) ∧ shaft(c) = UP ⇒ TOP_FLOOR ∉ cabin_schedule[{c}] end event MotorStarts extends MotorStarts end event MotorStops extends MotorStops end event DoorClosedToHalf extends DoorClosedToHalf then @remove_floor_request floor_schedule ≔ floor_schedule ∖ {floor(cabin) ↦ shaft(cabin)} @remove_cabin_floor_request cabin_schedule ≔ cabin_schedule ∖ {cabin ↦ floor(cabin)} end event DoorHalfToOpen extends DoorHalfToOpen end event DoorOpenToHalf extends DoorOpenToHalf end event DoorHalfToClosed extends DoorHalfToClosed end event UserPressesUpButton any any_floor where @floor any_floor ∈ FLOORS @!already_requested UP ∉ floor_schedule[{any_floor}] @not_top_floor any_floor ≠ TOP_FLOOR //REQ 12 @no_cabin_on_floor ∀c·c ∈ CABINS ⇒ floor(c) ≠ any_floor then @request_up floor_schedule ≔ floor_schedule ∪ {any_floor ↦ UP} end event UserPressesDownButton any any_floor where @floor any_floor ∈ FLOORS @!already_requested DOWN ∉ floor_schedule[{any_floor}] @not_ground_floor any_floor ≠ 0 //REQ 11 @no_cabin_on_floor ∀c·c ∈ CABINS ⇒ floor(c) ≠ any_floor then @request_down floor_schedule ≔ floor_schedule ∪ {any_floor ↦ DOWN} end event UserPressesFloorButton any cabin selected_floor where @floor selected_floor ∈ FLOORS @!already_requested selected_floor ∉ cabin_schedule[{cabin}] @not_at_selected_floor floor(cabin) ≠ selected_floor then @request_floor cabin_schedule ≔ cabin_schedule ∪ {cabin ↦ selected_floor} end end " version="5">
<org.eventb.core.refinesMachine name="'" org.eventb.core.target="m3_door"/>
<org.eventb.core.seesContext name="_hn4EgJ-kEeq6js3PozKjqQ" org.eventb.core.target="m4_buttons_context"/>
<org.eventb.core.variable name="_ez5z8J-XEeq6js3PozKjqQ" org.eventb.core.generated="false" org.eventb.core.identifier="floor"/>
<org.eventb.core.variable name="_ez6bAJ-XEeq6js3PozKjqQ" org.eventb.core.generated="false" org.eventb.core.identifier="shaft"/>
<org.eventb.core.variable name="_VKszIJ-ZEeq6js3PozKjqQ" org.eventb.core.generated="false" org.eventb.core.identifier="motor"/>
<org.eventb.core.variable name="_OtiJIJ-eEeq6js3PozKjqQ" org.eventb.core.generated="false" org.eventb.core.identifier="door"/>
<org.eventb.core.event name="_ez6bAJ-XEeq6js3PozKjqR" 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="_i2zXcKDxEeq6js3PozKjqQ" org.eventb.core.assignment="cabin_schedule ≔ ∅" org.eventb.core.generated="false" org.eventb.core.label="cabin_schedule_init"/>
<org.eventb.core.action name="_i2z-gKDxEeq6js3PozKjqQ" org.eventb.core.assignment="floor_schedule ≔ ∅" org.eventb.core.generated="false" org.eventb.core.label="floor_schedule_init"/>
</org.eventb.core.event>
<org.eventb.core.event name="_ez6bAJ-XEeq6js3PozKjqS" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.generated="false" org.eventb.core.label="CabinMovesUp">
<org.eventb.core.refinesEvent name="'" org.eventb.core.target="CabinMovesUp"/>
<org.eventb.core.guard name="_GiNrwKGGEeq6js3PozKjqQ" org.eventb.core.comment="there is some request" org.eventb.core.generated="false" org.eventb.core.label="request_exists" org.eventb.core.predicate="cabin_schedule ≠ ∅ ∨ floor_schedule ≠ ∅"/>
<org.eventb.core.guard name="_ZILxQKGaEeq6js3PozKjqQ" org.eventb.core.comment="the current floor is not requested from inside ..AND not requested from outside ....OR the cabin is blocking the path of another" org.eventb.core.generated="false" org.eventb.core.label="REQ14" org.eventb.core.predicate="(floor(cabin) ∉ cabin_schedule[{cabin}]) 	∧ ((∃f·f = floor(cabin) ∧ UP ∉ floor_schedule[{f}]) 		∨ (∃c·c ∈ dom(cabin_schedule) ∧ (∃f·f ∈ cabin_schedule[{c}] ∧ f ≥ floor(cabin))))"/>
</org.eventb.core.event>
<org.eventb.core.event name="_ez6bAJ-XEeq6js3PozKjqT" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.generated="false" org.eventb.core.label="CabinMovesDown">
<org.eventb.core.refinesEvent name="'" org.eventb.core.target="CabinMovesDown"/>
<org.eventb.core.guard name="_GiNrwqGGEeq6js3PozKjqQ" org.eventb.core.comment="there is some request" org.eventb.core.generated="false" org.eventb.core.label="request_exists" org.eventb.core.predicate="cabin_schedule ≠ ∅ ∨ floor_schedule ≠ ∅"/>
<org.eventb.core.guard name="_ZILxQaGaEeq6js3PozKjqQ" org.eventb.core.comment="the current floor is not requested from inside ..AND not requested from outside ....OR the cabin is blocking the path of another" org.eventb.core.generated="false" org.eventb.core.label="REQ14" org.eventb.core.predicate="(floor(cabin) ∉ cabin_schedule[{cabin}]) 	∧ ((∃f·f = floor(cabin) ∧ DOWN ∉ floor_schedule[{f}]) 		∨ (∃c·c ∈ dom(cabin_schedule) ∧ (∃f·f ∈ cabin_schedule[{c}] ∧ f ≤ floor(cabin))))"/>
</org.eventb.core.event>
<org.eventb.core.event name="_ez6bAJ-XEeq6js3PozKjqU" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.generated="false" org.eventb.core.label="CabinDownToUp">
<org.eventb.core.refinesEvent name="'" org.eventb.core.target="CabinDownToUp"/>
<org.eventb.core.guard name="_ZILxQqGaEeq6js3PozKjqQ" org.eventb.core.generated="false" org.eventb.core.label="REQ14" org.eventb.core.predicate="∀c·c ∈ dom(cabin_schedule) ∧ shaft(c) = DOWN ⇒ 0 ∉ cabin_schedule[{c}]"/>
</org.eventb.core.event>
<org.eventb.core.event name="_ez6bAJ-XEeq6js3PozKjqV" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.generated="false" org.eventb.core.label="CabinUpToDown">
<org.eventb.core.refinesEvent name="'" org.eventb.core.target="CabinUpToDown"/>
<org.eventb.core.guard name="_ZILxQ6GaEeq6js3PozKjqQ" org.eventb.core.generated="false" org.eventb.core.label="REQ14" org.eventb.core.predicate="∀c·c ∈ dom(cabin_schedule) ∧ shaft(c) = UP ⇒ TOP_FLOOR ∉ cabin_schedule[{c}]"/>
</org.eventb.core.event>
<org.eventb.core.event name="_ez6bAJ-XEeq6js3PozKjqW" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.generated="false" org.eventb.core.label="MotorStarts">
<org.eventb.core.refinesEvent name="'" org.eventb.core.target="MotorStarts"/>
</org.eventb.core.event>
<org.eventb.core.event name="_ez6bAJ-XEeq6js3PozKjqX" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.generated="false" org.eventb.core.label="MotorStops">
<org.eventb.core.refinesEvent name="'" org.eventb.core.target="MotorStops"/>
</org.eventb.core.event>
<org.eventb.core.event name="_ez6bAJ-XEeq6js3PozKjqY" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.generated="false" org.eventb.core.label="DoorClosedToHalf">
<org.eventb.core.refinesEvent name="'" org.eventb.core.target="DoorClosedToHalf"/>
<org.eventb.core.action name="_BKSoQKDrEeq6js3PozKjqQ" org.eventb.core.assignment="floor_schedule ≔ floor_schedule ∖ {floor(cabin) ↦ shaft(cabin)}" org.eventb.core.generated="false" org.eventb.core.label="remove_floor_request"/>
<org.eventb.core.action name="_N9FlUKDrEeq6js3PozKjqQ" org.eventb.core.assignment="cabin_schedule ≔ cabin_schedule ∖ {cabin ↦ floor(cabin)}" org.eventb.core.generated="false" org.eventb.core.label="remove_cabin_floor_request"/>
</org.eventb.core.event>
<org.eventb.core.event name="_ez6bAJ-XEeq6js3PozKjqZ" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.generated="false" org.eventb.core.label="DoorHalfToOpen">
<org.eventb.core.refinesEvent name="'" org.eventb.core.target="DoorHalfToOpen"/>
</org.eventb.core.event>
<org.eventb.core.event name="_ez6bAJ-XEeq6js3PozKjq[" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.generated="false" org.eventb.core.label="DoorOpenToHalf">
<org.eventb.core.refinesEvent name="'" org.eventb.core.target="DoorOpenToHalf"/>
</org.eventb.core.event>
<org.eventb.core.event name="_ez6bAJ-XEeq6js3PozKjq\" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.generated="false" org.eventb.core.label="DoorHalfToClosed">
<org.eventb.core.refinesEvent name="'" org.eventb.core.target="DoorHalfToClosed"/>
</org.eventb.core.event>
<org.eventb.core.event name="_xvZhsJ-kEeq6js3PozKjqQ" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.generated="false" org.eventb.core.label="UserPressesUpButton">
<org.eventb.core.parameter name="_y762IKDLEeq6js3PozKjqQ" org.eventb.core.generated="false" org.eventb.core.identifier="any_floor"/>
<org.eventb.core.guard name="_Ac_d4Z-tEeq6js3PozKjqQ" org.eventb.core.generated="false" org.eventb.core.label="floor" org.eventb.core.predicate="any_floor ∈ FLOORS"/>
<org.eventb.core.guard name="_5ah7gKDPEeq6js3PozKjqQ" org.eventb.core.generated="false" org.eventb.core.label="!already_requested" org.eventb.core.predicate="UP ∉ floor_schedule[{any_floor}]"/>
<org.eventb.core.guard name="_y762IaDLEeq6js3PozKjqQ" org.eventb.core.comment="REQ 12" org.eventb.core.generated="false" org.eventb.core.label="not_top_floor" org.eventb.core.predicate="any_floor ≠ TOP_FLOOR"/>
<org.eventb.core.guard name="_DQnN0KDmEeq6js3PozKjqQ" org.eventb.core.generated="false" org.eventb.core.label="no_cabin_on_floor" org.eventb.core.predicate="∀c·c ∈ CABINS ⇒ floor(c) ≠ any_floor"/>
<org.eventb.core.action name="_y762IqDLEeq6js3PozKjqQ" org.eventb.core.assignment="floor_schedule ≔ floor_schedule ∪ {any_floor ↦ UP}" org.eventb.core.generated="false" org.eventb.core.label="request_up"/>
</org.eventb.core.event>
<org.eventb.core.event name="_xvaIwJ-kEeq6js3PozKjqQ" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.generated="false" org.eventb.core.label="UserPressesDownButton">
<org.eventb.core.parameter name="_Fnar8KDMEeq6js3PozKjqQ" org.eventb.core.generated="false" org.eventb.core.identifier="any_floor"/>
<org.eventb.core.guard name="_dnLJUKDPEeq6js3PozKjqQ" org.eventb.core.generated="false" org.eventb.core.label="floor" org.eventb.core.predicate="any_floor ∈ FLOORS"/>
<org.eventb.core.guard name="_HJpW4KDQEeq6js3PozKjqQ" org.eventb.core.generated="false" org.eventb.core.label="!already_requested" org.eventb.core.predicate="DOWN ∉ floor_schedule[{any_floor}]"/>
<org.eventb.core.guard name="_nIbkgKDMEeq6js3PozKjqQ" org.eventb.core.comment="REQ 11" org.eventb.core.generated="false" org.eventb.core.label="not_ground_floor" org.eventb.core.predicate="any_floor ≠ 0"/>
<org.eventb.core.guard name="_DQxl4KDmEeq6js3PozKjqQ" org.eventb.core.generated="false" org.eventb.core.label="no_cabin_on_floor" org.eventb.core.predicate="∀c·c ∈ CABINS ⇒ floor(c) ≠ any_floor"/>
<org.eventb.core.action name="_nIbkgaDMEeq6js3PozKjqQ" org.eventb.core.assignment="floor_schedule ≔ floor_schedule ∪ {any_floor ↦ DOWN}" org.eventb.core.generated="false" org.eventb.core.label="request_down"/>
</org.eventb.core.event>
<org.eventb.core.event name="_xvav0J-kEeq6js3PozKjqQ" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.generated="false" org.eventb.core.label="UserPressesFloorButton">
<org.eventb.core.parameter name="_3bonkJ-rEeq6js3PozKjqQ" org.eventb.core.generated="false" org.eventb.core.identifier="cabin"/>
<org.eventb.core.parameter name="_CE0z0J-sEeq6js3PozKjqQ" org.eventb.core.generated="false" org.eventb.core.identifier="selected_floor"/>
<org.eventb.core.guard name="_P9YygKDSEeq6js3PozKjqQ" org.eventb.core.generated="false" org.eventb.core.label="floor" org.eventb.core.predicate="selected_floor ∈ FLOORS"/>
<org.eventb.core.guard name="_P9YygaDSEeq6js3PozKjqQ" org.eventb.core.generated="false" org.eventb.core.label="!already_requested" org.eventb.core.predicate="selected_floor ∉ cabin_schedule[{cabin}]"/>
<org.eventb.core.guard name="_P9YygqDSEeq6js3PozKjqQ" org.eventb.core.generated="false" org.eventb.core.label="not_at_selected_floor" org.eventb.core.predicate="floor(cabin) ≠ selected_floor"/>
<org.eventb.core.action name="_P9Yyg6DSEeq6js3PozKjqQ" org.eventb.core.assignment="cabin_schedule ≔ cabin_schedule ∪ {cabin ↦ selected_floor}" org.eventb.core.generated="false" org.eventb.core.label="request_floor"/>
</org.eventb.core.event>
<org.eventb.core.variable name="_i3G5cKDxEeq6js3PozKjqQ" org.eventb.core.generated="false" org.eventb.core.identifier="cabin_schedule"/>
<org.eventb.core.variable name="_i3HggKDxEeq6js3PozKjqQ" org.eventb.core.generated="false" org.eventb.core.identifier="floor_schedule"/>
<org.eventb.core.invariant name="_i3IHkKDxEeq6js3PozKjqQ" org.eventb.core.comment="REQ 13" org.eventb.core.generated="false" org.eventb.core.label="cabin_schedule_type" org.eventb.core.predicate="cabin_schedule ∈ CABINS ↔ FLOORS"/>
<org.eventb.core.invariant name="_i3IHkaDxEeq6js3PozKjqQ" org.eventb.core.generated="false" org.eventb.core.label="floor_schedule_type" org.eventb.core.predicate="floor_schedule ∈ FLOORS ↔ SHAFTS"/>
</org.eventb.core.machineFile>