-
Notifications
You must be signed in to change notification settings - Fork 0
/
firstRef.bcm
101 lines (101 loc) · 23.9 KB
/
firstRef.bcm
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
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<org.eventb.core.scMachineFile org.eventb.core.accurate="true" org.eventb.core.configuration="org.eventb.core.fwd">
<org.eventb.core.scRefinesMachine name="'" org.eventb.core.scTarget="/ferryBoat/initialModel.bcm" org.eventb.core.source="/ferryBoat/firstRef.bum|org.eventb.core.machineFile#firstRef|org.eventb.core.refinesMachine#'"/>
<org.eventb.core.scSeesContext name="(" org.eventb.core.scTarget="/ferryBoat/firstRef_ctx.bcc" org.eventb.core.source="/ferryBoat/firstRef.bum|org.eventb.core.machineFile#firstRef|org.eventb.core.seesContext#N"/>
<org.eventb.core.scInternalContext name="integral_ctx">
<org.eventb.core.scAxiom name="'" org.eventb.core.label="f_integral" org.eventb.core.predicate="integral=(λx⦂ℙ(ℤ×ℤ)·x=(∅ ⦂ ℙ(ℤ×ℤ)) ∣ 0)∪(λx⦂ℙ(ℤ×ℤ)·x∈ℤ ⇸ ℤ∧finite(x)∧card(x)>0∧finite(dom(x)) ∣ integral(x ∖ {max(dom(x)) ↦ x(max(dom(x)))})+x(max(dom(x))))" org.eventb.core.source="/ferryBoat/integral_ctx.buc|org.eventb.core.contextFile#integral_ctx|org.eventb.core.axiom#(" org.eventb.core.theorem="false"/>
<org.eventb.core.scConstant de.prob.symbolic.symbolicAttribute="false" name="integral" org.eventb.core.source="/ferryBoat/integral_ctx.buc|org.eventb.core.contextFile#integral_ctx|org.eventb.core.constant#'" org.eventb.core.type="ℙ(ℙ(ℤ×ℤ)×ℤ)"/>
</org.eventb.core.scInternalContext>
<org.eventb.core.scInternalContext name="firstRef_ctx">
<org.eventb.core.scExtendsContext name="'" org.eventb.core.scTarget="/ferryBoat/integral_ctx.bcc|org.eventb.core.scContextFile#integral_ctx" org.eventb.core.source="/ferryBoat/firstRef_ctx.buc|org.eventb.core.contextFile#firstRef_ctx|org.eventb.core.extendsContext#,"/>
<org.eventb.core.scAxiom name="integral_cty" org.eventb.core.label="axm1_1" org.eventb.core.predicate="max_bs_m=6" org.eventb.core.source="/ferryBoat/firstRef_ctx.buc|org.eventb.core.contextFile#firstRef_ctx|org.eventb.core.axiom#(" org.eventb.core.theorem="false"/>
<org.eventb.core.scAxiom name="integral_ctz" org.eventb.core.label="axm2_1" org.eventb.core.predicate="floors=1 ‥ 3" org.eventb.core.source="/ferryBoat/firstRef_ctx.buc|org.eventb.core.contextFile#firstRef_ctx|org.eventb.core.axiom#*" org.eventb.core.theorem="false"/>
<org.eventb.core.scConstant name="floors" org.eventb.core.source="/ferryBoat/firstRef_ctx.buc|org.eventb.core.contextFile#firstRef_ctx|org.eventb.core.constant#+" org.eventb.core.type="ℙ(ℤ)"/>
<org.eventb.core.scConstant de.prob.symbolic.symbolicAttribute="false" name="max_bs_m" org.eventb.core.source="/ferryBoat/firstRef_ctx.buc|org.eventb.core.contextFile#firstRef_ctx|org.eventb.core.constant#'" org.eventb.core.type="ℤ"/>
</org.eventb.core.scInternalContext>
<org.eventb.core.scInvariant name="'" org.eventb.core.label="inv1" org.eventb.core.predicate="max_busy_slots∈ℕ" org.eventb.core.source="/FerryBoat/initialModel.bum|org.eventb.core.machineFile#initialModel|org.eventb.core.invariant#)" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="(" org.eventb.core.label="inv2" org.eventb.core.predicate="busy_slots∈ℕ" org.eventb.core.source="/FerryBoat/initialModel.bum|org.eventb.core.machineFile#initialModel|org.eventb.core.invariant#," org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name=")" org.eventb.core.label="inv3" org.eventb.core.predicate="busy_slots≤max_busy_slots" org.eventb.core.source="/FerryBoat/initialModel.bum|org.eventb.core.machineFile#initialModel|org.eventb.core.invariant#-" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="integral_cty" org.eventb.core.label="inv1_1" org.eventb.core.predicate="max_bs_p∈floors → ℕ" org.eventb.core.source="/ferryBoat/firstRef.bum|org.eventb.core.machineFile#firstRef|org.eventb.core.invariant#2" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="integral_ctz" org.eventb.core.label="inv2_1" org.eventb.core.predicate="bs_p∈floors → ℕ" org.eventb.core.source="/ferryBoat/firstRef.bum|org.eventb.core.machineFile#firstRef|org.eventb.core.invariant#9" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="integral_ct{" org.eventb.core.label="inv3_1" org.eventb.core.predicate="∀x⦂ℤ·x∈floors⇒bs_p(x)≤max_bs_p(x)" org.eventb.core.source="/ferryBoat/firstRef.bum|org.eventb.core.machineFile#firstRef|org.eventb.core.invariant#;" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="integral_ct|" org.eventb.core.label="inv4_1_glue1" org.eventb.core.predicate="max_busy_slots=integral(max_bs_p)" org.eventb.core.source="/ferryBoat/firstRef.bum|org.eventb.core.machineFile#firstRef|org.eventb.core.invariant#B" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="integral_ct}" org.eventb.core.label="inv5_1_glue2" org.eventb.core.predicate="busy_slots=integral(bs_p)" org.eventb.core.source="/ferryBoat/firstRef.bum|org.eventb.core.machineFile#firstRef|org.eventb.core.invariant#D" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="integral_ct~" org.eventb.core.label="inv6_1" org.eventb.core.predicate="lift_level∈floors" org.eventb.core.source="/ferryBoat/firstRef.bum|org.eventb.core.machineFile#firstRef|org.eventb.core.invariant#F" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="integral_cu'" org.eventb.core.label="inv7_1" org.eventb.core.predicate="bs_m∈ℕ∧bs_m≤max_bs_m" org.eventb.core.source="/ferryBoat/firstRef.bum|org.eventb.core.machineFile#firstRef|org.eventb.core.invariant#L" org.eventb.core.theorem="false"/>
<org.eventb.core.scVariable name="bs_m" org.eventb.core.abstract="false" org.eventb.core.concrete="true" org.eventb.core.source="/ferryBoat/firstRef.bum|org.eventb.core.machineFile#firstRef|org.eventb.core.variable#K" org.eventb.core.type="ℤ"/>
<org.eventb.core.scVariable name="bs_p" org.eventb.core.abstract="false" org.eventb.core.concrete="true" org.eventb.core.source="/ferryBoat/firstRef.bum|org.eventb.core.machineFile#firstRef|org.eventb.core.variable#@" org.eventb.core.type="ℙ(ℤ×ℤ)"/>
<org.eventb.core.scVariable name="busy_slots" org.eventb.core.abstract="true" org.eventb.core.concrete="true" org.eventb.core.source="/ferryBoat/firstRef.bum|org.eventb.core.machineFile#firstRef|org.eventb.core.variable#+" org.eventb.core.type="ℤ"/>
<org.eventb.core.scVariable name="lift_level" org.eventb.core.abstract="false" org.eventb.core.concrete="true" org.eventb.core.source="/ferryBoat/firstRef.bum|org.eventb.core.machineFile#firstRef|org.eventb.core.variable#E" org.eventb.core.type="ℤ"/>
<org.eventb.core.scVariable name="max_bs_p" org.eventb.core.abstract="false" org.eventb.core.concrete="true" org.eventb.core.source="/ferryBoat/firstRef.bum|org.eventb.core.machineFile#firstRef|org.eventb.core.variable#1" org.eventb.core.type="ℙ(ℤ×ℤ)"/>
<org.eventb.core.scVariable name="max_busy_slots" org.eventb.core.abstract="true" org.eventb.core.concrete="true" org.eventb.core.source="/ferryBoat/firstRef.bum|org.eventb.core.machineFile#firstRef|org.eventb.core.variable#(" org.eventb.core.type="ℤ"/>
<org.eventb.core.scEvent name="max_busy_slott" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="INITIALISATION" org.eventb.core.source="/ferryBoat/firstRef.bum|org.eventb.core.machineFile#firstRef|org.eventb.core.event#,">
<org.eventb.core.scRefinesEvent name="'" org.eventb.core.scTarget="/ferryBoat/initialModel.bcm|org.eventb.core.scMachineFile#initialModel|org.eventb.core.scEvent#max_busy_slott" org.eventb.core.source="/ferryBoat/firstRef.bum|org.eventb.core.machineFile#firstRef|org.eventb.core.event#,"/>
<org.eventb.core.scAction name="'" org.eventb.core.assignment="max_busy_slots ≔ 0" org.eventb.core.label="act1" org.eventb.core.source="/FerryBoat/initialModel.bum|org.eventb.core.machineFile#initialModel|org.eventb.core.event#'|org.eventb.core.action#'"/>
<org.eventb.core.scAction name="(" org.eventb.core.assignment="busy_slots ≔ 0" org.eventb.core.label="act2" org.eventb.core.source="/FerryBoat/initialModel.bum|org.eventb.core.machineFile#initialModel|org.eventb.core.event#'|org.eventb.core.action#("/>
<org.eventb.core.scAction name=")" org.eventb.core.assignment="max_bs_p ≔ {f⦂ℤ·f∈floors ∣ f ↦ 0}" org.eventb.core.label="act3_1" org.eventb.core.source="/ferryBoat/firstRef.bum|org.eventb.core.machineFile#firstRef|org.eventb.core.event#,|org.eventb.core.action#'"/>
<org.eventb.core.scAction name="*" org.eventb.core.assignment="bs_p ≔ {f⦂ℤ·f∈floors ∣ f ↦ 0}" org.eventb.core.label="act6_1" org.eventb.core.source="/ferryBoat/firstRef.bum|org.eventb.core.machineFile#firstRef|org.eventb.core.event#,|org.eventb.core.action#*"/>
<org.eventb.core.scAction name="+" org.eventb.core.assignment="lift_level ≔ 1" org.eventb.core.label="act9_1" org.eventb.core.source="/ferryBoat/firstRef.bum|org.eventb.core.machineFile#firstRef|org.eventb.core.event#,|org.eventb.core.action#-"/>
<org.eventb.core.scAction name="," org.eventb.core.assignment="bs_m ≔ 0" org.eventb.core.label="act11_1" org.eventb.core.source="/ferryBoat/firstRef.bum|org.eventb.core.machineFile#firstRef|org.eventb.core.event#,|org.eventb.core.action#\/"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="max_busy_slotu" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="Boat_ready" org.eventb.core.source="/ferryBoat/firstRef.bum|org.eventb.core.machineFile#firstRef|org.eventb.core.event#-">
<org.eventb.core.scRefinesEvent name="'" org.eventb.core.scTarget="/ferryBoat/initialModel.bcm|org.eventb.core.scMachineFile#initialModel|org.eventb.core.scEvent#max_busy_slotu" org.eventb.core.source="/ferryBoat/firstRef.bum|org.eventb.core.machineFile#firstRef|org.eventb.core.event#-|org.eventb.core.refinesEvent#'"/>
<org.eventb.core.scGuard name="(" org.eventb.core.label="grd1_1" org.eventb.core.predicate="capacities∈floors → ℕ" org.eventb.core.source="/ferryBoat/firstRef.bum|org.eventb.core.machineFile#firstRef|org.eventb.core.event#-|org.eventb.core.guard#+" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name=")" org.eventb.core.label="grd2_1" org.eventb.core.predicate="ran(capacities)≠{0}" org.eventb.core.source="/ferryBoat/firstRef.bum|org.eventb.core.machineFile#firstRef|org.eventb.core.event#-|org.eventb.core.guard#internal4" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="*" org.eventb.core.label="grd3_1" org.eventb.core.predicate="∀x⦂ℤ·x∈floors⇒max_bs_p(x)=0" org.eventb.core.source="/ferryBoat/firstRef.bum|org.eventb.core.machineFile#firstRef|org.eventb.core.event#-|org.eventb.core.guard#," org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="+" org.eventb.core.label="grd4_1" org.eventb.core.predicate="∀x⦂ℤ·x∈floors⇒bs_p(x)=0" org.eventb.core.source="/ferryBoat/firstRef.bum|org.eventb.core.machineFile#firstRef|org.eventb.core.event#-|org.eventb.core.guard#-" org.eventb.core.theorem="false"/>
<org.eventb.core.scParameter name="capacities" org.eventb.core.source="/ferryBoat/firstRef.bum|org.eventb.core.machineFile#firstRef|org.eventb.core.event#-|org.eventb.core.parameter#)" org.eventb.core.type="ℙ(ℤ×ℤ)"/>
<org.eventb.core.scAction name="capacitiet" org.eventb.core.assignment="max_busy_slots ≔ integral(capacities)" org.eventb.core.label="act1_1" org.eventb.core.source="/ferryBoat/firstRef.bum|org.eventb.core.machineFile#firstRef|org.eventb.core.event#-|org.eventb.core.action#internal3"/>
<org.eventb.core.scAction name="capacitieu" org.eventb.core.assignment="max_bs_p ≔ capacities" org.eventb.core.label="act2_1" org.eventb.core.source="/ferryBoat/firstRef.bum|org.eventb.core.machineFile#firstRef|org.eventb.core.event#-|org.eventb.core.action#("/>
<org.eventb.core.scWitness name="capacitiev" org.eventb.core.label="total_capacity" org.eventb.core.predicate="total_capacity=integral(capacities)" org.eventb.core.source="/ferryBoat/firstRef.bum|org.eventb.core.machineFile#firstRef|org.eventb.core.event#-|org.eventb.core.witness#internal2"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="max_busy_slotv" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="Boat_leave" org.eventb.core.source="/ferryBoat/firstRef.bum|org.eventb.core.machineFile#firstRef|org.eventb.core.event#.">
<org.eventb.core.scRefinesEvent name="'" org.eventb.core.scTarget="/ferryBoat/initialModel.bcm|org.eventb.core.scMachineFile#initialModel|org.eventb.core.scEvent#max_busy_slotv" org.eventb.core.source="/ferryBoat/firstRef.bum|org.eventb.core.machineFile#firstRef|org.eventb.core.event#.|org.eventb.core.refinesEvent#'"/>
<org.eventb.core.scGuard name="'" org.eventb.core.label="grd1" org.eventb.core.predicate="0<max_busy_slots" org.eventb.core.source="/FerryBoat/initialModel.bum|org.eventb.core.machineFile#initialModel|org.eventb.core.event#0|org.eventb.core.guard#)" org.eventb.core.theorem="false"/>
<org.eventb.core.scAction name="(" org.eventb.core.assignment="busy_slots ≔ 0" org.eventb.core.label="act1" org.eventb.core.source="/FerryBoat/initialModel.bum|org.eventb.core.machineFile#initialModel|org.eventb.core.event#0|org.eventb.core.action#'"/>
<org.eventb.core.scAction name=")" org.eventb.core.assignment="max_busy_slots ≔ 0" org.eventb.core.label="act2" org.eventb.core.source="/FerryBoat/initialModel.bum|org.eventb.core.machineFile#initialModel|org.eventb.core.event#0|org.eventb.core.action#("/>
<org.eventb.core.scAction name="*" org.eventb.core.assignment="bs_p ≔ {f⦂ℤ·f∈floors ∣ f ↦ 0}" org.eventb.core.label="act3_1" org.eventb.core.source="/ferryBoat/firstRef.bum|org.eventb.core.machineFile#firstRef|org.eventb.core.event#.|org.eventb.core.action#("/>
<org.eventb.core.scAction name="+" org.eventb.core.assignment="max_bs_p ≔ {f⦂ℤ·f∈floors ∣ f ↦ 0}" org.eventb.core.label="act4_1" org.eventb.core.source="/ferryBoat/firstRef.bum|org.eventb.core.machineFile#firstRef|org.eventb.core.event#.|org.eventb.core.action#)"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="max_busy_slotw" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="Board" org.eventb.core.source="/ferryBoat/firstRef.bum|org.eventb.core.machineFile#firstRef|org.eventb.core.event#\/">
<org.eventb.core.scRefinesEvent name="'" org.eventb.core.scTarget="/ferryBoat/initialModel.bcm|org.eventb.core.scMachineFile#initialModel|org.eventb.core.scEvent#max_busy_slotw" org.eventb.core.source="/ferryBoat/firstRef.bum|org.eventb.core.machineFile#firstRef|org.eventb.core.event#\/|org.eventb.core.refinesEvent#'"/>
<org.eventb.core.scGuard name="'" org.eventb.core.label="grd1" org.eventb.core.predicate="load_at_once∈ℕ1" org.eventb.core.source="/FerryBoat/initialModel.bum|org.eventb.core.machineFile#initialModel|org.eventb.core.event#.|org.eventb.core.guard#(" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="(" org.eventb.core.label="grd2" org.eventb.core.predicate="busy_slots+load_at_once≤max_busy_slots" org.eventb.core.source="/FerryBoat/initialModel.bum|org.eventb.core.machineFile#initialModel|org.eventb.core.event#.|org.eventb.core.guard#+" org.eventb.core.theorem="false"/>
<org.eventb.core.scAction name="load_at_oncf" org.eventb.core.assignment="busy_slots ≔ busy_slots+load_at_once" org.eventb.core.label="act1" org.eventb.core.source="/FerryBoat/initialModel.bum|org.eventb.core.machineFile#initialModel|org.eventb.core.event#.|org.eventb.core.action#*"/>
<org.eventb.core.scParameter name="load_at_once" org.eventb.core.source="/FerryBoat/initialModel.bum|org.eventb.core.machineFile#initialModel|org.eventb.core.event#.|org.eventb.core.parameter#'" org.eventb.core.type="ℤ"/>
<org.eventb.core.scGuard name="load_at_oncg" org.eventb.core.label="grd4_1" org.eventb.core.predicate="bs_m≥load_at_once" org.eventb.core.source="/ferryBoat/firstRef.bum|org.eventb.core.machineFile#firstRef|org.eventb.core.event#\/|org.eventb.core.guard#-" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="load_at_onch" org.eventb.core.label="grd5_1" org.eventb.core.predicate="max_bs_p(lift_level)≥load_at_once+bs_p(lift_level)" org.eventb.core.source="/ferryBoat/firstRef.bum|org.eventb.core.machineFile#firstRef|org.eventb.core.event#\/|org.eventb.core.guard#." org.eventb.core.theorem="false"/>
<org.eventb.core.scAction name="load_at_onci" org.eventb.core.assignment="bs_p ≔ bs_p{lift_level ↦ bs_p(lift_level)+load_at_once}" org.eventb.core.label="act2_1" org.eventb.core.source="/ferryBoat/firstRef.bum|org.eventb.core.machineFile#firstRef|org.eventb.core.event#\/|org.eventb.core.action#+"/>
<org.eventb.core.scAction name="load_at_oncj" org.eventb.core.assignment="bs_m ≔ bs_m − load_at_once" org.eventb.core.label="act3_1" org.eventb.core.source="/ferryBoat/firstRef.bum|org.eventb.core.machineFile#firstRef|org.eventb.core.event#\/|org.eventb.core.action#,"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="max_busy_slotx" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="Unboard" org.eventb.core.source="/ferryBoat/firstRef.bum|org.eventb.core.machineFile#firstRef|org.eventb.core.event#0">
<org.eventb.core.scRefinesEvent name="'" org.eventb.core.scTarget="/ferryBoat/initialModel.bcm|org.eventb.core.scMachineFile#initialModel|org.eventb.core.scEvent#max_busy_slotx" org.eventb.core.source="/ferryBoat/firstRef.bum|org.eventb.core.machineFile#firstRef|org.eventb.core.event#0|org.eventb.core.refinesEvent#'"/>
<org.eventb.core.scGuard name="'" org.eventb.core.label="grd1" org.eventb.core.predicate="unload_at_once∈ℕ1" org.eventb.core.source="/FerryBoat/initialModel.bum|org.eventb.core.machineFile#initialModel|org.eventb.core.event#\/|org.eventb.core.guard#(" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="(" org.eventb.core.label="grd2" org.eventb.core.predicate="unload_at_once≤busy_slots" org.eventb.core.source="/FerryBoat/initialModel.bum|org.eventb.core.machineFile#initialModel|org.eventb.core.event#\/|org.eventb.core.guard#+" org.eventb.core.theorem="false"/>
<org.eventb.core.scAction name="unload_at_oncf" org.eventb.core.assignment="busy_slots ≔ busy_slots − unload_at_once" org.eventb.core.label="act1" org.eventb.core.source="/FerryBoat/initialModel.bum|org.eventb.core.machineFile#initialModel|org.eventb.core.event#\/|org.eventb.core.action#*"/>
<org.eventb.core.scParameter name="unload_at_once" org.eventb.core.source="/FerryBoat/initialModel.bum|org.eventb.core.machineFile#initialModel|org.eventb.core.event#\/|org.eventb.core.parameter#'" org.eventb.core.type="ℤ"/>
<org.eventb.core.scGuard name="unload_at_oncg" org.eventb.core.label="grd3_1" org.eventb.core.predicate="bs_m+unload_at_once≤max_bs_m" org.eventb.core.source="/ferryBoat/firstRef.bum|org.eventb.core.machineFile#firstRef|org.eventb.core.event#0|org.eventb.core.guard#(" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="unload_at_onch" org.eventb.core.label="grd5_1" org.eventb.core.predicate="unload_at_once≤bs_p(lift_level)" org.eventb.core.source="/ferryBoat/firstRef.bum|org.eventb.core.machineFile#firstRef|org.eventb.core.event#0|org.eventb.core.guard#," org.eventb.core.theorem="false"/>
<org.eventb.core.scAction name="unload_at_onci" org.eventb.core.assignment="bs_m ≔ bs_m+unload_at_once" org.eventb.core.label="act2_1" org.eventb.core.source="/ferryBoat/firstRef.bum|org.eventb.core.machineFile#firstRef|org.eventb.core.event#0|org.eventb.core.action#*"/>
<org.eventb.core.scAction name="unload_at_oncj" org.eventb.core.assignment="bs_p ≔ bs_p{lift_level ↦ bs_p(lift_level) − unload_at_once}" org.eventb.core.label="act3_1" org.eventb.core.source="/ferryBoat/firstRef.bum|org.eventb.core.machineFile#firstRef|org.eventb.core.event#0|org.eventb.core.action#+"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="max_busy_sloty" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="MoveLift" org.eventb.core.source="/ferryBoat/firstRef.bum|org.eventb.core.machineFile#firstRef|org.eventb.core.event#G">
<org.eventb.core.scGuard name="'" org.eventb.core.label="grd1_1" org.eventb.core.predicate="selected_level∈floors" org.eventb.core.source="/ferryBoat/firstRef.bum|org.eventb.core.machineFile#firstRef|org.eventb.core.event#G|org.eventb.core.guard#(" org.eventb.core.theorem="false"/>
<org.eventb.core.scParameter name="selected_level" org.eventb.core.source="/ferryBoat/firstRef.bum|org.eventb.core.machineFile#firstRef|org.eventb.core.event#G|org.eventb.core.parameter#'" org.eventb.core.type="ℤ"/>
<org.eventb.core.scAction name="selected_levem" org.eventb.core.assignment="lift_level ≔ selected_level" org.eventb.core.label="act1_1" org.eventb.core.source="/ferryBoat/firstRef.bum|org.eventb.core.machineFile#firstRef|org.eventb.core.event#G|org.eventb.core.action#)"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="max_busy_slotz" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="BoardLift" org.eventb.core.source="/ferryBoat/firstRef.bum|org.eventb.core.machineFile#firstRef|org.eventb.core.event#H">
<org.eventb.core.scGuard name="'" org.eventb.core.label="grd1_1" org.eventb.core.predicate="spot_number∈ℕ1" org.eventb.core.source="/ferryBoat/firstRef.bum|org.eventb.core.machineFile#firstRef|org.eventb.core.event#H|org.eventb.core.guard#+" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="(" org.eventb.core.label="grd2_1" org.eventb.core.predicate="spot_number+bs_m≤max_bs_m" org.eventb.core.source="/ferryBoat/firstRef.bum|org.eventb.core.machineFile#firstRef|org.eventb.core.event#H|org.eventb.core.guard#(" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name=")" org.eventb.core.label="grd3_1" org.eventb.core.predicate="lift_level=1" org.eventb.core.source="/ferryBoat/firstRef.bum|org.eventb.core.machineFile#firstRef|org.eventb.core.event#H|org.eventb.core.guard#*" org.eventb.core.theorem="false"/>
<org.eventb.core.scParameter name="spot_number" org.eventb.core.source="/ferryBoat/firstRef.bum|org.eventb.core.machineFile#firstRef|org.eventb.core.event#H|org.eventb.core.parameter#'" org.eventb.core.type="ℤ"/>
<org.eventb.core.scAction name="spot_numbes" org.eventb.core.assignment="bs_m ≔ spot_number+bs_m" org.eventb.core.label="act1_1" org.eventb.core.source="/ferryBoat/firstRef.bum|org.eventb.core.machineFile#firstRef|org.eventb.core.event#H|org.eventb.core.action#)"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="max_busy_slot{" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="LeaveLift" org.eventb.core.source="/ferryBoat/firstRef.bum|org.eventb.core.machineFile#firstRef|org.eventb.core.event#M">
<org.eventb.core.scGuard name="'" org.eventb.core.label="grd1_1" org.eventb.core.predicate="at_once∈ℕ1" org.eventb.core.source="/ferryBoat/firstRef.bum|org.eventb.core.machineFile#firstRef|org.eventb.core.event#M|org.eventb.core.guard#(" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="(" org.eventb.core.label="grd2_1" org.eventb.core.predicate="bs_m>0∧at_once≤bs_m" org.eventb.core.source="/ferryBoat/firstRef.bum|org.eventb.core.machineFile#firstRef|org.eventb.core.event#M|org.eventb.core.guard#)" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name=")" org.eventb.core.label="grd3_1" org.eventb.core.predicate="lift_level=1" org.eventb.core.source="/ferryBoat/firstRef.bum|org.eventb.core.machineFile#firstRef|org.eventb.core.event#M|org.eventb.core.guard#+" org.eventb.core.theorem="false"/>
<org.eventb.core.scParameter name="at_once" org.eventb.core.source="/ferryBoat/firstRef.bum|org.eventb.core.machineFile#firstRef|org.eventb.core.event#M|org.eventb.core.parameter#'" org.eventb.core.type="ℤ"/>
<org.eventb.core.scAction name="at_oncf" org.eventb.core.assignment="bs_m ≔ bs_m − at_once" org.eventb.core.label="act1_1" org.eventb.core.source="/ferryBoat/firstRef.bum|org.eventb.core.machineFile#firstRef|org.eventb.core.event#M|org.eventb.core.action#*"/>
</org.eventb.core.scEvent>
</org.eventb.core.scMachineFile>