The eqc_statem model is not able to model background side-effects.
As a result, assuming that commands are atomic, even though they are not, will make tests sporadically fail.
By adding a precondition for not using dead processes to lock resources or get tokens, this failure is made less frequent.
The eqc_statem model is not able to model background side-effects. As a result, assuming that commands are atomic, even though they are not, will make tests sporadically fail.
By adding a precondition for not using dead processes to lock resources or get tokens, this failure is made less frequent.