Isabelle/TLA

This Web page describes my encoding of Lamport's Temporal Logic of Actions in the higher-order logic of the generic interactive proof assistant Isabelle.

Downloading

The TLA embedding comes with the standard distribution of Isabelle, no separate download is required. It includes a number of examples that should help you to get started.

In order to work with TLA, you should first build a heap with TLA built-in. To do that, change to the directory src/HOL/TLA below the Isabelle installation directory and issue the command

   isatool usedir -b HOL TLA

(assuming isatool is in your search path). If all goes well, you should see output similar to

   Building TLA ...
   Finished TLA (0:00:24 elapsed time)

This will create a heap file in your isabelle directory (usually located beneath your home directory, look in ~/isabelle/heaps/). Be careful, heap files tend to be large, probably on the order of 20MB!

You may also want to generate the theory browsing information for TLA. To do this, change to the src/HOL directory (i.e., the one just above the directory containing the TLA sources) and issue the command

   isatool usedir -i true HOL TLA

The output should now look like

   Running HOL-TLA ...
   Finished HOL-TLA (0:00:08 elapsed time)

The generated HTML files reside in ~/isabelle/browser_info/HOL/TLA. Alternatively, they can be browsed on the Isabelle WWW server. Similar commands can be used to generate the files for the TLA examples.

To run the examples or create your own TLA projects, you should tell Isabelle to use the TLA heap instead of the default one (usually HOL). If you are using ProofGeneral, you can enter the name of the heap to use when processing a theory file (you may have to enable an option allowing for interactive selection of the heap file). Also, since TLA is based on the traditional interface to Isabelle instead of the newer Isar interface, be sure to invoke ProofGeneral via Isabelle -I false.

Documentation

Isabelle/TLA is based on a complete axiomatization of the "raw" (stuttering-sensitive) variant of TLA. Here are two notes on the design of the prover and on a completeness proof for the underlying axiom system.

The distribution contains a few examples, including

the increment example from Lamport's TLA paper
the proof of the RPC-Memory case study, which is described in a paper by Abadi, Lamport, and Merz.

Isabelle/TLA should be extended to provide an embedding of Lamport's TLA+ specification language (based on ZF set theory instead of HOL), and it should be updated for the more recent Isar interface to Isabelle. While I may eventually do this myself, I'd be happy to help anybody willing to undertake this.

Please let me know about any comments or suggestions.

Stephan Merz