-
Notifications
You must be signed in to change notification settings - Fork 0
/
M3.bum
executable file
·70 lines (70 loc) · 8.34 KB
/
M3.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
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<org.eventb.core.machineFile org.eventb.core.configuration="org.eventb.core.fwd" org.eventb.texttools.text_lastmodified="1491916148352" org.eventb.texttools.text_representation="machine M3 refines M2 sees C2 variables motor_actuator motor_sensor start_motor_button start_motor_impulse stop_motor_button stop_motor_impulse clutch_actuator clutch_sensor invariants @inv1 clutch_sensor=engaged ⇒ motor_sensor=working @inv2 clutch_actuator=engaged ⇒ motor_sensor=working @inv3 motor_actuator=stopped ⇒ clutch_sensor=disengaged @inv4 motor_actuator=stopped ⇒ clutch_actuator=disengaged events event INITIALISATION extends INITIALISATION end event push_start_motor_button extends push_start_motor_button end event release_start_motor_button extends release_start_motor_button end event treat_push_start_motor_button extends treat_push_start_motor_button end event treat_push_start_motor_button_false extends treat_push_start_motor_button_false end event treat_release_start_motor_button extends treat_release_start_motor_button end event treat_push_stop_motor_button extends treat_push_stop_motor_button where @grd5 clutch_sensor = disengaged @grd6 clutch_actuator = disengaged end event treat_push_stop_motor_button_false extends treat_push_stop_motor_button_false end event treat_release_stop_motor_button extends treat_release_stop_motor_button end event motor_start extends motor_start end event motor_stop extends motor_stop end event push_stop_motor_button extends push_stop_motor_button end event release_stop_motor_button extends release_stop_motor_button end event treat_start_clutch extends treat_start_clutch where @grd3 motor_sensor = working @grd4 motor_actuator = working end event treat_stop_clutch extends treat_stop_clutch end event clutch_start extends clutch_start end event clutch_stop extends clutch_stop end end " version="5">
<org.eventb.core.refinesMachine name="'" org.eventb.core.target="M2"/>
<org.eventb.core.seesContext name="," org.eventb.core.target="C2"/>
<org.eventb.core.variable name="(" org.eventb.core.identifier="motor_actuator"/>
<org.eventb.core.variable name=")" org.eventb.core.identifier="motor_sensor"/>
<org.eventb.core.variable name="2" org.eventb.core.identifier="start_motor_button"/>
<org.eventb.core.variable name="3" org.eventb.core.identifier="start_motor_impulse"/>
<org.eventb.core.variable name="9" org.eventb.core.identifier="stop_motor_button"/>
<org.eventb.core.variable name=":" org.eventb.core.identifier="stop_motor_impulse"/>
<org.eventb.core.variable name="I" org.eventb.core.identifier="clutch_actuator"/>
<org.eventb.core.variable name="J" org.eventb.core.identifier="clutch_sensor"/>
<org.eventb.core.event name="K" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="INITIALISATION"/>
<org.eventb.core.event name="L" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="push_start_motor_button">
<org.eventb.core.refinesEvent name="'" org.eventb.core.target="push_start_motor_button"/>
</org.eventb.core.event>
<org.eventb.core.event name="M" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="release_start_motor_button">
<org.eventb.core.refinesEvent name="'" org.eventb.core.target="release_start_motor_button"/>
</org.eventb.core.event>
<org.eventb.core.event name="N" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="treat_push_start_motor_button">
<org.eventb.core.refinesEvent name="'" org.eventb.core.target="treat_push_start_motor_button"/>
</org.eventb.core.event>
<org.eventb.core.event name="O" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="treat_push_start_motor_button_false">
<org.eventb.core.refinesEvent name="'" org.eventb.core.target="treat_push_start_motor_button_false"/>
</org.eventb.core.event>
<org.eventb.core.event name="P" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="treat_release_start_motor_button">
<org.eventb.core.refinesEvent name="'" org.eventb.core.target="treat_release_start_motor_button"/>
</org.eventb.core.event>
<org.eventb.core.event name="Q" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="treat_push_stop_motor_button">
<org.eventb.core.refinesEvent name="'" org.eventb.core.target="treat_push_stop_motor_button"/>
<org.eventb.core.guard name="(" org.eventb.core.label="grd5" org.eventb.core.predicate="clutch_sensor = disengaged"/>
<org.eventb.core.guard name=")" org.eventb.core.label="grd6" org.eventb.core.predicate="clutch_actuator = disengaged"/>
</org.eventb.core.event>
<org.eventb.core.event name="R" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="treat_push_stop_motor_button_false">
<org.eventb.core.refinesEvent name="'" org.eventb.core.target="treat_push_stop_motor_button_false"/>
</org.eventb.core.event>
<org.eventb.core.event name="S" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="treat_release_stop_motor_button">
<org.eventb.core.refinesEvent name="'" org.eventb.core.target="treat_release_stop_motor_button"/>
</org.eventb.core.event>
<org.eventb.core.event name="T" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="motor_start">
<org.eventb.core.refinesEvent name="'" org.eventb.core.target="motor_start"/>
</org.eventb.core.event>
<org.eventb.core.event name="U" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="motor_stop">
<org.eventb.core.refinesEvent name="'" org.eventb.core.target="motor_stop"/>
</org.eventb.core.event>
<org.eventb.core.event name="V" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="push_stop_motor_button">
<org.eventb.core.refinesEvent name="'" org.eventb.core.target="push_stop_motor_button"/>
</org.eventb.core.event>
<org.eventb.core.event name="W" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="release_stop_motor_button">
<org.eventb.core.refinesEvent name="_pGYPkB63EeeaAbt6uRn7ow" org.eventb.core.target="release_stop_motor_button"/>
</org.eventb.core.event>
<org.eventb.core.event name="X" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="treat_start_clutch">
<org.eventb.core.refinesEvent name="'" org.eventb.core.target="treat_start_clutch"/>
<org.eventb.core.guard name="_DBS5cB64EeeaAbt6uRn7ow" org.eventb.core.label="grd3" org.eventb.core.predicate="motor_sensor = working"/>
<org.eventb.core.guard name="_DBS5cR64EeeaAbt6uRn7ow" org.eventb.core.label="grd4" org.eventb.core.predicate="motor_actuator = working"/>
</org.eventb.core.event>
<org.eventb.core.event name="Y" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="treat_stop_clutch">
<org.eventb.core.refinesEvent name="'" org.eventb.core.target="treat_stop_clutch"/>
</org.eventb.core.event>
<org.eventb.core.event name="Z" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="clutch_start">
<org.eventb.core.refinesEvent name="'" org.eventb.core.target="clutch_start"/>
</org.eventb.core.event>
<org.eventb.core.event name="[" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="clutch_stop">
<org.eventb.core.refinesEvent name="'" org.eventb.core.target="clutch_stop"/>
</org.eventb.core.event>
<org.eventb.core.invariant name="\" org.eventb.core.label="inv1" org.eventb.core.predicate="clutch_sensor=engaged ⇒ motor_sensor=working"/>
<org.eventb.core.invariant name="]" org.eventb.core.label="inv2" org.eventb.core.predicate="clutch_actuator=engaged ⇒ motor_sensor=working"/>
<org.eventb.core.invariant name="^" org.eventb.core.label="inv3" org.eventb.core.predicate="motor_actuator=stopped ⇒ clutch_sensor=disengaged"/>
<org.eventb.core.invariant name="_" org.eventb.core.label="inv4" org.eventb.core.predicate="motor_actuator=stopped ⇒ clutch_actuator=disengaged"/>
</org.eventb.core.machineFile>