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 does not parse quantifiers using \forall or \exists keywords instead of \A or \E #160

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

Thanks to @muenchnerkindl for remembering this; opening an issue for tracking. This will fail at the syntax parse level:

---- MODULE Test ----
op == \forall x, y \in Nat, z \in Int, a, b, c \in Real : FALSE
op == \exists x, y \in Nat, a, b \in Int : TRUE
====

While this will succeed:

---- MODULE Test ----
op == \A x, y \in Nat, z \in Int, a, b, c \in Real : FALSE
op == \E x, y \in Nat, a, b \in Int : TRUE
====

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