-
Notifications
You must be signed in to change notification settings - Fork 1
/
Copy pathm2_motor.bum
38 lines (38 loc) · 5.9 KB
/
m2_motor.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
<?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="1590749082771" org.eventb.texttools.text_representation="machine m2_motor refines m1_shafts sees m2_motor_context variables floor shaft motor invariants @motor_type motor ∈ CABINS → MOTOR_STATE //REQ 6 events event INITIALISATION extends INITIALISATION then @motor_init motor ≔ CABINS × {OFF} end event CabinMovesUp extends CabinMovesUp where @is_motor_on motor(cabin) = ON //REQ 7 end event CabinMovesDown extends CabinMovesDown where @is_motor_on motor(cabin) = ON //REQ 7 end event CabinDownToUp extends CabinDownToUp where @is_motor_on motor(cabin) = ON //REQ 7 end event CabinUpToDown extends CabinUpToDown where @is_motor_on motor(cabin) = ON //REQ 7 end event MotorStarts any cabin where @is_off motor(cabin) = OFF then @turn_on motor(cabin) ≔ ON end event MotorStops any cabin where @is_on motor(cabin) = ON then @turn_off motor(cabin) ≔ OFF end end " version="5">
<org.eventb.core.refinesMachine name="_SWcNsJ-XEeq6js3PozKjqQ" org.eventb.core.target="m1_shafts"/>
<org.eventb.core.seesContext name="_hmScAJ-XEeq6js3PozKjqQ" org.eventb.core.target="m2_motor_context"/>
<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="_OtD9MKFNEeq6js3PozKjqQ" org.eventb.core.assignment="motor ≔ CABINS × {OFF}" org.eventb.core.generated="false" org.eventb.core.label="motor_init"/>
</org.eventb.core.event>
<org.eventb.core.event name="_dgJtEJ-XEeq6js3PozKjqQ" 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="_dgKUIJ-XEeq6js3PozKjqQ" org.eventb.core.target="CabinMovesUp"/>
<org.eventb.core.guard name="_54oToJ-ZEeq6js3PozKjqQ" org.eventb.core.comment="REQ 7" org.eventb.core.generated="false" org.eventb.core.label="is_motor_on" org.eventb.core.predicate="motor(cabin) = ON"/>
</org.eventb.core.event>
<org.eventb.core.event name="_dgK7MJ-XEeq6js3PozKjqQ" 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="_dgK7MZ-XEeq6js3PozKjqQ" org.eventb.core.target="CabinMovesDown"/>
<org.eventb.core.guard name="_54o6sJ-ZEeq6js3PozKjqQ" org.eventb.core.comment="REQ 7" org.eventb.core.generated="false" org.eventb.core.label="is_motor_on" org.eventb.core.predicate="motor(cabin) = ON"/>
</org.eventb.core.event>
<org.eventb.core.event name="_dgLiQJ-XEeq6js3PozKjqQ" 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="_dgLiQZ-XEeq6js3PozKjqQ" org.eventb.core.target="CabinDownToUp"/>
<org.eventb.core.guard name="_54qI0J-ZEeq6js3PozKjqQ" org.eventb.core.comment="REQ 7" org.eventb.core.generated="false" org.eventb.core.label="is_motor_on" org.eventb.core.predicate="motor(cabin) = ON"/>
</org.eventb.core.event>
<org.eventb.core.event name="_dgMJUJ-XEeq6js3PozKjqQ" 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="_dgMJUZ-XEeq6js3PozKjqQ" org.eventb.core.target="CabinUpToDown"/>
<org.eventb.core.guard name="_54rW8J-ZEeq6js3PozKjqQ" org.eventb.core.comment="REQ 7" org.eventb.core.generated="false" org.eventb.core.label="is_motor_on" org.eventb.core.predicate="motor(cabin) = ON"/>
</org.eventb.core.event>
<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.event name="_sL6W4J-XEeq6js3PozKjqQ" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.generated="false" org.eventb.core.label="MotorStarts">
<org.eventb.core.parameter name="_lSD4QJ-ZEeq6js3PozKjqQ" org.eventb.core.generated="false" org.eventb.core.identifier="cabin"/>
<org.eventb.core.guard name="_lSEfUJ-ZEeq6js3PozKjqQ" org.eventb.core.generated="false" org.eventb.core.label="is_off" org.eventb.core.predicate="motor(cabin) = OFF"/>
<org.eventb.core.action name="_lSEfUZ-ZEeq6js3PozKjqQ" org.eventb.core.assignment="motor(cabin) ≔ ON" org.eventb.core.generated="false" org.eventb.core.label="turn_on"/>
</org.eventb.core.event>
<org.eventb.core.event name="_sL698Z-XEeq6js3PozKjqQ" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.generated="false" org.eventb.core.label="MotorStops">
<org.eventb.core.parameter name="_lSFGYJ-ZEeq6js3PozKjqQ" org.eventb.core.generated="false" org.eventb.core.identifier="cabin"/>
<org.eventb.core.guard name="_lSFGYZ-ZEeq6js3PozKjqQ" org.eventb.core.generated="false" org.eventb.core.label="is_on" org.eventb.core.predicate="motor(cabin) = ON"/>
<org.eventb.core.action name="_lSFtcJ-ZEeq6js3PozKjqQ" org.eventb.core.assignment="motor(cabin) ≔ OFF" org.eventb.core.generated="false" org.eventb.core.label="turn_off"/>
</org.eventb.core.event>
<org.eventb.core.variable name="_VKszIJ-ZEeq6js3PozKjqQ" org.eventb.core.generated="false" org.eventb.core.identifier="motor"/>
<org.eventb.core.invariant name="_OtKD0KFNEeq6js3PozKjqQ" org.eventb.core.comment="REQ 6" org.eventb.core.generated="false" org.eventb.core.label="motor_type" org.eventb.core.predicate="motor ∈ CABINS → MOTOR_STATE"/>
</org.eventb.core.machineFile>