[HN Gopher] TLA from First Principles
___________________________________________________________________
TLA from First Principles
Author : ingve
Score : 87 points
Date : 2024-10-23 10:03 UTC (2 days ago)
(HTM) web link (buttondown.com)
(TXT) w3m dump (buttondown.com)
| mrkeen wrote:
| 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?
| hwayne wrote:
| 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.
| hansvm wrote:
| 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.
| thaumasiotes wrote:
| > 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?
| mrkeen wrote:
| > What am I missing?
|
| A use-case for the <> "eventually" operator.
| larsrc wrote:
| 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!
| bubblyworld wrote:
| Temporal Logic of Actions, to fix the irony here.
| daelon wrote:
| Thank you.
| deskr wrote:
| DIYOAJFTSOI, dude! (Don't invent your own acronyms just for the
| sake of it)
| drewcoo wrote:
| TIMTOWTDI!
|
| Pythonistas, feh!
| beardbound wrote:
| 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.
| Jtsummers wrote:
| > 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.
| wslh wrote:
| 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.
| djoldman wrote:
| @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: Next == AliceToBob
| \/ BobToAlice
|
| ...so does it matter which "pathway is taken"? This reminds me of
| context free grammars / PEG grammars.
| sriram_malhar wrote:
| No, it doesn't matter. All paths are explored
| itishappy wrote:
| 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?
| Tomte wrote:
| The TLA+ book, freely available online:
| https://lamport.azurewebsites.net/tla/book.html
| tombert wrote:
| 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.
| justanotheratom wrote:
| TLA - now this is something I could use a coding copilot for..
| skybrian wrote:
| 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.
| kadoban wrote:
| You can use pluscal, it embeds in tla+ and compiles to it, it's
| fairly nice.
| hwayne wrote:
| In addition to PlusCal, I think the main "pseudocode
| alternative" to TLA+ is now Quint:
| https://github.com/informalsystems/quint
___________________________________________________________________
(page generated 2024-10-25 23:01 UTC)