Finished problem class 7

Author: Lewes

PC07_HotelReception/c0.bucx

@@ -0,0 +1,5 @@
+context c0
+sets
+  GUEST
+  ROOM
+end

PC07_HotelReception/m0.bumx

@@ -0,0 +1,36 @@
+machine m0
+sees c0
+variables
+  allocations
+invariants
+  @typeof-allocations: allocations ∈ ROOM ⤔ GUEST
+events
+
+	event INITIALISATION
+	then
+	  @init-allocations: allocations ≔ ∅
+	end
+
+    event CheckIn
+    any
+      g
+      r
+    where
+      @is-guest: g ∈ GUEST
+      @is-room: r ∈ ROOM
+      @guest-is-not-checked-in: g ∉ ran(allocations)
+      @room-is-free: r ∉ dom(allocations)
+    then
+      @allocate-room: allocations(r) ≔ g
+    end
+    
+    event CheckOut
+    any
+      g
+    where
+      @guest-is-checked-in: g ∈ ran(allocations)
+    then
+      @allocate-room: allocations ≔ allocations ⩥ {g}
+    end
+
+end

PC07_HotelReception/m1.bumx

@@ -0,0 +1,44 @@
+machine m1
+refines m0
+sees c0
+variables
+  allocations
+  rooms
+invariants
+  @typeof-rooms: rooms ⊆ ROOM
+  @typeof-allocations: allocations ∈ rooms ⤔ GUEST
+events
+	event INITIALISATION extends INITIALISATION
+	then
+	  @init-rooms: rooms ≔ ∅
+	end
+
+	event CheckIn extends CheckIn
+	where 
+	  @is-registered-room: r ∈ rooms
+	end
+
+	event CheckOut extends CheckOut
+	end
+	
+	event AddRoom
+	any
+	  r
+	where
+	  @is-room: r ∈ ROOM
+	  @is-not-registered: r ∉ rooms
+	then
+	  @add-room: rooms ≔ rooms ∪ {r}
+	end
+	
+	event RemoveRoom
+	any
+	  r
+	where
+	  @is-registered-room: r ∈ rooms
+	  @is-not-occupied: r ∉ dom(allocations)
+	then
+	  @remove-room: rooms ≔ rooms ∖ {r}
+	end
+
+end