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

*From*: Timi <oluwatimilehinadeniran@xxxxxxxxx>*Date*: Tue, 2 Aug 2022 15:57:25 -0700 (PDT)*References*: <fbda7721-e8c9-4e09-9239-4a8c4a162496n@googlegroups.com> <CAHf4GKq-b=viPzA5Ckgnp-rzEO=+knXjSyQF+NEJ5r4q4CHB8g@mail.gmail.com>

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?

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 7Even 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 = 5A == /\ x = 5

/\ x' = 7Next == AWhen 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.

--

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/5602a426-d049-4069-9298-e00d257ee3f5n%40googlegroups.com.

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

**References**:**[tlaplus] Question about the value of action expressions***From:*Timi

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

- Prev by Date:
**Re: [tlaplus] Question about the value of action expressions** - Next by Date:
**Re: [tlaplus] Question about the value of action expressions** - Previous by thread:
**Re: [tlaplus] Question about the value of action expressions** - Next by thread:
**Re: [tlaplus] Question about the value of action expressions** - Index(es):