This project contains alternative definitions of commonly-used data structures:
-
Lists.tla are typed 0-based sequences of elements, as an alternative to untyped 1-based TLA+ Sequences.
-
Tuples.tla are typed constructors for TLA+ Tuples. When using these constructors, you do not need additional type annotations.
Our goal is not to replace the standard constructs of TLA+, but to provide specification writers with alternative definitions, if they need them. If you are looking for TLA+ definitions for all life circumstances, check TLA+ Community Modules.
For example, too many people were wondering, why indices of TLA+ sequences start with 1? Why cannot they start with zero? The answer is simple: They can, Lists.tla contains definitions like that. To avoid name collisions with TLA+ Sequences, we use alternative names that you can find in programming languages.
\* with Sequences
<<1, 2, 3>>[2] = 2
<<2, 3>> \o <<5, 6>> = <<2, 3, 5, 6>>
\* with Lists
At(List(<<1, 2, 3>>), 1) = 2
Concat(List(<<2, 3>>), List(<<5, 6>>)) = List(<<2, 3, 5, 6>>)
\* standard TLA+: a triple is also a sequence
<<5, 6>>
<<1, 2, 3>>
\* with Tuples: a triple that is definitely annotated as a tuple
Pair(5, 6)
T2(5, 6)
T3(1, 2, 3)How to pronounce TLAki? [tee-el-ay-kee]. In my mother tongue, the suffix '-ki' usually points to little or cute things, animals, or people. Like, in Pirozhki.