TLA from First Principles
5 comments
·October 23, 2024larsrc
bubblyworld
Temporal Logic of Actions, to fix the irony here.
mrkeen
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
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
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!