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.

Sign up for GitHub

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

Jump to bottom

[BUG] Bogus "Expected Spec to be in the canonical form Init /\ [][Next]_vars" #636

Closed
lemmy opened this issue Mar 10, 2021 · 3 comments
Closed

[BUG] Bogus "Expected Spec to be in the canonical form Init /\ [][Next]_vars" #636

lemmy opened this issue Mar 10, 2021 · 3 comments
Labels
bug product-owner-triage This should be triaged by the product owner usability UX improvements

Comments

@lemmy
Copy link
Contributor

lemmy commented Mar 10, 2021

Reported as not in canonical form:

VARIABLE x
Init == x = TRUE

Spec == Init /\ [][UNCHANGED x]_x

Works fine:

VARIABLE x
Init == x = TRUE
Next == UNCHANGED x
Spec == Init /\ [][Next]_x

With APALACHE version 0.11.1-SNAPSHOT build v0.11.0-17-gf55663c
@lemmy lemmy added the bug label Mar 10, 2021
@lemmy
Copy link
Contributor Author

lemmy commented Mar 10, 2021 

Spec == Init /\ [][TRUE]_x

also not accepted.

@konnov konnov self-assigned this Mar 12, 2021
@konnov konnov added this to the backlog2021 milestone Mar 12, 2021
@konnov konnov added the usability UX improvements label Mar 12, 2021
@konnov
Copy link
Collaborator

konnov commented Mar 12, 2021

Right. Now Apalache is expecting an operator name like Next. A similar issue has been raised by @Quantifier

lemmy added a commit to tlaplus/Examples that referenced this issue Mar 15, 2021
@lemmy
Refactor Einstein to work better with TLC and to be accepted
a9c08fd 
by Apalache (apalache-mc/apalache#636).
@konnov konnov modified the milestones: backlog2021, June iteration Jun 3, 2021
@konnov konnov added the product-owner-triage This should be triaged by the product owner label Jul 13, 2022
@konnov konnov removed their assignment Feb 22, 2023
@Kukovec
Copy link
Collaborator

Kukovec commented Mar 14, 2023

Closing this, as it is effectively a duplicate of #468

@Kukovec Kukovec closed this as not planned Won't fix, can't repro, duplicate, stale Mar 14, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
bug product-owner-triage This should be triaged by the product owner usability UX improvements
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
4 participants
@lemmy @konnov @shonfeder @Kukovec