Short-circuit evaluation in conjunctions

[ajdavis]

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]

I have a PR in progress.

[ajdavis]

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)

[lemmy]

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

[ajdavis]

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.

[will62794]

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]

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