alper · October 4, 2019 09:51 · Oct 4, 2019 · Oct 3, 2019
diff --git a/seating.snt b/seating.snt
@@ -4,10 +4,11 @@ array2<int> rooms;
 rooms = [2, 3, 4, 5];
 
 
-# People are represented by a list of indexes of the rooms where they sit
+# People are represented by a list of indexes of the rooms where they sit (ten people in this case)
 array10<int> people;
 
 function respectCapacity? (people, roomNumber, capacity) {
+    # Make sure each room does not have more peopl in it than its capacity
     uses = people.countBy(function^ (allocatedRoom) {
         return allocatedRoom == roomNumber;
     });

diff --git a/seating.snt b/seating.snt
@@ -0,0 +1,35 @@
+array2<int> rooms;
+
+# Each room is represented by the maximum number of people that it can seat
+rooms = [2, 3, 4, 5];
+
+
+# People are represented by a list of indexes of the rooms where they sit
+array10<int> people;
+
+function respectCapacity? (people, roomNumber, capacity) {
+    uses = people.countBy(function^ (allocatedRoom) {
+        return allocatedRoom == roomNumber;
+    });
+
+    return uses <= capacity;
+};
+
+function wishes? (people) {
+    # People who want to be in the same room together
+
+    firstWish = people[1] == people[2];
+    secondWish = (people[6] == people[7]) && (people[7] == people[8]);
+    thirdWish = people[0] == people[4];
+
+    return firstWish && secondWish && thirdWish;
+};
+
+people.each(function^ (roomIndex, personNumber) {
+    invariant roomIndex.between?(0, rooms.count);
+    invariant people.wishes?;
+
+    invariant people.respectCapacity?(roomIndex, rooms[roomIndex]);
+});
+
+expose people;