Bogus error about ENABLED with 1.4.5 TLAPS.tla

[lemmy]

https://github.com/lemmy/BlockingQueue/ contains a copy of TLAPS.tla as released with 1.4.5. Re-proving the proofs in, e.g., BlockingQueue.tla with what will become TLAPS 1.4.6, produces a bogus error.

This probably doesn't need changing in TLAPS, but perhaps a mention in the 1.4.6 release notes.

[johnyf]

The module TLAPS has changed, and I think that the lines that cause this message are after the closing module line. This change to the module TLAPS preceded the support for ENABLED, for example:

tlapm/library/TLAPS.tla

Lines 317 to 318 in f54897a

	=============================================================================

[johnyf]

The reported message arises when running a version of tlapm that supports reasoning about ENABLED, in a TLA+ module that instantiates a version (or suitable excerpt) of the TLA+ module TLAPS from earlier than the initial commit (c9f82ae) to this repository (support for ENABLED was introduced later than the initial commit).

This earlier change in the module TLAPS commented certain theorems that contained ENABLED and operator declarations (with the intention of using BY PTL instead). When these theorems in the module TLAPS are not commented, and support for ENABLED is present, then when tlapm attempts to instantiate the module TLAPS, tlapm encounters the theorems that contain ENABLED applied to operators that are declared with the keyword ACTION. tlapm then raises a warning that it cannot instantiate such theorems. (tlapm will raise this warning even when no proof directive related to ENABLED is used in user modules, because the INSTANCE statement will lead tlapm to attempt instantiating all the theorems in the module that is being instantiated.)

The warning is raised to inform that certain theorems from the module being instantiated will be absent in the instantiated module, and so proofs that invoke them will not work. This warning is not raised when instantiating versions of the module TLAPS in this repository. When this warning is raised due to instantiating modules other than TLAPS, then one possibility would be to change the modules to not instantiate theorems that contain ENABLED applied to ACTION operators (reasoning about instantiations of such theorems is currently unsupported by tlapm).

As suggested above (#15 (comment)), in the release notes of TLAPS in the website, in commit 66befe1 I added a note about this combination of tlapm with a version of the TLA+ module TLAPS.tla from an older release of TLAPS. Commit 66befe1 adds a test for the instantiation of the module TLAPS, including comments that document this combination of tlapm and TLAPS.tla versions.

Writing this test revealed a bug unrelated to this issue. That bug has been fixed in commit d7f57d0.