[HN Gopher] TLA from First Principles
       ___________________________________________________________________
        
       TLA from First Principles
        
       Author : ingve
       Score  : 10 points
       Date   : 2024-10-23 10:03 UTC (12 hours 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.
        
       ___________________________________________________________________
       (page generated 2024-10-23 23:01 UTC)