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

On Tuesday, 2 August 2022 at 23:20:33 UTC+1 ocad...@xxxxxxxxx wrote:

Hi.

> it assigns the value of x in the next state as 7

Even for primed variables, it's just a formula (predicate). Not an assignment.
You can read x'= 7 as "It evaluates to true when the value of x in the next state is 7".

So Action A is just a formula that evaluates to true when x in current state is 5 and x's next state value is 7.
In short, actions are formulas over the state transitions (pair of current state and next state).

Maybe thinking like below might help to understand the TLA+ concept.

- TLA+ spec never defines the instructions of the system like ordinary programming languages. Rather, it defines the possible state transitions of the system.
- TLC explores the states that satisfy the spec.

Let's say we have the following spec:

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

When we run TLC, it works like:
- Find initial state (i.e. the assignment of the variables) that satisfy Init formula (x = 5)
- Starting from initial state, find next state that satisfy Next formula (current value of x is 5, so if next value of x is 7, it satisfies A)
- Update the current state and try to find next state, but there's no variable assignment that satisfies Next so it terminates with reporting Deadlock.

2022年8月3日(水) 6:15 Timi <oluwatimile...@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+u...@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/fbda7721-e8c9-4e09-9239-4a8c4a162496n%40googlegroups.com.

--
========================
Okada Haruki
ocad...@xxxxxxxxx
========================