-
Notifications
You must be signed in to change notification settings - Fork 0
/
M1.bum
executable file
·77 lines (77 loc) · 10.5 KB
/
M1.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
<?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="1491915901380" org.eventb.texttools.text_representation="machine M1 refines M0 sees C0 variables motor_actuator motor_sensor start_motor_button start_motor_impulse stop_motor_button stop_motor_impulse invariants @inv1 start_motor_button∈BOOL @inv2 start_motor_impulse∈BOOL @inv3 stop_motor_button∈BOOL @inv4 stop_motor_impulse∈BOOL events event INITIALISATION extends INITIALISATION then @act3 start_motor_button ≔ FALSE @act4 start_motor_impulse ≔ FALSE @act5 stop_motor_button ≔ FALSE @act6 stop_motor_impulse ≔ FALSE end event push_start_motor_button where @grd1 start_motor_button = FALSE then @act1 start_motor_button ≔ TRUE end event release_start_motor_button where @grd1 start_motor_button = TRUE then @act1 start_motor_button ≔ FALSE end event treat_push_start_motor_button extends treat_start_motor where @grd3 start_motor_impulse = FALSE @grd4 start_motor_button = TRUE then @act2 start_motor_impulse ≔ TRUE end event treat_push_start_motor_button_false where @grd1 ¬(motor_actuator = stopped ∧ motor_sensor=stopped) @grd2 start_motor_impulse = FALSE @grd3 start_motor_button = TRUE then @act1 start_motor_impulse ≔ TRUE end event treat_release_start_motor_button where @grd1 start_motor_impulse = TRUE @grd2 start_motor_button = FALSE then @act1 start_motor_impulse ≔ FALSE end event treat_push_stop_motor_button extends treat_stop_motor where @grd3 stop_motor_impulse = FALSE @grd4 stop_motor_button = TRUE then @act2 stop_motor_impulse ≔ TRUE end event treat_push_stop_motor_button_false where @grd1 ¬(motor_actuator = working ∧ motor_sensor=working) @grd2 stop_motor_impulse = FALSE @grd3 stop_motor_button = TRUE then @act1 stop_motor_impulse ≔ TRUE end event treat_release_stop_motor_button where @grd1 stop_motor_impulse = TRUE @grd2 stop_motor_button = FALSE then @act1 stop_motor_impulse ≔ FALSE end event motor_start extends motor_start end event motor_stop extends motor_stop end event push_stop_motor_button where @grd1 stop_motor_button = FALSE then @act1 stop_motor_button ≔ TRUE end event release_stop_motor_button where @grd1 stop_motor_button = TRUE then @act1 stop_motor_button ≔ FALSE end end " version="5">
<org.eventb.core.refinesMachine name="'" org.eventb.core.target="M0"/>
<org.eventb.core.seesContext name="," org.eventb.core.target="C0"/>
<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.event name="-" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="INITIALISATION">
<org.eventb.core.action name="'" org.eventb.core.assignment="start_motor_button ≔ FALSE" org.eventb.core.label="act3"/>
<org.eventb.core.action name="(" org.eventb.core.assignment="start_motor_impulse ≔ FALSE" org.eventb.core.label="act4"/>
<org.eventb.core.action name=")" org.eventb.core.assignment="stop_motor_button ≔ FALSE" org.eventb.core.label="act5"/>
<org.eventb.core.action name="*" org.eventb.core.assignment="stop_motor_impulse ≔ FALSE" org.eventb.core.label="act6"/>
</org.eventb.core.event>
<org.eventb.core.event name="6" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="push_start_motor_button">
<org.eventb.core.guard name="'" org.eventb.core.label="grd1" org.eventb.core.predicate="start_motor_button = FALSE"/>
<org.eventb.core.action name="(" org.eventb.core.assignment="start_motor_button ≔ TRUE" org.eventb.core.label="act1"/>
</org.eventb.core.event>
<org.eventb.core.event name="7" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="release_start_motor_button">
<org.eventb.core.guard name="'" org.eventb.core.label="grd1" org.eventb.core.predicate="start_motor_button = TRUE"/>
<org.eventb.core.action name="(" org.eventb.core.assignment="start_motor_button ≔ FALSE" org.eventb.core.label="act1"/>
</org.eventb.core.event>
<org.eventb.core.event name="." 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_start_motor"/>
<org.eventb.core.guard name="(" org.eventb.core.label="grd3" org.eventb.core.predicate="start_motor_impulse = FALSE"/>
<org.eventb.core.guard name=")" org.eventb.core.label="grd4" org.eventb.core.predicate="start_motor_button = TRUE"/>
<org.eventb.core.action name="*" org.eventb.core.assignment="start_motor_impulse ≔ TRUE" org.eventb.core.label="act2"/>
</org.eventb.core.event>
<org.eventb.core.event name="evt4" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="treat_push_start_motor_button_false">
<org.eventb.core.guard name="'" org.eventb.core.label="grd1" org.eventb.core.predicate="¬(motor_actuator = stopped ∧ motor_sensor=stopped)"/>
<org.eventb.core.action name="(" org.eventb.core.assignment="start_motor_impulse ≔ TRUE" org.eventb.core.label="act1"/>
<org.eventb.core.guard name=")" org.eventb.core.label="grd2" org.eventb.core.predicate="start_motor_impulse = FALSE"/>
<org.eventb.core.guard name="*" org.eventb.core.label="grd3" org.eventb.core.predicate="start_motor_button = TRUE"/>
</org.eventb.core.event>
<org.eventb.core.event name="8" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="treat_release_start_motor_button">
<org.eventb.core.guard name="'" org.eventb.core.label="grd1" org.eventb.core.predicate="start_motor_impulse = TRUE"/>
<org.eventb.core.guard name="(" org.eventb.core.label="grd2" org.eventb.core.predicate="start_motor_button = FALSE"/>
<org.eventb.core.action name=")" org.eventb.core.assignment="start_motor_impulse ≔ FALSE" org.eventb.core.label="act1"/>
</org.eventb.core.event>
<org.eventb.core.event name="/" 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_stop_motor"/>
<org.eventb.core.guard name="(" org.eventb.core.label="grd3" org.eventb.core.predicate="stop_motor_impulse = FALSE"/>
<org.eventb.core.guard name=")" org.eventb.core.label="grd4" org.eventb.core.predicate="stop_motor_button = TRUE"/>
<org.eventb.core.action name="*" org.eventb.core.assignment="stop_motor_impulse ≔ TRUE" org.eventb.core.label="act2"/>
</org.eventb.core.event>
<org.eventb.core.event name="evt5" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="treat_push_stop_motor_button_false">
<org.eventb.core.guard name="'" org.eventb.core.label="grd1" org.eventb.core.predicate="¬(motor_actuator = working ∧ motor_sensor=working)"/>
<org.eventb.core.action name="(" org.eventb.core.assignment="stop_motor_impulse ≔ TRUE" org.eventb.core.label="act1"/>
<org.eventb.core.guard name=")" org.eventb.core.label="grd2" org.eventb.core.predicate="stop_motor_impulse = FALSE"/>
<org.eventb.core.guard name="*" org.eventb.core.label="grd3" org.eventb.core.predicate="stop_motor_button = TRUE"/>
</org.eventb.core.event>
<org.eventb.core.event name="evt3" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="treat_release_stop_motor_button">
<org.eventb.core.guard name="'" org.eventb.core.label="grd1" org.eventb.core.predicate="stop_motor_impulse = TRUE"/>
<org.eventb.core.guard name="(" org.eventb.core.label="grd2" org.eventb.core.predicate="stop_motor_button = FALSE"/>
<org.eventb.core.action name=")" org.eventb.core.assignment="stop_motor_impulse ≔ FALSE" org.eventb.core.label="act1"/>
</org.eventb.core.event>
<org.eventb.core.event name="0" 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="1" 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="evt1" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="push_stop_motor_button">
<org.eventb.core.guard name="'" org.eventb.core.label="grd1" org.eventb.core.predicate="stop_motor_button = FALSE"/>
<org.eventb.core.action name="(" org.eventb.core.assignment="stop_motor_button ≔ TRUE" org.eventb.core.label="act1"/>
</org.eventb.core.event>
<org.eventb.core.event name="evt2" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="release_stop_motor_button">
<org.eventb.core.guard name="'" org.eventb.core.label="grd1" org.eventb.core.predicate="stop_motor_button = TRUE"/>
<org.eventb.core.action name="(" org.eventb.core.assignment="stop_motor_button ≔ FALSE" org.eventb.core.label="act1"/>
</org.eventb.core.event>
<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.invariant name="4" org.eventb.core.label="inv1" org.eventb.core.predicate="start_motor_button∈BOOL"/>
<org.eventb.core.invariant name="5" org.eventb.core.label="inv2" org.eventb.core.predicate="start_motor_impulse∈BOOL"/>
<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.invariant name=";" org.eventb.core.label="inv3" org.eventb.core.predicate="stop_motor_button∈BOOL"/>
<org.eventb.core.invariant name="=" org.eventb.core.label="inv4" org.eventb.core.predicate="stop_motor_impulse∈BOOL"/>
</org.eventb.core.machineFile>