[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[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?


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.