This is an old revision of the document!
PHP's gd library is missing or unable to create PNG images
Parsing TLA⁺ Syntax
TLA⁺ is a large, complicated, and ambiguous language that takes a huge amount of work to parse correctly & completely. This is assisted by a comprehensive test corpus exercises the language's nooks & crannies, but here we will make life easy on ourselves. This tutorial only uses a minimal subset of TLA⁺ syntax, just enough to handle the classic DieHard spec. You are encouraged to extend this minimal core as you wish; language tooling is best developed incrementally! Slowly filling in the details of this rough language sketch has a satisfying meditative aspect.