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

*From*: Timi <oluwatimilehinadeniran@xxxxxxxxx>*Date*: Tue, 2 Aug 2022 14:15:00 -0700 (PDT)

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.

**Follow-Ups**:**Re: [tlaplus] Question about the value of action expressions***From:*Haruki Okada

**[tlaplus] Re: Question about the value of action expressions***From:*Brandon Barker

- Prev by Date:
**Re: [tlaplus] Modeling optional values - from a newbie** - Next by Date:
**[tlaplus] Re: Issue enumerating Nat, but I don't see where I'm enumerating the entire set Nat** - Previous by thread:
**[tlaplus] Re: Issue enumerating Nat, but I don't see where I'm enumerating the entire set Nat** - Next by thread:
**[tlaplus] Re: Question about the value of action expressions** - Index(es):