-
Notifications
You must be signed in to change notification settings - Fork 1
/
Copy pathm3_door.bum
55 lines (55 loc) · 8.28 KB
/
m3_door.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
<?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="1590749225686" org.eventb.texttools.text_representation="machine m3_door refines m2_motor sees m3_door_context variables floor shaft motor door invariants @door_type door ∈ CABINS → DOOR_STATE //REQ 9 @SAF10 ∀c·c ∈ CABINS ∧ motor(c) = ON ⇒ door(c) = CLOSED @SAF10thm ∀c·c ∈ CABINS ∧ door(c) ∈ {OPEN, HALF} ⇒ motor(c) = OFF events event INITIALISATION extends INITIALISATION then @door_type door ≔ CABINS × {CLOSED} end event CabinMovesUp extends CabinMovesUp end event CabinMovesDown extends CabinMovesDown end event CabinDownToUp extends CabinDownToUp end event CabinUpToDown extends CabinUpToDown end event MotorStarts extends MotorStarts where @door_is_closed door(cabin) = CLOSED end event MotorStops extends MotorStops end event DoorClosedToHalf any cabin where @door_closed door(cabin) = CLOSED @motor_off motor(cabin) = OFF then @half door(cabin) ≔ HALF end event DoorHalfToOpen any cabin where @door_half door(cabin) = HALF then @open door(cabin) ≔ OPEN end event DoorOpenToHalf any cabin where @door_open door(cabin) = OPEN then @half door(cabin) ≔ HALF end event DoorHalfToClosed any cabin where @door_half door(cabin) = HALF then @closed door(cabin) ≔ CLOSED end end" version="5">
<org.eventb.core.refinesMachine name="'" org.eventb.core.target="m2_motor"/>
<org.eventb.core.seesContext name="_bEAogJ-cEeq6js3PozKjqQ" org.eventb.core.target="m3_door_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.event name="_hmScAJ-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="_dx8jgJ-eEeq6js3PozKjqQ" org.eventb.core.assignment="door ≔ CABINS × {CLOSED}" org.eventb.core.generated="false" org.eventb.core.label="door_type"/>
</org.eventb.core.event>
<org.eventb.core.event name="_hmScAJ-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.event>
<org.eventb.core.event name="_hmScAJ-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.event>
<org.eventb.core.event name="_hmScAJ-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.event>
<org.eventb.core.event name="_hmScAJ-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.event>
<org.eventb.core.event name="_hmScAJ-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.guard name="_wz0KkJ-hEeq6js3PozKjqQ" org.eventb.core.generated="false" org.eventb.core.label="door_is_closed" org.eventb.core.predicate="door(cabin) = CLOSED"/>
</org.eventb.core.event>
<org.eventb.core.event name="_hmScAJ-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="_sWF-4J-dEeq6js3PozKjqQ" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.generated="false" org.eventb.core.label="DoorClosedToHalf">
<org.eventb.core.parameter name="_bOPT0J-iEeq6js3PozKjqQ" org.eventb.core.generated="false" org.eventb.core.identifier="cabin"/>
<org.eventb.core.guard name="_bOP64J-iEeq6js3PozKjqQ" org.eventb.core.generated="false" org.eventb.core.label="door_closed" org.eventb.core.predicate="door(cabin) = CLOSED"/>
<org.eventb.core.guard name="_9W1w0J-iEeq6js3PozKjqQ" org.eventb.core.generated="false" org.eventb.core.label="motor_off" org.eventb.core.predicate="motor(cabin) = OFF"/>
<org.eventb.core.action name="_bOP64Z-iEeq6js3PozKjqQ" org.eventb.core.assignment="door(cabin) ≔ HALF" org.eventb.core.generated="false" org.eventb.core.label="half"/>
</org.eventb.core.event>
<org.eventb.core.event name="_sWGl8J-dEeq6js3PozKjqQ" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.generated="false" org.eventb.core.label="DoorHalfToOpen">
<org.eventb.core.parameter name="_bORJAJ-iEeq6js3PozKjqQ" org.eventb.core.generated="false" org.eventb.core.identifier="cabin"/>
<org.eventb.core.guard name="_bORJAZ-iEeq6js3PozKjqQ" org.eventb.core.generated="false" org.eventb.core.label="door_half" org.eventb.core.predicate="door(cabin) = HALF"/>
<org.eventb.core.action name="_bORwEJ-iEeq6js3PozKjqQ" org.eventb.core.assignment="door(cabin) ≔ OPEN" org.eventb.core.generated="false" org.eventb.core.label="open"/>
</org.eventb.core.event>
<org.eventb.core.event name="_sWHNAJ-dEeq6js3PozKjqQ" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.generated="false" org.eventb.core.label="DoorOpenToHalf">
<org.eventb.core.parameter name="_bOSXIJ-iEeq6js3PozKjqQ" org.eventb.core.generated="false" org.eventb.core.identifier="cabin"/>
<org.eventb.core.guard name="_bOSXIZ-iEeq6js3PozKjqQ" org.eventb.core.generated="false" org.eventb.core.label="door_open" org.eventb.core.predicate="door(cabin) = OPEN"/>
<org.eventb.core.action name="_bOS-MJ-iEeq6js3PozKjqQ" org.eventb.core.assignment="door(cabin) ≔ HALF" org.eventb.core.generated="false" org.eventb.core.label="half"/>
</org.eventb.core.event>
<org.eventb.core.event name="_sWH0EJ-dEeq6js3PozKjqQ" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.generated="false" org.eventb.core.label="DoorHalfToClosed">
<org.eventb.core.parameter name="_bOTlQJ-iEeq6js3PozKjqQ" org.eventb.core.generated="false" org.eventb.core.identifier="cabin"/>
<org.eventb.core.guard name="_bOUMUJ-iEeq6js3PozKjqQ" org.eventb.core.generated="false" org.eventb.core.label="door_half" org.eventb.core.predicate="door(cabin) = HALF"/>
<org.eventb.core.action name="_bOUMUZ-iEeq6js3PozKjqQ" org.eventb.core.assignment="door(cabin) ≔ CLOSED" org.eventb.core.generated="false" org.eventb.core.label="closed"/>
</org.eventb.core.event>
<org.eventb.core.variable name="_OtiJIJ-eEeq6js3PozKjqQ" org.eventb.core.generated="false" org.eventb.core.identifier="door"/>
<org.eventb.core.invariant name="_UN69sKFNEeq6js3PozKjqQ" org.eventb.core.comment="REQ 9" org.eventb.core.generated="false" org.eventb.core.label="door_type" org.eventb.core.predicate="door ∈ CABINS → DOOR_STATE"/>
<org.eventb.core.invariant name="_AsXfAJ-fEeq6js3PozKjqQ" org.eventb.core.generated="false" org.eventb.core.label="SAF10" org.eventb.core.predicate="∀c·c ∈ CABINS ∧ motor(c) = ON ⇒ door(c) = CLOSED"/>
<org.eventb.core.invariant name="_GOxI4J-lEeq6js3PozKjqQ" org.eventb.core.generated="false" org.eventb.core.label="SAF10thm" org.eventb.core.predicate="∀c·c ∈ CABINS ∧ door(c) ∈ {OPEN, HALF} ⇒ motor(c) = OFF"/>
</org.eventb.core.machineFile>