hwayne / learntla-v2 Goto Github PK
View Code? Open in Web Editor NEWLearn TLA+ for free! No prior experience necessary!
Home Page: https://www.learntla.com
License: Other
Learn TLA+ for free! No prior experience necessary!
Home Page: https://www.learntla.com
License: Other
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.
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?)
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?)
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
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
Linux and macOS allocate memory lazily while Windows allocates memory eagerly: https://learntla.com/topics/optimization.html#use-refactor-properties
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?
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
So that older links to specific learntla pages on the old site don't all break
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:
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>
andsetup
.
core or Core or The Core (as in intro.rst)?
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.
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.
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]
?
TLA+ Toolbox seems clunky. All the cool kids are using VSCode! (And TLA+ is VSCode is nice and useable thanks to https://github.com/tlaplus/vscode-tlaplus.) The learntla text uses TLA+ Toolbox. But there's no direct 1-1 mapping of TLA+ Toolbox screens/fields/commands (and there are a lot of screens/fields/commands there!) to VSCode. As a specific example, it took me a bit of time to figure out where to put duplicates
's (just started on your learntla website --- thanks for this) invariants and properties in the duplicate.cfg
. Can the learntla text (examples, in particular) be ported to use VSCode instead?
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?
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
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.
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
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.
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?
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.
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?
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.
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
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?
B/c no graphviz on the build machines
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
"“Formal methods” is, very roughly, the field of computer scientist dedicated to writing correct programs." on https://learntla.com/intro/faq.html.
In https://learntla.com/intro/faq.html#does-tla-actually-find-bugs it should be "hundreds of thousands".
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.
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.
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.
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
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.
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.
the CHOOSE section states:
Here’s another thing we could do:
- Take the set of all possible clock values.
- 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).
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.
pc
probably stands for program counter.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.Tip
in the Structured Data chapter ("State sweeping is when...", then "... trick known as state sweeping").<>
is used in an example spec before it is defined.WF_v
and SF_v
, but the English explanation uses WF_x
and WF_vars
. This is kind of confusing. Does it matter?<=>
is used in "General Tips" and /=
in the Goroutines example without either being defined. (The /=
looks like it could be #
?)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 :-)
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!)
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."
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
docs/core/setup.rst
Adding "No Overdrafts" as an Invariant results in an error when trying to run the model.
***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.
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.
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
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”?
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):
=
) 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 FALSEA=>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:
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 writtenIn the summary section, adding the implication with a very short explainer would be helpful.
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”.
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.
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
The writing specifications page says this of the duplication checker:
Create an empty set
seen
, then step through the elements ofseq
.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.If we reach the end and haven't seen any duplicate elements, we say the list is unique.
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?
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.
A declarative, efficient, and flexible JavaScript library for building user interfaces.
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
An Open Source Machine Learning Framework for Everyone
The Web framework for perfectionists with deadlines.
A PHP framework for web artisans
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
Some thing interesting about web. New door for the world.
A server is a program made to process requests and deliver data to clients.
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
Some thing interesting about visualization, use data art
Some thing interesting about game, make everyone happy.
We are working to build community through open source technology. NB: members must have two-factor auth.
Open source projects and samples from Microsoft.
Google ❤️ Open Source for everyone.
Alibaba Open Source for everyone
Data-Driven Documents codes.
China tencent open source team.