Homework 3: TLA+ and Model Checking

This homework explores model and specification development with TLA+, the same toolkit you read about that is in use at Amazon, Microsoft, and other places.

The homework directory contains a file trafficlight.tla, which is a model of two traffic lights, each watching how the other behaves, waiting its turn to advance. Each light is modeled as an independently executing process. (Yes, a real traffic light is probably only sequential code, though this version would extend more easily to crosswalk signals, vehicle sensors, etc.)

It has two bugs (unless I made a mistake, in which case it has more :-p). Your job is to find them by writing properties that should be true of any reasonable two-way (two-road) traffic light, and running TLC (the TLA+ model checker) to see if the properties you want to be true are violated by this implementation.

You should also fix the bugs once you find them, and eventually submit:

• A fixed version of the traffic light

• Definitions for a selected set of correctness properties (those specified below)

• A response to the reflection section below

General Advice

TLA+ is a tool where most of the effort to improve the tool improves its capabilities, not its interface. Similarly, the PlusCal language used to define the traffic light model is a bit idiosyncratic, and more closely resembles Algol68 than modern languages. In short, TLA+ has a lot of sharp corners; most are there for a good reason, but the tooling is definitely designed for expert users, not novices like you. This is part of the reason I'm not asking you to write your own model! Try to follow these pieces of guidance, and you should avoid these sharp corners for now:

• PlusCal needs to be translated into TLA, which is what the model check actually looks at. Think of this like compiling your code --- if you make a change, then forget to recompile (re-translate), your next testing (model checking) run will check the old version.

• The fixes to this PlusCal model are small, local changes. There are not large chunks of missing code. There is no missing state. You don't need to write any procedures or new processes. If you're changing more than one line of code for each bug, you're probably overthinking things.

Related to the matter of "interface work": Apparently TLA+ running on Windows does not accept the .tla file I wrote (using TLA+ Toolbox) on my Mac, because it's sensitive to the difference in standard line endings on Windows vs. Unix.  If you're on Windows and run into trouble translating the PlusCal, try the wintrafficlight.tla file, which I've converted line endings for.  If you're not on windows, you may safely ignore this paragraph.

Resources

During this assignment, you'll need to consult resources on TLA+ to learn more details of how to write assertions. Here are an array of references:

• Week 5's lecture and slides

• Hillel Wayne's book, which was one of the reading options for Week 5's reading assignments (use the link from the syllabus to get the Drexel Libraries e-version). This book focuses on programs written in the PlusCal pseudo-code language, as the code in this assignment is.

o Hillel also has a handy reference for the temporal logic operators: https://learntla.com/temporal-logic/operators/

• Leslie Lamport's Specifying Systems (the other reading choice for week 5). This is the canonical reference on writing specifications in TLA. The first few chapters are reasonably readable even without a heavy math background, but some of the examples assume you're familiar with things like cache coherency protocols. The book only uses the TLA language, not PlusCal.

• Leslie Lamport has posted other resources as well, including a video course and a "Hyperbook", neither of which I've really looked at, but which you might consider if you don't like the earlier sources (I've heard from a number of people that each is quite good, but have not independently checked this).

Getting Started

If you haven't already, download and install the TLA+ Toolbox, which is essentially an Eclipse-based IDE for writing TLA+ models and specifications. If you're on Windows, download wintrafficlight.tla and save it as trafficlight.tla (TLA+ cares about the filename). Otherwise you can grap the file already named trafficlight.tla. (For the curious: TLA+ is still sensitive to line ending encodings across different platforms, and Windows does it differently from MacOS/Linux)

Loading the Project

File > Open Spec > Add New Spec... will give a dialog box. Navigate to where you unpacked the homework zip file, and select trafficlight.tla.

Place your cursor inside the (*--algorithm ... end algorithm;*) block, and press Ctrl+T (or Command+T on Mac) to translate the PlusCal code to TLA. The toolbox will emit a bunch of code into the buffer below the block you just translated. Every time you define or change a property, or tweak the code to fix a bug, you'll need to re-translate.

Now create a model checking configuration. Go to TLC Model Checker > New Model..., and give it a name (the name is for you to read, not the tool, so pick at will). This will create a new tab in the Toolbox. On the model overview tab, make sure to select the following:

• Under "What is the behavior spec?" make sure "Temporal Formula" is selected, and the textbox below it says "Spec" (this should already be the default, just make sure)

• Under "What to Check?":

o Make sure "Deadlock" is checked (it should be by default). This way TLC will ensure the traffic light implementation doesn't get stuck.

o Under "Invariants" click the "Add" button and type "ValidColors" (the name of a predicate defined in the code).

Now run this model, via the menu (TLC Model Checker > Run model), key (F11), or the green play/run button at the top of the Model Overview tab. You should see it do a bunch of work, and once the pop-up disappears you will see a Model Checking Results tab with a bunch of information. Among other things, at this point you should see "Errors Detected: No errors". If so, you have successfully gotten the model checker to ensure the traffic light colors are always red, green, and blue, and never (for example) purple. You're ready to start writing your own properties, checking them, and fixing the bugs for properties that fail.

Properties to Check

For each of the following properties, define the invariant or temporal formula, and run the model check to see if it's true of the traffic light model. See below for a recap of the difference between an invariant and a temporal formula.

1. Define an invariant Safe that requires one of the light directions to be red (i.e., either lights[0] is red, or lights[1] is red). (Using this as an invariant for the model checker will ensure it is true in all states, so one direction will always have red lights).

2. Define a temporal formula EventuallyGreen ensuring that each light is always eventually green.

3. Define a temporal formula EventuallyYellow ensuring that each light is always eventually yellow.

4. Define a temporal formula EventuallyRed ensuring that each light is always eventually red.

5. Challenge goal: Define a temporal formula LightOrder ensuring that for each light, it cycles through colors in the appropriate order (Green, Yellow, Red, and back to green, as opposed something like going from Red to Green). This is actually subtle to get fully correct, requiring use of primed (next-state) versions of flags.  You must attempt it, but any serious attempt will net full credit for this point.

The PlusCal code contains one or two mistakes depending on what you decide to change. It is possible that one of the bugs makes multiple of the above properties fail. When you know which properties are false, fix the model so the model checker succeeds in checking all invariants and temporal formulas. Each fix is a small change to a single line of code, so you'll make small changes to one or two lines of code.

Feeding them to the Model Checker

TLC considers two classes of formulas: invariants, and temporal properties.

An invariant is something that should be true in any state, and therefore only uses normal logical operators (and, or, not, implies) and predicates on state like checking if a value is in some set, as in the definition of ValidColors:

 ValidColors == (\A l \in {0,1}: lights[l] \in colors)

This defines ValidColors as a predicate that is true when for all (\A) values l in (\in) the set {0,1}, the value of lights[l] is in (\in) the set colors, defined earlier as the normal set of US traffic light colors.

To have TLC check an invariant, add it to the same list you added ValidColors to earlier.

TLC considers any formula that uses a temporal operator --- such as always ([]) or eventually (<>) --- to be a temporal formula, because it talks about the state of the program over time (specifically, relating one state of the program to future states of the program).

Note: this suggests the property you must write as an invariant should not use temporal operators!

You could for example define the temporal formula requiring that light 0 is eventually green (this is similar to, but not quite the same as, the second specification you're asked for):

 EventuallyGreenOnce == <>(lights[0] = "green")

To check a temporal property with TLC, in the "Model Overview" tab, below where you add invariants, there's a section called "Properties". Add the property name you'd like to check just as you did for invariants (make sure it's checked, as in, there is a mark in the check box for it). You'll see an already-provided "Termination" property listed, which should not be checked, and for this example won't pass the model checker (since the traffic light should run forever).

TLC can check all of these properties simultaneously, which is handy if you're confident they're all true (which should be the case at the end of this assignment). But as you're adding new properties, it's best to check one additional property at a time, so if something breaks you know which property is not true of the system.

If a Property Fails

If one of your properties causes TLA+ to report an error, there are two possibilities:

• You found a bug! or

• You wrote the property incorrectly!

If TLC reports an error, the first thing you should do is convince yourself (again) that you have expressed the correct property --- the one you intended. If you believe you have written the formal property definition that matches your intended meaning, look at the error trace TLC produces, and see if the sequence of program states reported corresponds to a validation of the property you intended to write. (If you think you translated the property to TLA correctly, but don't think the erroneous trace should be a problem for what you were trying to check, either your translation or your understanding of the property you're checking needs to be refined.) If you're convinced the trace from the failure report is indeed a violation of the property, this is a good sign that you've understood the property, translated it to a formal specification correctly, and you can look for the bug that caused the property to fail.

Reflection

Please consider the following questions, and write up a response. Your response can be point-by-point, or holistic, as long as you address all of the following:

• How does (mathematically) formal specification (just the specification, not the model checking) compare to property-based specification and traditional unit testing? What sorts of things seem easier to do well in each? You might consider things like ease of defining or building data structures, precision of the specification, learning curves, or other aspects (but you don't have to necessarily talk about each of those, or only those).

• How would you pursue (traditional) testing of liveness properties (i.e., always eventually P, eventually always P...)? This isn't meant to be a trick question, so to be clear, this isn't possible in general (an execution that violates a liveness property is infinitely long, so you can't write an assertion at the end). But how would you approach the problem of building confidence in one of these liveness properties being true of a piece of software using traditional techniques (or property-based)?

o "Building confidence" isn't meant to be subtle: remember that since most programs effectively have infinite possible inputs, and you can't test them all, traditional testing is meant to increase confidence, not show the program is absolutely correct.

• Several of our readings' authors have reported higher confidence making changes to real systems when they have a formal model they can query (e.g., PVS in the life-critical systems paper, or TLA+ in the Amazon paper). After this (comparatively short) experience, how do you think tools like this would affect your confidence making changes to a system? For example, consider if you were making changes to a traffic light to add turn signals or crosswalk signals. Would having a formal model make you more comfortable changing the design, not affect your confidence, or decrease your confidence? Why?

o The correct answer here is not what you think I might like to hear, but what you think, with the reasoning behind your thoughts clearly explained.