hwayne/learntla-v2

Learn TLA+ for free! No prior experience necessary!

Learntla V2

A guide to learning the TLA+ specification language. Going to be a gigantic mess right now, will be a while before the dust settles.

Usage

Installation

Requires Python 3.10.

git clone https://github.com/hwayne/learntla-v2.git
python -m venv learntla-v2
# Activate the venv yo
python -m pip install -r requirements.txt

Building

# with todos
sphinx-build docs/ docs/_build/html/

# without todos
sphinx-build -D todo_include_todos=0 docs/ docs/_build/html/

# check links for issues
sphinx-build -b linkcheck docs/ docs/_build/

Working with Specs

See the raw-specs readme for explanation of what these are for.

To expand an xml template:

# dryrun
python expand_template.py --dryrun file.xml

# actually write files
python expand_template.py file.xml

To process a spec, write

# one file
python process_spec.py file.tla

# every file in a folder
ConvertFolder.ps1 folder

Watcher.ps1

Builds the site whenever an rst file changes. Can be ignored, unnecessary for development.

Requires

Install-Module -Name FSWatcherEngineEvent

learntla-v2's Issues

confusion about labels in overview -> specification

in overview -> specification the following bullet point is confusing to me coming in with zero knowledge:

Each step of the algorithm belongs to a separate label. The labels determine what happens atomically and what can be interrupted by another process. That way we can represent race conditions.

each of the other bullet points reference text from the spec for what is being explained (like People and acct) but this one does not. After following the link, I assume Check:, Withdraw:, and Deposit: are the labels, but I'm not 100% sure and just have to continue reading.

clarification on model checking completion vs. system termination

referring to here

We modify the reader to have an infinite loop but model checking completes successfully. When I enable the generated Termination property I see that the system does not terminate (as expected), but I was confused before digging deeper and discovering this. At first, I expected some sort of error when running model checking due to the system generating an infinite number of "actions". After thinking about this more and knowing the behavior, I think this is because there can be a finite number of states to check even if the path through those states does not terminate - but I'm not 100% sure.

Maybe it's worth clarifying for the inexperienced reader that the model checking can complete even if the modeled system does not terminate and helping to build the mental model of why that is the case?

Token

In operators.rst you're contrasting strings and tokens. I'm not sure everyone really has a good mental model for "token".

OTOH it's fine to decide that this is prerequisite knowledge.

"the field of computer scientist" in FAQ - "computer science"?

"“Formal methods” is, very roughly, the field of computer scientist dedicated to writing correct programs." on https://learntla.com/intro/faq.html.

Update sphinx from 4.4.0 to 7.2.2

I don't know what features exactly this is gonna get us but I've fallen behind on these kinds of upgrades before and do not recommend it

Ever checked the https://lamport.azurewebsites.net/tla/practical-tla.html?

Hi, Hillel.
I loved your Learn TLA+ tutorial, and I was so fascinated by the second version of the book.

As I go through the TLA+ website, I found that Lamport already said something about your book https://lamport.azurewebsites.net/tla/practical-tla.html.

I guess there is some overlapping in the content between the book and this tutorial, more or less.

And if you haven't checked it yet, I guess you may look at it, you might find something useful. :-D

Cutoff sentence in "Writing Specifications"

This sentence here is cut off:

Not all blocks have to have the same number of labels! Conditionals trigger different behavior, which can take different amounts of
time. If you have a lot of

Question about > vs. = in example.

operators.rst:

{t \in ClockType: t[2] = 29 /\ t[3] = 0}

Why not t[2] = 30? We're 1-indexing, right?

At first I misunderstood that as “all the times in the second half of the hour” and wondered why there isn't a > anywhere. Maybe check if others misread it similarly?

A set of suggestions and confusing bits

This is a set of all the suggestions I had or confusing things I noticed during a read-through. I hope you don't mind the list of unrelated items here, but I didn't want to spam the issues board. I know this is very much a work in progress so some issues aren't unexpected -- thanks for making this resource, and take or leave these suggestions as you wish.

1. I thought it would be worth mentioning that pc probably stands for program counter.
2. A sentence in "Writing an Invariant > Quantifiers" says "That's for two reasons", but then the text appears to give three reasons.
3. The fact that A => B is equivalent to ~A \/ B was the most helpful piece to help me understand =>. Many programmers are already have an intuition for this form. It could be just me, but explaining it like "~A \/ B is really helpful, so TLA+ gives us syntactic sugar in the form of =>" would make for a more natural explanation. Just something to consider.
4. "State sweeping" is defined twice in the Tip in the Structured Data chapter ("State sweeping is when...", then "... trick known as state sweeping").
5. In "Temporal Properties > Strong Fairness", <> is used in an example spec before it is defined.
6. In "TLA+ > Fairness in TLA+", the fairness definitions use WF_v and SF_v, but the English explanation uses WF_x and WF_vars. This is kind of confusing. Does it matter?
7. Related to the previous comment, a discussion of how TLA+ treats underscores might be helpful. It is very surprising that underscores convey meaning. In every language I've used, they are just identifier characters, but in TLA+ they seem to be used as some sort of special separator. Is that right? Some clarification might be helpful.
8. <=> is used in "General Tips" and /= in the Goroutines example without either being defined. (The /= looks like it could be #?)
9. In "Using the Toolbox > Module Configuration" there is an unfinished sentence: "On the Model Overview page of a model, there are three This is not comprehensive."

clarification on efficiency of CHOOSE in introduction

the CHOOSE section states:

Here’s another thing we could do:

1. Take the set of all possible clock values.
2. Pick the element in the set that, when converted to seconds, gives us the value.

We don’t do it this way because “the set of all possible clock values” is over 80,000 elements long and doing a find on an 80,000 element list is a waste of resources. But it more closely matches the definition of the conversion, making it more useful for specification. In TLA+ we can write the selection like this:

ToClock(seconds) == CHOOSE x \in ClockType: ToSeconds(x) = seconds

It's unclear to me if doing it this way actually is a waste of resources (maybe implying there is a better way?) or if it is the best practice for doing this type of operation (I'm guessing this is the case from the text).

clarification on fairness

in the Fairness in TLA+ section, it was unclear to me thatWF_v and SF_v were for weakly and strongly fair until I looked them up in the manual.

Feature Request: eBook build target

There have been a couple of times I have found great online content and wanted to have it on my Kindle. In both cases it was relatively easy to convert the content from the scraped HTML to epub (and then mobi).

I suspect it would be easy to make an epub build target for Learn TLA+ v.2 also.

Add Randomization.tla to Standard Modules

https://www.learntla.com/reference/standard-library.html

Error in definition of IsComposite

The definition of IsComposite in the Quantifiers section of Writing an Invariant is:

IsComposite(num) ==
\E m, n \in 2..Len(num):
m * n = num

I believe it should be:

IsComposite(num) ==
\E m, n \in 2..num:
m * n = num

Clarify the 8 existing TLA+ types

Values starts with:

TLA+ is an “untyped” language, due to its roots in mathematics. In practice, the model checker recognizes four primitive types and four advanced ones.
But these types are not explicitly (or at least not explicitly enough) demonstrated to the reader.

To address this, I think a simple list with links to the relevant part of the book would suffice.

Duplication checker: itself self-explanatory, text around it confusing

Description

The writing specifications page says this of the duplication checker:

1. Create an empty set seen, then step through the elements of seq.

2. Every time we see a number, we check if it's already in seen.

   • If it is, we say the list is not unique.
   • Otherwise, we add the element to seen and continue.

3. If we reach the end and haven't seen any duplicate elements, we say the list is unique.

4. Our decision should match the operator IsUnique(seq).

In this chapter we'll focus on just writing out the spec, parts (2) and (3). In the next chapter we'll do steps (1) and (4), actually verifying the algorithm.

But the example plainly does do steps 1, 2, 3. Does the segment

In this chapter we'll focus on just writing out the spec, parts (2) and (3). In the next chapter we'll do steps (1) and (4), actually verifying the algorithm.

perhaps refer to an earlier list of activities that the user is to do?

problem statement

Suggest that IsUnique(seq) is a misleading name, and that something like ContainsNoDuplicates(seq) expresses the intent better. Similarly, if we reach the end and haven’t seen any duplicate elements, we might better say the elements of the list is_are_ unique.

Consider mentioning TLAPS in "Refactor Properties"

Instead of having TLC check refactor properties, TLAPS is occasionally able to help:

    Linearizability == LET Ops == {o \in Operations : LSN[o] # 0}
                       IN  \A i, j \in Ops :
                       times[j][2] # Pending
                            => (times[i][1] >= times[j][2] => LSN[i] >= LSN[j])

    LinearizabilityRef ==
        \A i, j \in Operations :
            /\ LSN[i] # 0 /\ LSN[j] # 0
            /\ times[j][2] # Pending
            => (times[i][1] >= times[j][2] => LSN[i] >= LSN[j])

    THEOREM LinearizabilityRef <=> Linearizability
    BY DEF  Linearizability, LinearizabilityRef

feature request: pluscal/tla cheatsheet

While going through the website and trying to write some specs, it was noticeable that there's a certain lack of a page that puts it all together in a way that one can easily refer to and see the big picture.

As an example I can give this, a really nice Rust cheatsheet page.

Due to the semantic differences in basic operators between PlusCal/TLA and conventional languages, I think this could be something that would help people to more easily onboard.

It is, however, an undertaking, but it would definitely be useful.

The Standard Modules page exists, and it could be repurposed to do this. It appears that the current purpose of the page is to serve as a "standard library" equivalent for Pluscal/TLA. However, given that the standard library is pretty mature (and lean), it might be more informative and helpful to just "spec it all out" with the stuff that's been left out - the actual nuts and bolts that are given in the guide (from the most basic things like operators, conditionals, logical operators, etc). I find myself running through the entire guide trying to figure out how to do very basic things still, and it's definitely a time consumer since one needs to keep a mind-map of where a given concept has been introduced. This is especially noticeable in the first few chapters where all the basics are spread out.

Would be interested to hear what you think of this.

Java module overrides are hard

https://learntla.com/topics/optimization.html#use-overrides suggests creating Java module overrides. Due to the fact that TLC's value classes are largely undocumented and have subtle behavior, writing module overrides is not easy. A slightly more accessible approach is perhaps to guide users towards depending on the CommunityModules, which already provide several module overrides for costly operators.

How to make a scratch file?

In the section Setup > Making a Scratchfile, the paragraph only mentions

To do that, I have a separate file I call “Scratch”

Yet how to create this separate file is not mentioned. I started looking for "New File" without success.

There is also a strong relation that a file is a module, so I started looking for "New Module", which I found, but it not mentioned in the guide makes me unsure what to make of it.

Finally I remember that the guide until this point only mentioned creating spec, and creating a separate scratch spec works.

For the scratch spec, the screenshot shows the file name to be lowercase "scratch", but the listed code has titlecase MODULE Scratch which led to an error.

For the scratch model, the screenshot shows the Value box to the bottom, but the text reads "the output of Eval will be put on the box to the right."

Warn that a set has to be symmetric when it is declared symmetric

After recently witnessing yet another instance of a set being mistakenly declared as symmetric when it is actually not, I would like to propose that users be reminded of their responsibility to ensure that a set is indeed symmetry (https://learntla.com/topics/optimization.html#use-symmetry-sets). Additionally, symmetry reduction should not be on while liveness checking.

https://tla.msr-inria.inria.fr/tlatoolbox/doc/model/model-values.html

"And if you’re not already testing, TLA+ isn’t the best investment.2"

In "And if you’re not already testing, TLA+ isn’t the best investment.2" (ooh NICE, copy-paste as Markdown!) the 2 should show up as a superscript, shouldn't it?

(The eSpark reference has the same problem, so maybe that's the style?)

Core->Setup: No Overdrafts in Invariants results in error

File

docs/core/setup.rst

Problem

Adding "No Overdrafts" as an Invariant results in an error when trying to run the model.

Error

***Parse Error***
Was expecting "=== or more Module body"
Encountered "Overdrafts" in Invariants at line 1 and token "No"

Residual stack trace follows:
Module definition starting at line 1, column 1.

Comments

I am complete beginner. I have never heard of TLA or touched it before.
I redid the guide from scratch an extra time just to make sure I didn't do anything wrong. But I got the same error both times.

My Setup

OS: Windows 10 (running in a VM)
Cores: 1
RAM: 4G
Java: Version 8 Update 333 (build 1.8.0_333-b02)
Toolbox: https://github.com/tlaplus/tlaplus/releases/tag/v1.8.0
Exec: Unpacked TLAToolbox-1.8.0-win32.win32.x86_64.zip and ran toolbox.exe

confusion about the text "writing `INVARIANT P`"

always/box section says:

[]P means that P is true in every state. When on the outside of a predicate, this is equivalent to an invariant, and in fact is how TLC supports them: writing INVARIANT P is the same as writing PROPERTY []P.

Having read through core linearly up to here, I don't know what "writing INVARIANT P" means. Examples have only configured invariants with the Model Overview GUI - is this referencing a way to write the model checker properties as config?

clarification on EXCEPT

the except section includes:

What we actually wanted to write is that s' is the same as s except that s[1] is false. Here’s the syntax for that:

Next == s' = [s EXCEPT ![1] = FALSE]

Yes, I know it’s really awkward. No, I can’t think of anything better.

Could you clarify why the ! is necessary? To me it seems like a double-negative as I read the line in my head as "the sequence s except that not the the first index has value is FALSE". On first reading I actually expected this to modify index 2+ (all indexes not the first) due to the ! and would have thought that [s EXCEPT [1] = FALSE] would do as intended.

I found the text explaining how you think about the colon earlier very useful for being able to read the code better.

I’ve found that the best way to remember which is which is by reading the colon as a “where”. So the map is “x squared where x in 1..4”, while the filter is “x in 1..4 where x is even”.

How do you think about the meaning of Next == s' = [s EXCEPT ![1] = FALSE]?

Vocabulary

It's bewildering to me that the first example specification in the body text contains only a thing called an algorithm, which moreover doesn't seem to do anything meaningful. I understand that it's just a syntactically valid lump to use to point at to name some parts but my autistic brain gets stopped at this point. It's…an algorithm, says so right there, algorithm and it talks about changing some variables. So what does it specify, if it's a specification?

Reduce memory allocation Windows issue

Linux and macOS allocate memory lazily while Windows allocates memory eagerly: https://learntla.com/topics/optimization.html#use-refactor-properties

syntax highlighting bug in Structured Data part

In the tip section within Function sets:

A function set of form [A -> B] will have 
 elements in it. If there were two tasks and three CPUs, that would be :math`(2^3)^2 = 64` possible functions.

Here, :math should be changed to whatever should yield the right result or simply be removed in favor of the usual syntax highlighting

feature request: all images should be clickable

Something that I noticed while reading this is that the often attached images aren't clickable. It would be nice to have them all clickable, ideally opening in a new tab. As of right now the flow to actually viewing them is right-clicking and then opening the image in a new tab/window. It's a bit clunky however necessary more often than not. Especially since most of the screenshots aren't properly cropped and in their natural state (for laptop users) they aren't legible.

I'm happy to go through the docs and do the change if it's OK.

Make a 404 page that tells people about the legacy site

So that older links to specific learntla pages on the old site don't all break

Wording of "new" types

operators.rst:

If you want to get on ahead, the new types we are not talking about are model values <model_value>, structs <struct>, and
functions <function>. Yes, operators and functions are different things.

Sorry, this had me stumble, because I wasn't sure what “new” refers to here. I surmised that it might be the ones not covered now, but the wording seemed strange and it had me count in the right sidebar if 3 types were missing from the 4+4. Which wasn't easy, because the structure in the sidebar isn't meant to support this counting. Maybe just leave out the “new”?

Structured data chapter improvements

Now what about an operator that sorts as a sequence? Specifically, one such that IsSorted(SortSeq(seq)) is always true. That’s easy:

Sort(seq) ==
  <<>>

We had to tweak the definition a bit and make sure that the output sequence has all the same elements, too.

The phrasing of this sentence is not clear, and together with the example operator, it appears that the operator is one that simply returns an empty sequence for any given input. In that case, it does not seem to "sort" anything. It is also not clear what changes to the definition were made and since the output sequence is an empty sequence, the last sentence is even more confusing.
I do understand that an empty sequence may satisfy any picked indices since the set is empty, therefore landing on the edge case that any two picked indices in an empty set will satisfy the condition; if that was the intention behind it, clarifying this somehow might be helpful.
Nit: before the actual code snippet there's mentioning of SortSeq but the example has Sort. Aligning them might be useful too.

---

Then [DOMAIN seq -> Range(seq)] is the set of all sequences which have the same elements as seq. Our operator will then look something like this...

I've tried to wrap my head around it multiple times halfway successfully. Range(seq) here is the set of all unique elements in the given input seq. DOMAIN seq here should be {<<1,2,3>>} (since seq is a sequence and it's domain is the actual indices). Therefore how can "[DOMAIN seq -> Range(seq)]" do the actual value indirection + different permutations of the values? Maybe a word on "how to read" could help here

---

For the Summary section in this chapter, there's no reference to Function sets. It would be useful to have a succinct description which would help remember how they work and their intended use-case along with the syntax.

Error in definition of IsComposite

The definition of IsComposite in the Quantifiers section of Writing an Invariant is:

IsComposite(num) ==
\E m, n \in 2..Len(num):
m * n = num

I believe it should be:

Come up with good exercises

Now that there's an exercise directive I can start putting exercises in the text. What are some good ones? Feel free to drop them here and I'll add some I like

Clarify model for the threads example

For the threads example in the concurrency section there is no indication on how assign the constant NULL when running the model after adding the lock. I think it might be a good idea to explicitly state how to run the model.

If I understand correctly both assigning a model variable or an ordinary assignment of, say, -1 would work equally well in this case, but the model variable would be preferable. If that's the case it might also be a good idea to explain the difference between both possibilities.

Typo in the number of functions when explaining function sets?

I think there's a typo in https://github.com/hwayne/learntla-v2/blob/master/docs/core/functions.rst?plain=1#L239

IMO it should be 3^2 = 9 functions when calculating functions mapping 2 tasks with 3 CPUs.

Typo in example or guard semantics unclear?

The conceptual overview starts with pseudocode:

and naively I read this as python-ish code, where the if is controlling whether the other two lines run, in which case I think the guard expression is backwards (from.balance should be greater than or equal to the amount for it to work?)

(but perhaps some other pseudo-code format is intended, in which case I just got confused? or perhaps the typo is intentional and a later section will describe how model-checking interacts with things like unit tests or other ways to check for typos in the non-model real code? or perhaps I am doing the logic wrong myself?)

Navigation structure

index.rst:

Rethink when things have settled down: structure apparent to reader in sidebar is "Learn", "Examples" and "Reference", where "Core" and "Topics" are under "Learn" today.

You said: "That's intentional, though it may be a bad idea"

I reply: I really think it's a bad idea :-)

"hundreds in thousands"

In https://learntla.com/intro/faq.html#does-tla-actually-find-bugs it should be "hundreds of thousands".

Graphviz renderings are broken

B/c no graphviz on the build machines

Stylistic choice: core/Core/The Core

intro/conceptual-overview.rst:

There's a few concepts I haven't introduced here: temporal properties, fairness, stutter-invariance, etc. All of these will be covered later. Hopefully, though, this is enough to give you a sense of what, if you decide to learn TLA+, you'll actually be able to do with it. If you're interested in continuing, check out the :doc:core </core/index> and setup.

core or Core or The Core (as in intro.rst)?

On the size of `SUBSET ClockType`

The "Operators and Values" page says:

As a quick sanity check, run Cardinality(ClockType) [...]. You should see it has 86400 elements. [...]

Finally, we can get all subsets of a set with SUBSET S. SUBSET ClockType will be all the sets containing a bunch of clock values… all 7,464,960,000 of them.

The 7-billion-ish figure is 86400^2, but shouldn't the actual
cardinality of SUBSET S be the vastly larger 2^86400?

For example, if I ask my scratchfile to evaluate the size of SUBSET S
when S has 6 elements, it properly reports 64 (= 2^6):

SixType == (0..1) \X (0..2)

>>> <<Cardinality(SixType), Cardinality(SUBSET SixType)>>
<<6, 64>>

I also can't quite reproduce the behavior of the #million footnote
with a fresh install of TLAToolbox-1.8.0 on Linux. Specifically,
Cardinality(SUBSET (1..30)) happily evaluates to 1073741824, while
attempting to compute Cardinality(SUBSET (1..31)) fails with "Overflow
when computing the number of elements". Maybe this is out of date?

(would generally send a PR here but I'm brand new to TLA+ so rather
unconfident with which changes to suggest; thanks for all your work!)

Improvements to Operators and Value chapter

Greetings,

I've identified a couple of minor points that can be improved in the aforementioned chapter.

The first is the following paragraph:

There is one more boolean operator of note: =>, or “implication”. A => B means “A is at least as true as B”. A => B = FALSE when false if A is true and B is false, otherwise it’s true. B is true or A is false (or both). You don’t see this very often in programming, as it’s pretty useless for control flow. But it’s extremely important for any kind of specification work. We’ll go into more detail about it later.2

As feedback, I feel that it can be improved in the following manner(s):

• The syntax of equality checks (single =) vs assignment == is not very clearly introduced prior to this point and so at first glance it is not clear that the expression A=>B=FALSE means the expression ... equals FALSE. It might be useful to add a short sentence in parenthesis afterwards which clearly articulates that the whole expression evaluates to FALSE
• after the expression the sentences just barely add up. A=>B = FALSE _when false if_.... I'm not 100% sure if it's just me but it is quite difficult to read. Since this operator is very important I would suggest to improve the wording somehow. Adding a truth table would be a plus. Even after going through this phrasing multiple times over and over it is very unclear how this behave. Another suggestion would be to describe it in logic gates terms (is it a XNOR?)

In the section of contrapositives exercise:

• It is not clear what does "regular three" refers to (perhaps explicitly naming the operators or at least namedropping the term "regular three" in the boolean operators section just above).
• The question For what values of A and B is ~B => ~A true? is phrased a bit misleadingly - as a reader I infer I need to find the values for which the expression yields a TRUE i.e. find the actual values of A and B in this case. It is not clear that a new implication need be written

In the summary section, adding the implication with a very short explainer would be helpful.

Wording on "everything after"

core/indes.rst:

Everything up to and including "temporal properties" is necessary to fully use TLA+. Everything after that adds further power.

I get your point, really, but it sounds awkward when “everything else” is one single bullet point that is basically “whatever”.

fix typo: remove "far" from "That's why concurrency errors are so far hard to find."

couldn't figure out how to do a proper pull request, but you can see what I mean by looking here:
https://github.com/simondorfman/learntla-v2/pull/1/files

Mention operator re-definitions

Section https://learntla.com/topics/optimization.html#construct-don-t-filter might demonstrate how you can redefine operators. This way, users can keep a simple, more axiomatic definition in the main spec, while using a complex yet more efficient definition during model checking. A Java module override is kind of the most extreme variant of this technique.

"DSL" in the FAQ

Of course there's some level of assumed knowledge in everything, and if you're good with "I assume readers know what a DSL is", please feel free to close the issue. Otherwise, I'm thinking a tooltip or other lightweight thing to show "DSL = Domain Specific Language" might be handy?

Bug in the LET sample sepc

In LET, it said:

ToClock2(seconds) ==
  LET
    h == seconds \div 3600
    h_left == seconds % 3600
    m == h_left \div 60
    m_left == h_left % 60
    s == m_left \div 60
  IN
    <<h, m, s>>

It should be s == m_left instead of s == m_left \div 60

text seems to silently swap between examples

On Writing an Invariant seems to switch silently between examples. It start by using "another spec for finding duplicates that also runs without error", the one where is_unique is set to TRUE. But in the later section Testing Duplicates it seems to be taking the example on the page Writing Specifications in which is_unique gets updated. The first five or seven times I read the page Writing an Invariant I was so confused that I came close to giving up on the whole endeavour, feeling that if I'm not smart enough to understand how the text could possibly apply to the example given on that page I've basically got no chance of ever using this tool.