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 (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;
    });

    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;