Hi, I was playing around with a simple TLA+ model and noticed the following:
---- MODULEm----
EXTENDS Integers, FiniteSets
VARIABLES t
_Init == t = 0
_Next == t'\in 1..10
====
TLC ran successfully. When I edited it like so:
---- MODULEm----
EXTENDS Integers, FiniteSets
VARIABLES t
_Init == t = 0
_Next == t' <= 10 /\ t' >= 0
====
It produced an error message:
"TLC threw an unexpected exception. This was probably caused by an error in the spec or model. See the User Output or TLC Console for clues to what happened. The exception was a java.lang.RuntimeException : In evaluation, the identifier t is either undefined or not an operator."
This happens on both the VSCode extension and the toolbox. Is there a set of rules about how expressions involving primed variables ought to be written? From what I understand, both specs mean the same thing.
--
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 visit https://groups.google.com/d/msgid/tlaplus/1b6b77fa-7e32-4370-80a3-ce750e8928d4n%40googlegroups.com.