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.
Pythonistas, feh!
As usual, a good blog post.
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?
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.
Can you explain how a time-step without a transaction is handled by the final TLA+ code?
My confusion stems from:
Next ==
AliceToBob
\/ BobToAlice
...so does it matter which "pathway is taken"? This reminds me of context free grammars / PEG grammars. 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?