[tlaplus] Question about the value of action expressions

[Timi <oluwatimilehinadeniran@xxxxxxxxx>]

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/fbda7721-e8c9-4e09-9239-4a8c4a162496n%40googlegroups.com.