[tlaplus] TLC bug or TLA+ subtlety?

[Hillel Wayne <hwayne@xxxxxxxxx>]

Take the following spec:

VARIABLES x, y

vars == <<x, y>>

Init ==
  /\ x = FALSE
  /\ y = FALSE

Next ==
  /\ x' \in BOOLEAN
  /\ y' = (x \/ x')

Spec == /\ Init /\ [][Next]_vars

This checks with 7 states generated. Now remove the parenthesis in Next, 
giving

Next ==
  /\ x' \in BOOLEAN
  /\ y' = x \/ x'

This now fails, with a not fully specified successor state:

State 2: <Next line 11, col 3 to line 12, col 17 of module problem>
/\ x = TRUE
/\ y = null

This seems to me like a bug with TLC, but I wanted to check if the two 
Nexts aren't actually different semantically, and if so, what makes them 
different.

H

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/b2139e63-9e12-f82c-4935-2077a148f7ef%40gmail.com.