Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

TLAPM parser does not accept MODULE references in several places #166

Open
ahelwer opened this issue Oct 24, 2024 · 1 comment
Open

TLAPM parser does not accept MODULE references in several places #166

ahelwer opened this issue Oct 24, 2024 · 1 comment
Labels
bug An error, usually in the code. syntax parser Issues relating to TLAPM's syntax parser

Comments

@ahelwer
Copy link
Collaborator

ahelwer commented Oct 24, 2024

Quoting from TLA Version 2: A Preliminary Guide [pdf], page 20:

The parser also allows the following two kinds of “facts” in a use or hide statement. However, they are not supported by TLAPS and are likely to be removed from the language:

  • MODULE Name, indicating that all known facts obtained from the module Name are to be added or removed from the set of usable facts. The module name must appear in an extends or instance statement or else be the name of the current module.

And indeed TLAPM does not accept this syntax (although SANY does):

---- MODULE Test ----
USE x, MODULE M, 1 + 3
HIDE DEFS MODULE M, -., *, ^+
USE x, MODULE M DEF MODULE M, x
====

Though this is not discussed explicitly in the TLA+ V2 document, these "module references" are accepted in another place by SANY and the extant formal TLA+ grammar, which makes sense because they share parsing logic with use-or-hide: PROOF BY statements:

---- MODULE Test ----
LEMMA TRUE
PROOF BY ONLY
  MODULE Naturals,
  MODULE Integers
  DEFS
    MODULE Reals,
    MODULE Sequences
====

So the thing to do here is decide at the standard level whether these statements should actually be allowed in the language.

Ref #159

@ahelwer ahelwer added bug An error, usually in the code. syntax parser Issues relating to TLAPM's syntax parser labels Oct 24, 2024
@muenchnerkindl
Copy link
Contributor

Thanks for reporting this. IMHO, it would indeed be better to remove this syntax from the language, as well as the similar "BY MODULE" construct. These constructs look like a maintainer's headache because changes to a module could cause proof failures elsewhere that are hard to understand. Mild reformulations of facts and even additions of new theorems can confuse the provers to the point that existing proofs may fail. Instead, appealing to specific facts from a module indicates what is needed for a proof step to go through. Expanding all definitions contained in a module breaks the abstraction barrier: usually, one uses definitions to prove facts about operators and then uses those theorems, forgetting the actual definition.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
bug An error, usually in the code. syntax parser Issues relating to TLAPM's syntax parser
Development

No branches or pull requests

2 participants