[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[tlaplus] TLC bug or TLA+ subtlety?

Take the following spec:


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.


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.