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 accepts incorrect use of labels that break operator precedence #169

Open
ahelwer opened this issue Oct 24, 2024 · 0 comments
Open
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

It is possible to use the label syntax to break operator precedence, and the parser should reject this:

---- MODULE Test ----
op == a * lab :: b + c
====

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

However, the expression is illegal if removing the label would change the way the expression is parsed. For example,
a + lab :: b * c
is legal because it is parsed as a + (lab :: (b * c)), which is how it would be
parsed if the label lab were not there. However,
a * lab :: b + c
is illegal because it would be parsed as a * (lab :: (b + c)) and removing the label causes the expression to be parsed as (a * b) + c.

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
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

1 participant