Modeling Awkward Social Situations with TLA+

Walkward!

You're walking down the street and need to pass someone going the opposite way. You take a step left, but they're thinking the same thing and take a step to their right, aka your left. You're still blocking each other. Then you take a step to the right, and they take a step to their left, and you're back to where you started. I've heard this called "walkwarding"

Let's model this in TLA+. TLA+ is a formal methods tool for finding bugs in complex software designs, most often involving concurrency. Two people trying to get past each other just also happens to be a concurrent system. A gentler introduction to TLA+'s capabilities is here, an in-depth guide teaching the language is here.

The spec

---- MODULE walkward ----
EXTENDS Integers

VARIABLES pos
vars == <<pos>>

Double equals defines a new operator, single equals is an equality check. <<pos>> is a sequence, aka array.

you == "you"
me == "me"
People == {you, me}

MaxPlace == 4

left == 0
right == 1

I've gotten into the habit of assigning string "symbols" to operators so that the compiler complains if I misspelled something. left and right are numbers so we can shift position with right - pos.

direction == [you |-> 1, me |-> -1]
goal == [you |-> MaxPlace, me |-> 1]

Init ==
  \* left-right, forward-backward
  pos = [you |-> [lr |-> left, fb |-> 1], me |-> [lr |-> left, fb |-> MaxPlace]]

direction, goal, and pos are "records", or hash tables with string keys. I can get my left-right position with pos.me.lr or pos["me"]["lr"] (or pos[me].lr, as me == "me").

Juke(person) ==
  pos' = [pos EXCEPT ![person].lr = right - @]

TLA+ breaks the world into a sequence of steps. In each step, pos is the value of pos in the current step and pos' is the value in the next step. The main outcome of this semantics is that we "assign" a new value to pos by declaring pos' equal to something. But the semantics also open up lots of cool tricks, like swapping two values with x' = y /\ y' = x.

TLA+ is a little weird about updating functions. To set f[x] = 3, you gotta write f' = [f EXCEPT ![x] = 3]. To make things a little easier, the rhs of a function update can contain @ for the old value. ![me].lr = right - @ is the same as right - pos[me].lr, so it swaps left and right.

("Juke" comes from here)

Move(person) ==
  LET new_pos == [pos[person] EXCEPT !.fb = @ + direction[person]]
  IN
    /\ pos[person].fb # goal[person]
    /\ \A p \in People: pos[p] # new_pos
    /\ pos' = [pos EXCEPT ![person] = new_pos]

The EXCEPT syntax can be used in regular definitions, too. This lets someone move one step in their goal direction unless they are at the goal or someone is already in that space. /\ means "and".

Next ==
  \E p \in People:
    \/ Move(p)
    \/ Juke(p)

I really like how TLA+ represents concurrency: "In each step, there is a person who either moves or jukes." It can take a few uses to really wrap your head around but it can express extraordinarily complicated distributed systems.

Spec == Init /\ [][Next]_vars

Liveness == <>(pos[me].fb = goal[me])
====

Spec is our specification: we start at Init and take a Next step every step.

Liveness is the generic term for "something good is guaranteed to happen", see here for more. <> means "eventually", so Liveness means "eventually my forward-backward position will be my goal". I could extend it to "both of us eventually reach out goal" but I think this is good enough for a demo.

Checking the spec

Four years ago, everybody in TLA+ used the toolbox. Now the community has collectively shifted over to using the VSCode extension.¹ VSCode requires we write a configuration file, which I will call walkward.cfg.

SPECIFICATION Spec
PROPERTY Liveness

I then check the model with the VSCode command TLA+: Check model with TLC. Unsurprisingly, it finds an error:

The reason it fails is "stuttering": I can get one step away from my goal and then just stop moving forever. We say the spec is unfair: it does not guarantee that if progress is always possible, progress will be made. If I want the spec to always make progress, I have to make some of the steps weakly fair.

+ Fairness == WF_vars(Next)

- Spec == Init /\ [][Next]_vars
+ Spec == Init /\ [][Next]_vars /\ Fairness

Now the spec is weakly fair, so someone will always do something. New error:

\* First six steps cut
7: <Move("me")>
pos = [you |-> [lr |-> 0, fb |-> 4], me |-> [lr |-> 1, fb |-> 2]]
8: <Juke("me")>
pos = [you |-> [lr |-> 0, fb |-> 4], me |-> [lr |-> 0, fb |-> 2]]
9: <Juke("me")> (back to state 7)

In this failure, I've successfully gotten past you, and then spend the rest of my life endlessly juking back and forth. The Next step keeps happening, so weak fairness is satisfied. What I actually want is for both my Move and my Juke to both be weakly fair independently of each other.

- Fairness == WF_vars(Next)
+ Fairness == WF_vars(Move(me)) /\ WF_vars(Juke(me))

If my liveness property also specified that you reached your goal, I could instead write \A p \in People: WF_vars(Move(p)) etc. I could also swap the \A with a \E to mean at least one of us is guaranteed to have fair actions, but not necessarily both of us.

New error:

3: <Move("me")>
pos = [you |-> [lr |-> 0, fb |-> 2], me |-> [lr |-> 0, fb |-> 3]]
4: <Juke("you")>
pos = [you |-> [lr |-> 1, fb |-> 2], me |-> [lr |-> 0, fb |-> 3]]
5: <Juke("me")>
pos = [you |-> [lr |-> 1, fb |-> 2], me |-> [lr |-> 1, fb |-> 3]]
6: <Juke("me")>
pos = [you |-> [lr |-> 1, fb |-> 2], me |-> [lr |-> 0, fb |-> 3]]
7: <Juke("you")> (back to state 3)

Now we're getting somewhere! This is the original walkwarding situation we wanted to capture. We're in each others way, then you juke, but before either of us can move you juke, then we both juke back. We can repeat this forever, trapped in a social hell.

Wait, but doesn't WF(Move(me)) guarantee I will eventually move? Yes, but only if a move is permanently available. In this case, it's not permanently available, because every couple of steps it's made temporarily unavailable.

How do I fix this? I can't add a rule saying that we only juke if we're blocked, because the whole point of walkwarding is that we're not coordinated. In the real world, walkwarding can go on for agonizing seconds. What I can do instead is say that Liveness holds as long as Move is strongly fair. Unlike weak fairness, strong fairness guarantees something happens if it keeps becoming possible, even with interruptions.

Liveness == 
+  SF_vars(Move(me)) => 
    <>(pos[me].fb = goal[me])

This makes the spec pass. Even if we weave back and forth for five minutes, as long as we eventually pass each other, I will reach my goal. Note we could also by making Move in Fairness strongly fair, which is preferable if we have a lot of different liveness properties to check.

A small exercise for the reader

There is a presumed invariant that is violated. Identify what it is, write it as a property in TLA+, and show the spec violates it. Then fix it.

Answer (in rot13): Gur vainevnag vf "ab gjb crbcyr ner va gur rknpg fnzr ybpngvba". Zbir thnenagrrf guvf ohg Whxr qbrf abg.

More TLA+ Exercises

I've started work on an exercises repo. There's only a handful of specific problems now but I'm planning on adding more over the summer.

If you're reading this on the web, you can subscribe here. Updates are once a week. My main website is here.

My new book, Logic for Programmers, is now in early access! Get it here.