[tlaplus] Doing arithmetic with current state value and next state value of a variable in TLA+

[Jefferson Andrade <joandrade@xxxxxxxxx>]

Hello,

I want to write a (piece of a) formula like this:

y' = x' - x

But every time I try to run the model I get the error, «In evaluation, the identifier x is either undefined or not an operator.»

What is going on? Is it really not possible to write such formulas? why? How can I work around this?

Thanks.

-- 
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/b36a24e7-f78c-4983-a776-16d56a09fd64n%40googlegroups.com.