A.3.3.TR:8 - Common Anti-Patterns and How to Avoid Them

Failure	Why it changes the result	Repair
Replace saved-value updates with updates of the current value	Interference between read and write disappears from the model.	Retain the saved value and instruction position, or justify an atomic operation.
Conjoin alternative actions	The model demands incompatible changes at once and can lose legitimate executions.	State the alternatives and the condition enabling each one.
Leave a local action’s other state values free	A model can introduce changes no participant performs.	State the unchanged values or the joint action that changes them.
Filter away violations of the property being investigated	The model excludes the failure instead of explaining whether the implementation prevents it.	Model the behavior or derive the prevention rule, then test the property.
Infer progress from preservation	An invariant can hold in a cycle with no useful completion.	Supply a decreasing measure, scheduling condition or other relevant progress argument.
Repair a missing interaction law by changing a numerical setting	The computation still lacks the relation needed to determine the modeled change.	Repair the subject account and then select a computation for it.