[tlaplus] Priming TLA+ formulas

[n s <nedsri1988@xxxxxxxxx>]

Hello again, in the example below I want to use Foo' to mean 

a'=1 /\ b'=2. The compiler accepts this but TLC complains. Why is that?

VARIABLE a,b
Foo == a=1 /\ b=2
Init == Foo
Next == Foo /\ Foo'

Spec == Init /\ [][Next]_<<a,b>>

TLC complains 

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 a is either undefined or not an operator.
line 6, col 8 to line 6, col 8 of module test

-- 
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/3f57bc3e-3211-40cc-b153-2b61d53b092cn%40googlegroups.com.