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

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.