[tlaplus] Re: Question about the value of action expressions

I'm also a newbie to TLA+, but my understanding is that it is better not to think in terms of assignment happening with '='; you are expressing the state of x at "time t" and at "time t+1" (written as x'). So if you have a pair of such consecutive states, where x is first 5 and then 7, then A is true. Anything else, and A is false.

On Tuesday, August 2, 2022 at 5:15:00 PM UTC-4 Timi wrote:
Hello all,

I would like to check my understanding of a simple TLA+ concept that I now find confusing.

Say we have the action:

A == /\ x  = 5
/\ x' = 7

I understand that the equals sign in TLA+ is not an assignment but an equality check, so it's clear to me why 'x = 5' returns a boolean.

What I'm less clear about is the second line. My understanding is that it assigns the value of x in the next state as 7, and the line evaluates to True if x has not already been assigned in the next state.  Is that right?

I'm confused because the equality check in this case is performing an assignment, while also seemingly evaluating to a boolean. I'm assuming it evaluates to a boolean value here because it's used with the AND operator.  Am I thinking about this in the wrong way?

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.