-
Notifications
You must be signed in to change notification settings - Fork 1
/
m0_cabins_context.buc
16 lines (16 loc) · 3.3 KB
/
m0_cabins_context.buc
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<org.eventb.core.contextFile org.eventb.core.configuration="org.eventb.core.fwd" org.eventb.core.generated="false" org.eventb.texttools.text_lastmodified="1590748863196" org.eventb.texttools.text_representation="context m0_cabins_context sets CABINS constants FLOORS TOP_FLOOR CABIN_FLOOR axioms @top_floor_INT TOP_FLOOR ∈ ℕ1 //REQ 3 @proB_no_timeout TOP_FLOOR = 7 //REQ 3 @floor_enum FLOORS = 0‥TOP_FLOOR //REQ 3 @fixed_num_cabins finite(CABINS) //REQ 1 @num_floors card(FLOORS) = TOP_FLOOR + 1 //REQ 3 @fixed_num_floors finite(FLOORS) //REQ 3 @max_num_cabins card(CABINS) < (card(FLOORS)∗2) //REQ 1 @init_cabin_floor CABIN_FLOOR ∈ CABINS → FLOORS @avoid_collisions ∀c·c ∈ dom(CABIN_FLOOR) ⇒ CABIN_FLOOR(c) ∉ ran({c} ⩤ CABIN_FLOOR) end" version="3">
<org.eventb.core.carrierSet name="_dp-v4J4VEeq9QKfOiT4EOw" org.eventb.core.generated="false" org.eventb.core.identifier="CABINS"/>
<org.eventb.core.constant name="_dp_W8Z4VEeq9QKfOiT4EOw" org.eventb.core.generated="false" org.eventb.core.identifier="FLOORS"/>
<org.eventb.core.constant name="_dp_-AJ4VEeq9QKfOiT4EOw" org.eventb.core.generated="false" org.eventb.core.identifier="TOP_FLOOR"/>
<org.eventb.core.constant name="_kbFmIJ6rEeqVQ6qy3MLSjQ" org.eventb.core.generated="false" org.eventb.core.identifier="CABIN_FLOOR"/>
<org.eventb.core.axiom name="_MsxEwJ6tEeqVQ6qy3MLSjQ" org.eventb.core.comment="REQ 3" org.eventb.core.generated="false" org.eventb.core.label="top_floor_INT" org.eventb.core.predicate="TOP_FLOOR ∈ ℕ1"/>
<org.eventb.core.axiom name="_Msxr0J6tEeqVQ6qy3MLSjQ" org.eventb.core.comment="REQ 3" org.eventb.core.generated="false" org.eventb.core.label="proB_no_timeout" org.eventb.core.predicate="TOP_FLOOR = 7"/>
<org.eventb.core.axiom name="_MsyS4J6tEeqVQ6qy3MLSjQ" org.eventb.core.comment="REQ 3" org.eventb.core.generated="false" org.eventb.core.label="floor_enum" org.eventb.core.predicate="FLOORS = 0‥TOP_FLOOR"/>
<org.eventb.core.axiom name="_M9xTMJ7DEeqVQ6qy3MLSjQ" org.eventb.core.comment="REQ 1" org.eventb.core.generated="false" org.eventb.core.label="fixed_num_cabins" org.eventb.core.predicate="finite(CABINS)"/>
<org.eventb.core.axiom name="_MszhAJ6tEeqVQ6qy3MLSjQ" org.eventb.core.comment="REQ 3" org.eventb.core.generated="false" org.eventb.core.label="num_floors" org.eventb.core.predicate="card(FLOORS) = TOP_FLOOR + 1"/>
<org.eventb.core.axiom name="_MszhAZ6tEeqVQ6qy3MLSjQ" org.eventb.core.comment="REQ 3" org.eventb.core.generated="false" org.eventb.core.label="fixed_num_floors" org.eventb.core.predicate="finite(FLOORS)"/>
<org.eventb.core.axiom name="_Rn7VMJ7DEeqVQ6qy3MLSjQ" org.eventb.core.comment="REQ 1" org.eventb.core.generated="false" org.eventb.core.label="max_num_cabins" org.eventb.core.predicate="card(CABINS) < (card(FLOORS)∗2)"/>
<org.eventb.core.axiom name="_Ms0vIJ6tEeqVQ6qy3MLSjQ" org.eventb.core.generated="false" org.eventb.core.label="init_cabin_floor" org.eventb.core.predicate="CABIN_FLOOR ∈ CABINS → FLOORS"/>
<org.eventb.core.axiom name="_Ms1WMJ6tEeqVQ6qy3MLSjQ" org.eventb.core.generated="false" org.eventb.core.label="avoid_collisions" org.eventb.core.predicate="∀c·c ∈ dom(CABIN_FLOOR) ⇒ CABIN_FLOOR(c) ∉ ran({c} ⩤ CABIN_FLOOR)"/>
</org.eventb.core.contextFile>