TLA+ Action Properties
hillelwayne.com
TLA+ Action Properties
1–10 of 38 posts
Re: TLA+ Action Properties
#2 [][x' > x]_x
Re: TLA+ Action Properties
#3[][x' > x]_x TLA+ seems like an incredibly useful tool, but damn it could do with a better syntax. Math notation is designed to be written on paper and to handle extreme repetitiveness when you do proofs or calculations. Both of those premises are largely irrelevant in the domain TLA+ is intended for.
That's what PlusCal seems to be there to help with. It will generate statements like the above from a more Pascal-ish form.
Re: TLA+ Action Properties
#4I wanna die... WTH this undigest stuff :Ð unmaintanable, awfully
Re: TLA+ Action Properties
#5[][x' > x]_x TLA+ seems like an incredibly useful tool, but damn it could do with a better syntax. Math notation is designed to be written on paper and to handle extreme repetitiveness when you do proofs or calculations. Both of those premises are largely irrelevant in the domain TLA+ is intended for.
most of the time I need to read it, I use the PDF generation. It turns all the ascii into math symbols. way easier to read
Re: TLA+ Action Properties
#6[][x' > x]_x TLA+ seems like an incredibly useful tool, but damn it could do with a better syntax. Math notation is designed to be written on paper and to handle extreme repetitiveness when you do proofs or calculations. Both of those premises are largely irrelevant in the domain TLA+ is intended for.
First, what you posted (and the article uses), is not really TLA+ syntax, but its ASCII source; it's like publishing the LaTeX source for your typeset maths. TLA+ syntax looks like what you see here: https://pron.github.io/posts/tlaplus_part2 Some TLA+ bloggers publish the typesetting source rather than actual pretty-printed TLA+; I'm not thrilled with that, but there's a good, mundane, reason for doing it: there is no convenient formatter for HTML yet, only PDF.
Second, TLA+ is very much designed for writing mathematical specifications that are much smaller than most programs (a TLA+ specification with ~2000 lines of maths is very big, while a program with 2000 lines of code is quite small), that are then read and contemplated a lot. Several hours of thought for every line of maths is pretty normal for TLA+. Writing maths [1] is absolutely not like programming, both for ergonomic and workflow reasons (https://old.reddit.com/r/tlaplus/comments/edqf6j/an_interest...) as well as semantic reasons (https://old.reddit.com/r/tlaplus/comments/enencr/yet_another...). Easily the hardest thing in learning TLA+ (which is a tiny, and extremely simple formal maths language) is understanding the difference between programming and simple mathematics, and it takes work to internalise that. The syntax, which is pretty much standard mathematical notation, more or less, helps.
[1]: TLA+ is roughly the discrete analogue to ODEs describing a continuous engineered system.
Re: TLA+ Action Properties
#7A very useful article for the non-noob learner of TLA+!
> This is the launching point into refinement, or using an entire specification as the checked property of another spec.
We use the term "refinement" for those more special cases where `A` and `B` are both canonical formulas (`Init ∧ □[Next]_vars ∧ Fairness`), or, at least, both contain an initial state predicate and at least one box-action clause, but when learning, it's important to understand that there is nothing special about refinement in TLA+ from a mathematical point-of-view. Every formula in TLA+ describes a class of behaviours. The key general point to learn is that TLA+ does not distinguish between specifications and properties; they're just classes of behaviours that we can call a "system property" or a "system specification" based on how we psychologically think of it. The TLA+ formula `A ⇒ B` means that `A`'s behaviours are contained in `B`'s, and can be read as "specification A implements specification B" or "specification A satisfies property B" or "property B is an abstraction of property A" or "specification B is a generalisation of property A." All of these are just words used to describe the abstraction/refinement relation that's the very core of TLA+. So this is refinement, and `□[A]_vars` is an entire TLA+ specification, as is `□P` (it is true that TLC cannot check the specification `□(x ∈ 1..3)` but it can check the equivalent formula `x ∈ 1..3 ∧ □[x' ∈ 1..3]_x` but that doesn't make the simpler formulation any less of a valid and complete TLA+ specification of a system).
Re: TLA+ Action Properties
#8[][x' > x]_x TLA+ seems like an incredibly useful tool, but damn it could do with a better syntax. Math notation is designed to be written on paper and to handle extreme repetitiveness when you do proofs or calculations. Both of those premises are largely irrelevant in the domain TLA+ is intended for.
First, what you posted (and the article uses), is not really TLA+ syntax, but its ASCII source; it's like publishing the LaTeX source for your typeset maths. TLA+ syntax looks like what you see here: https://pron.github.io/posts/tlaplus_part2 Some TLA+ bloggers publish the typesetting source rather than actual pretty-printed TLA+; I'm not thrilled with that, but there's a good, mundane, reason for doing it: there is…
Would it make sense for the TLA+ source to just be a subset of LaTeX, then? At least some fraction of the potential userbase is already familiar with that.
Re: TLA+ Action Properties
#9Earlier quoted context omitted.
First, what you posted (and the article uses), is not really TLA+ syntax, but its ASCII source; it's like publishing the LaTeX source for your typeset maths. TLA+ syntax looks like what you see here: https://pron.github.io/posts/tlaplus_part2 Some TLA+ bloggers publish the typesetting source rather than actual pretty-printed TLA+; I'm not thrilled with that, but there's a good, mundane, reason for doing it: there is…
Would it make sense for the TLA+ source to just be a subset of LaTeX, then? At least some fraction of the potential userbase is already familiar with that.
It largely already is. E.g. you can write \forall rather than \A, \lor instead of \/, \neg instead of ~, etc.. The representation most people choose to write as their ASCII typesetting source is just more ergonomic, as it's specifically tailored for TLA+; conversely, there is a LaTeX mode that renders TLA+.
Anyway, it's not what you're supposed to read. The vast majority of TLA+ is readable to someone familiar with ordinary mathematical notation within two to ten minutes of training (if you know temporal logic, then almost all of TLA+ is readable within minutes). See e.g. this complete (and very sophisticated in its use of advanced TLA+) specification, written at Arm, of CPU speculation side-channels: http://www.procode.org/cachespec/ (direct link to spec: http://www.procode.org/cachespec/CacheSpecv1.pdf). The syntax is quite beautiful, and almost immediately familiar to anyone who knows standard mathematical notation.
Re: TLA+ Action Properties
#10[][x' > x]_x TLA+ seems like an incredibly useful tool, but damn it could do with a better syntax. Math notation is designed to be written on paper and to handle extreme repetitiveness when you do proofs or calculations. Both of those premises are largely irrelevant in the domain TLA+ is intended for.
We're seeing more people create DSLs that compile to TLA+. For example, salt lets you write TLA+ specs in Clojure: https://github.com/Viasat/salt