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.
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
isatoolis 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
isabelledirectory (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
(i.e., the one just above the directory containing
the TLA sources) and issue the command
isatool usedir -i true HOL TLAThe 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.
The distribution contains a few examples, including
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.