TLA Will always mean Three Letter Acronym in my book. It took many link hops to find an actual definition, I finally found it in Leslie's first paper on the subject. PEYA, people! Please Explain Your Acronyms!
I've seen this more and more in recent memory. I feel like the standard used to be define an acronym the first time you use it, then you can use it without explanation.
> I stumbled on a great way to explain the temporal logic of actions that TLA+ is based on. [emphasis added]
I mean, it's spelled out right there in the post so what's the complaint? And I double checked, that's copied from the email on Tuesday so not a later addition. He does seem to have changed it on the page for people who don't want to read so now the T, L, and A in the words are capitalized and bolded.
These articles are fantastic for people like me who want a quick, hands-on taste of TLA/TLA+ (or similar languages/technologies) and then move on—while letting the neurons hold onto the lesson to revisit later, even as it continues to sink in slowly.
Can anyone provide an intuitive use-case for including stuttering in a model?
I get that you can't model what 'eventually' happens: will a purchase flow end in a good state? NOT IF THE USER WAITS FOR AN INFINITE AMOUNT OF TIME BEFORE CLICKING THE 'BUY' BUTTON!
So the first thing I always have to do is turn off that nonsense so I can get back to modelling the purchase flow.
The main reason for stuttering is it makes composing specs a lot easier. Say you have two specs, one which is [](x' = x + 1) and one which is [](y' = y + 1). If you put the two together, you get [](x' = x + 1) && [](y' = y + 1), meaning both are always synchronized. If both also have stutter steps, though, you also get interleaving, where on a step only of the two increments.
Fair locking is a classic example. Stuttering can happen at a hardware level, and you need to create a composite data structure / algorithm which is correct regardless.
This is a great introduction. I liked the pseudocode better than TLA syntax, though, so I think if I needed something like this, I would look into alternatives to TLA itself.
Same question. Is stuttering now handled by the next line somehow?
Spec == Init /\ [][Next]_vars
Edit: Answered in the paragraph below the TLA+ code:
> The only thing that's "unusual" (besides == for definition) is the [][Next]_vars bit. That's TLA+ notation for [](Next || Stutter): Next or Stutter always happens.
I guess the `_vars` notation is shorthand for stutter. Anyone know where I can learn more?
TLA Will always mean Three Letter Acronym in my book. It took many link hops to find an actual definition, I finally found it in Leslie's first paper on the subject. PEYA, people! Please Explain Your Acronyms!
Temporal Logic of Actions, to fix the irony here.
Thank you.
I've seen this more and more in recent memory. I feel like the standard used to be define an acronym the first time you use it, then you can use it without explanation.
Such as the TLA (three letter acronym) used here.
> I stumbled on a great way to explain the temporal logic of actions that TLA+ is based on. [emphasis added]
I mean, it's spelled out right there in the post so what's the complaint? And I double checked, that's copied from the email on Tuesday so not a later addition. He does seem to have changed it on the page for people who don't want to read so now the T, L, and A in the words are capitalized and bolded.
Wow, I totally missed that. Sorry.
DIYOAJFTSOI, dude! (Don't invent your own acronyms just for the sake of it)
TIMTOWTDI!
Pythonistas, feh!
These articles are fantastic for people like me who want a quick, hands-on taste of TLA/TLA+ (or similar languages/technologies) and then move on—while letting the neurons hold onto the lesson to revisit later, even as it continues to sink in slowly.
I gotta say that I am jealous of how prolific Hillel is; I have no idea how he manages to find the time and not burn out.
As usual, a good blog post.
Can anyone provide an intuitive use-case for including stuttering in a model?
I get that you can't model what 'eventually' happens: will a purchase flow end in a good state? NOT IF THE USER WAITS FOR AN INFINITE AMOUNT OF TIME BEFORE CLICKING THE 'BUY' BUTTON!
So the first thing I always have to do is turn off that nonsense so I can get back to modelling the purchase flow.
Any counter examples?
The main reason for stuttering is it makes composing specs a lot easier. Say you have two specs, one which is [](x' = x + 1) and one which is [](y' = y + 1). If you put the two together, you get [](x' = x + 1) && [](y' = y + 1), meaning both are always synchronized. If both also have stutter steps, though, you also get interleaving, where on a step only of the two increments.
Fair locking is a classic example. Stuttering can happen at a hardware level, and you need to create a composite data structure / algorithm which is correct regardless.
> will a purchase flow end in a good state? NOT IF THE USER WAITS FOR AN INFINITE AMOUNT OF TIME BEFORE CLICKING THE 'BUY' BUTTON!
You seem to be presenting this as a ridiculous thing to consider, but it's very common behavior.
Visit the site, add something to your cart, close the tab, never come back.
What am I missing?
> What am I missing?
A use-case for the <> "eventually" operator.
This is a great introduction. I liked the pseudocode better than TLA syntax, though, so I think if I needed something like this, I would look into alternatives to TLA itself.
In addition to PlusCal, I think the main "pseudocode alternative" to TLA+ is now Quint: https://github.com/informalsystems/quint
You can use pluscal, it embeds in tla+ and compiles to it, it's fairly nice.
@hwayne, thanks for the explanation.
Can you explain how a time-step without a transaction is handled by the final TLA+ code?
My confusion stems from:
...so does it matter which "pathway is taken"? This reminds me of context free grammars / PEG grammars.Same question. Is stuttering now handled by the next line somehow?
Edit: Answered in the paragraph below the TLA+ code:> The only thing that's "unusual" (besides == for definition) is the [][Next]_vars bit. That's TLA+ notation for [](Next || Stutter): Next or Stutter always happens.
I guess the `_vars` notation is shorthand for stutter. Anyone know where I can learn more?
The TLA+ book, freely available online: https://lamport.azurewebsites.net/tla/book.html
No, it doesn’t matter. All paths are explored
TLA - now this is something I could use a coding copilot for..