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.
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.
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?
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.
24 comments
[ 2.2 ms ] story [ 61.7 ms ] threadI 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?
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?
A use-case for the <> "eventually" operator.
Pythonistas, feh!
Such as the TLA (three letter acronym) used here.
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.
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.> 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?
As usual, a good blog post.