When instantiating a module, care must be taken with handling operators that implicitly bind state variables, notably ENABLED and fairness conditions. In particular, it is not generally the case that I!(WFvars(A)) is the same as WF(I!vars)(I!A) where I denotes the instance of a module. Note that the notation I!(WF_vars(A)) is not actually legal TLA+ syntax, I am only using it here to denote the instantiated fairness condition.
The attached modules seem to indicate that TLAPS implicitly performs this substitution and therefore allows me to prove an absurdity. This is a soundness issue.
Z.tla.txtXY.tla.txt
When instantiating a module, care must be taken with handling operators that implicitly bind state variables, notably ENABLED and fairness conditions. In particular, it is not generally the case that I!(WFvars(A)) is the same as WF(I!vars)(I!A) where I denotes the instance of a module. Note that the notation I!(WF_vars(A)) is not actually legal TLA+ syntax, I am only using it here to denote the instantiated fairness condition.
The attached modules seem to indicate that TLAPS implicitly performs this substitution and therefore allows me to prove an absurdity. This is a soundness issue. Z.tla.txt XY.tla.txt