SRC Research Report 127

TLA in Pictures

Leslie Lamport

Predicate-action diagrams, which are similar to standard state-transition diagrams, are interpreted as formulas of TLA (the Temporal Logic of Action). We explain how these diagrams can be used to describe aspects of a specification, even when the complete specification cannot be written as a diagram, and to illustrate proofs.

Back to the SRC Research Reports main page.

• PostScript compressed with UNIX compress -- 104 Kbytes
  
• PostScript compressed with GNU compress (gzip) -- 80 Kbytes
  
• PostScript compressed with ZIP -- 80 Kbytes
  
• PostScript -- 264 Kbytes
  
• Portable Document Format (PDF) -- 288 Kbytes