Sadraskol

Modeling the train reservation kata - Part 2

In our last article, we covered the basics of TLA+. This article is about the last rule left to implement: we want ideally 70% of coach occupation. Before implementing the rule, let's refine the implementation of our algorithm.

Refining implementation

So far our specification describes an abstract algorithm. We choose seats randomly in the train which would certainly not be the case of a real world implementation. Let's refine the Reserve action to a more realistic approach.

We need to choose between a lot of alternatives. Let's say that our database imposes us to reserve seats in a numerical order order, A1 first then A2 and so forth. For instance:

Reserving in order

To order seats, we need to compare them. We implement an \prec operator to do so:

a \prec b == \/ a[1] < b[1]
             \/ a[1] = b[1] /\ a[2] < b[2]

In the formula, a and b are two different seats. Remember they are something like <<"A", 1>> or <<"B", 5>>. The issue is that TLA+ does not implement comparison for strings. We can easily alleviate this issue by replacing coach labels with numbers. So:

Coaches = 1..2

We now have to express the idea of reserving in order. If you were to implement it in a regular language, you'd use something like:

seats.sort(SeatOrdering).take(n);

This javascript expression is descriptive of the how: we first order the list of seats, and then take the n first items. It tells how the n first seats are selected, but now what it means to be the n first seats. For TLA+ we need to change our mindset: what does it mean to reserve the first free seats. First we know that it is a subset of n seats. So we can still write:

SequenceSeatsStrategy(seats, count) ==
    /\ Cardinality(seats) = count
    /\ SameCoach(seats)
    /\ reservations' = reservations \union {seats}

What does it mean to have successive seats reservation in set theory? You could start by stating that every seats in the current reservation needs to be below the new reservation. But this condition does not guarantee to have holes in your reservation. So we can refine this definition by not allowing holes in the reservation: there is no remaining free seat within the reserved seats.

SequenceSeatsStrategy(seats, count) ==
    /\ Cardinality(seats) = count
    /\ SameCoach(seats)
    /\ ~(\E s \in FreeSeats \ seats: \E t \in seats: s \prec t)
    /\ reservations' = reservations \union {seats}

The ~ operator is the proposition negation. We read the expression "There is no seat such as...". Why don't we write FreeSeats' using the ' operator instead of FreeSeats \ seats? We just cannot write that. The ' next state operator only works for describing the next state, not querying it.

You verify that the specification is still valid with our previous invariants.

Expressing the last rule

Instead of trying to explain the ideal 70% rule, let's study the ambiguous case for which this rule isn't clear. Let's say two coaches have respectively 5 seats reserved and 6. How should we place a reservation of 3 seats:

Reserving 3 seats in different configurations.

We know that our current implementation does not respect these scenarios. Do both respect the third rule "Ideally, all coaches have 70% occupation"? "Ideally" is relative to your experience. The rule is more interesting with more ambiguity, so we allow both cases to occur.

Let's first try to understand the rule in our interpretation: for any reservation, either the coach respects its 70% occupation, or there is no other coach which has enough free seats to handle the reservation. We want the 70% rule to be violated in last resort.

There is a little problem: so far we stated reservations to be a set, an unordered collection. There is no way to get to the "last" reservation since the order of reservations is not maintained. We need to refactor our whole spec to use the ordered collection: sequences.

We already used sequences as tuples, but this time we want to have variable length collection. The easiest change is the Init action:

Init == reservations = <<>>

We then replace the reservation state change with the Append operation of sequences:

reservations' = Append(reservations, seats)

Changing the type of the variable means we need to change the type checking we set at the start:

TypeCheck == \A i \in DOMAIN reservations: reservations[i] \in SUBSET Seats

Sets have a native way of exploring the values with the \in operator. Unfortunately TLA+ does not have the equivalent syntax for sequences. We use instead the DOMAIN keyword that provides all keys of a structure, in the case of sequences, the set of indexes. Be aware that since the return of DOMAIN is a set, it is not ordered and there are no guarantees on the order in which the indexes are iterated over.

Now we run our refactored specification. We check that even though we have changed the state of reservations, from an unordered set to a sequence, there's no violation of our previous invariants. TLA+ is pretty solid. Time to implement the invariant for the last rule. First we need to find the number of seats reserved by coach:

ReservationCountFor(coach) == Cardinality({<<c, _i>> \in ReservedSeats: c = coach})

We have already met this syntax when trying to count the occurence of the same seat in reservations in the SeatsCanBeReservedOnce invariant. As the name suggest, this time we count the number of seat reserved in a given coach.

Next we want to find the coach of a given reservation. We are going to use our friend CHOOSE:

ReservationCoach(reservation) == (CHOOSE seat \in reservation: TRUE)[1]

CHOOSE provides a way of selecting an element of a set respecting a predicate. CHOOSE x \in {1, 2, 3}: x % 2 = 1 returns either 1 or 3, the two odd numbers of the set. Note that TLA+ does not guarantee to be fair in the selection. In our case, the predicate is TRUE, meaning we select any seat in the reservation. We Finally we need to select the latest reservation made:

LatestReservation == reservations[Len(reservations)]

Len yield the same result for sequences as Cardinality for sets. Sequences are 1-indexed. They start at index 1, not index 0 as most programming languages. We have all we need to check the third rule:

LatestReservationShouldNotHaveBeenMadeIfAnotherCoachCanReceiveItWhileKeepingUnder70PercentOccupation ==
    \/ reservations = <<>>
    \/ ReservationCountFor(ReservationCoach(LatestReservation)) <= 70PercentCoachOccupation
    \/ ~(\E other \in Coaches: ReservationCountFor(other) + Cardinality(LatestReservation) <= 70PercentCoachOccupation)

The name of this invariant is over the top. I love it and hate it at the same time. We have three possibilities:

The first predicate allows the Init state to check the invariant. Other state contains at least a reservation and one of the two other predicate has to be true.

Our current specification violates this final rule, and the first found example shows why.

Final implementation

Now that we finally expressed the three rules and checked that our current algorithm does not respect them, let's choose a better algorithm. There are many options and we advise you to take some time to think about it. Even try implementing it in TLA+! We choose to reserve this way: reservations will be made in the least occupied coach.

LeastOccupiedCoach == CHOOSE c \in Coaches: \A x \in Coaches:
    ReservationCountFor(c) <= ReservationCountFor(x)

LeastOccupiedCoachStrategy(seats, count) ==
    /\ \A <<c, _i>> \in seats: c = LeastOccupiedCoach
    /\ Cardinality(seats) = count
    /\ count <= Cardinality(SeatNumbers)
    /\ reservations' = Append(reservations, seats)

We already covered all the operators used here. CHOOSE is used to select the least occupied coach, if two coaches are candidate, any of them would do. The rest is familiar.

Conclusion

Implementing the final specification takes me between 1 and 2 hours of work. TLA+ has this incredible power of letting logic drive the algorithm design, and not language features or implementation details. It yields a much clearer mental model of the problem at hand.

You might think that this specification is useless: you could have made it in your head. We did not try to convince you otherwise. These articles are an introduction to TLA+ syntax, and a discovery of the train reservation kata. If you want to challenge TLA+ you could:

If you have to think of all the possible scenarios of such systems in your head, you need a lot of time and end up with an headache and no clear call on the correctness of your design. TLA+ and formal methods allow to explore tons of scenarios while learning a lot from your system.