A Simple TLA Formula

The following formula provides a simple introduction to TLA. Start by middle-clicking on the Pi on the left-hand side. Then click on the different parts of the formula to find out what they mean.

   Pi  ==  (x = 0) /\ [][x' = x+1]  /\ WF (x' = x+1)
                                  x      x

A Slightly More Complicated TLA Formula

Choose one of the viewing modes at the bottom of the window, and then explore this specification, starting with the Phi on the left-hand side.

   Phi  ==  Init /\ [][AX \/ AY]       /\ WF      (AX)
                                <x, y>      <x, y>

An Enlightening Theorem

This theorem explains hiding in TLA. Remember to choose the viewing mode at the bottom of the window.

   |=  Pi \equiv \EE y : Phi

You can view formulas in in two different modes: Definition Mode, in which clicking on a symbol reveals its definition, and Explanation Mode, in which clicking on an expression describes its meaning. Use the "menu bar" at the bottom of the window to choose the viewing mode.

               Click here for Explanation Mode       You are in Definition Mode