TLA from First Principles

Temporal Logic of Actions, to fix the irony here.

DIYOAJFTSOI, dude! (Don't invent your own acronyms just for the sake of it)

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.

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?

You can use pluscal, it embeds in tla+ and compiles to it, it's fairly nice.

In addition to PlusCal, I think the main "pseudocode alternative" to TLA+ is now Quint: https://github.com/informalsystems/quint

No, it doesn’t matter. All paths are explored

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?