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

[Brandon Barker <brandon.barker@xxxxxxxxx>]

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.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/76db6cf3-d003-42e7-adce-4a13c05ec631n%40googlegroups.com.