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

Short-circuit evaluation in conjunctions #44

Closed
ajdavis opened this issue May 19, 2024 · 6 comments · Fixed by #47
Closed

Short-circuit evaluation in conjunctions #44

ajdavis opened this issue May 19, 2024 · 6 comments · Fixed by #47

Comments

@ajdavis
Copy link
Contributor

ajdavis commented May 19, 2024

Repro for disjunct: type TRUE \/ <<"a">>[2] = "b" in the REPL.

Expected: result TRUE, the second half isn't evaluated.

Actual: no result, "swallowing parse errors during repl evaluation" is logged in the console. The REPL tried to interpret the second half and failed with an index error.

Repro for conjunct: type FALSE /\ <<>>[1] = "a" in the REPL.

Expected: result FALSE, the second half isn't evaluated.

Actual: no result, "swallowing parse errors during repl evaluation" is logged in the console. The REPL tried to interpret the second half and failed with an index error.
@ajdavis
Copy link
Contributor Author

ajdavis commented May 19, 2024

I have a PR in progress.

@ajdavis
Copy link
Contributor Author

ajdavis commented May 20, 2024

To test evalDisjList, try this spec:

------------------------------- MODULE DisjunctList ----------------------------- 
EXTENDS TLC, Naturals

VARIABLES x

Action ==
  \/ 1 = 1 /\ x' = 1
  \/ <<>>[-1]

Next == Action
Init == x = 176
=============================================================================

After clicking on the initial state in the "Actions" tab, tla-web displays "Assertion failed". The console shows:

app.js:757 Error computing next states. Error: Assertion failed
    at assert (eval.js:47:15)
    at processDisjunctiveContexts (eval.js:1904:9)
    at evalDisjList (eval.js:2518:12)
    at evalExpr (eval.js:3542:16)
    at evalExpr (eval.js:4043:16)
    at evalIdentifierRef (eval.js:2602:16)
    at evalExpr (eval.js:3576:16)
    at evalExpr (eval.js:4043:16)
    at getNextStates (eval.js:3853:15)
    at TlaInterpreter.computeNextStates (eval.js:3929:23)

ajdavis added a commit to ajdavis/tla-web that referenced this issue May 20, 2024
@ajdavis
Short-circuit and/or eval
714af39 
Fixes will62794#44
@ajdavis ajdavis mentioned this issue May 20, 2024
Merged
@lemmy
Copy link
Contributor

lemmy commented May 20, 2024

@ajdavis How does this handle x' = x + 1 \/ x' = x+ 2?

@ajdavis
Copy link
Contributor Author

ajdavis commented May 20, 2024

Thanks very much @lemmy, I misunderstood how TLA+ works! I see now that your expression permits behaviors where x is incremented by one or two, so both sides must be evaluated. No short-circuiting of disjunctions.

ajdavis added a commit to ajdavis/tla-web that referenced this issue May 20, 2024
@ajdavis
Short-circuit conjunction evaluation
dd33716 
Fixes will62794#44
@ajdavis ajdavis changed the title Short-circuit evaluation in disjunct and conjunct expressions Short-circuit evaluation in conjunctions May 20, 2024
@will62794
Copy link
Owner

Yeah, short-circuiting becomes a bit more subtle when doing initial/next state generation. Short-circuiting conjunctions should be safe, though. Note that we already try to do it for conjunction lists.

Note also that test suites are currently run here. I will soon add documentation on how to add/run new tests.

@lemmy
Copy link
Contributor

lemmy commented Jun 12, 2024 •
edited

Also, FALSE implies anything.

-> % tlcrepl
Welcome to the TLA+ REPL!
TLC2 Version 2.18 of Day Month 20??
Enter a constant-level TLA+ expression.
(tla+) FALSE => 42 = "abc"
TRUE

will62794 pushed a commit that referenced this issue Jun 12, 2024
@ajdavis @will62794
Short-circuit conjunction evaluation
5933fa6 
Fixes #44
@will62794 will62794 mentioned this issue Jun 13, 2024
Open
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

Short-circuit and/or eval ajdavis/tla-web
3 participants
@ajdavis @lemmy @will62794