Question about the value of action expressions

[Timi]

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!

[Brandon Barker]

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.

[Haruki Okada]

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...@gmail.com>:

--
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...@googlegroups.com.
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...@gmail.com

========================

[Timi]

Right. Thank you both for your responses.

Just to be clear, say we have another spec like:

Init == x = 1
A == /\ x < 5
         /\ x' = x + 1

   

Next == A

This will also deadlock but before then, what I'm getting from your responses is it will find a next state that satisfies the Next formula (x in the current state is less than 5 and in the next state is x+1).

What I don't understand is if x is 1 and x' is not an assignment, how is there a next state where the value of x is 2? I don't suppose TLC generates all possible values of x in the next state and then picks the one that satisfies the condition.

Can you please help clarify that?

[Hillel Wayne]

There's two sides to this, what the logic is saying and what TLC does.

What the logic is saying is that for the next-state relations <4, 5>, <1,2>, and <2,3> the action A is true, while for the next-state relations <5,6>, <1, 3>, and <rutabaga, kumquat> the action is false. Since Next == A, only the first set of next state relations are part of the specification.

What TLC actually does is, the first time it encounters a primed value in each state, it uses it as a guide to generate the set of possible states. In all future cases, it treats it as a boolean. So take

A ==
  /\ x < 5

  /\ \/ x' = x + 1
     \/ x' = x - 1
  /\ x' > x

Let's say in this state x = 2. Then TLC will first encounter the disjunction and create the possible next state-relations <2, 3> and <2, 1>. Then it will use the x' > x to determine that for <2, 3>, A is true, while for <2, 1> A is false.

H

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/5602a426-d049-4069-9298-e00d257ee3f5n%40googlegroups.com.

[Timi]

Thank you, Hillel. This clarifies it for me.

Thank you all for the help!

Timi