[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)*Ironport-data*: A9a23:4KtLsqnTXW+R0qG7y/iUgAzo5gwbI0RdPkR7XQ2eYbSJt1+Wr1Gzt xIYXmqObKqKa2PwLdggPtjg9RkFupaDx4QwTgdk+yljQ1tH+JHPbTi7BhepbnnKdqUvb2o+s p5AMoGYRCwQZiWBzvt4GuG59RGQ7YnRGvykTrSs1hlZHWeIcg944f5Ys7N/09UAbeSRWVvX4 4ui+5eHZDdJ5hYtWo4qw/LbwP9QlK+q0N8olgRWiSdj4TcyP1FMZH4uDfnZw0nQGuG4LcbmL wr394xVy0uCl/sb5nxJpZ6gGqECaua60QFjERO6UYD66vRJjnRaPqrWqJPwZG8P4whlkeydx /1Mv6C1UAcTZ5bPt/9DSAMEQiUlIaJ/reqvzXiX6aR/zmXDenrohuxyVQQ4ZNxCvOlwBm5K+ LoTLzVlghKr3brnhuLmDLAy3oJ6fZOD0IA34hmMyRnFCf8+RY3YAK/M7vVz5mwKqO10LN/8T eAnNwpSNjD5RjJ2F34lVbFlucaAiX74fDlVp0iSuLIspWPUyWSd1ZCxb4WFJIXbHK25mG7Gl nDPoWaiUig9PdalxDXawEm0tMDQyHaTtIU6TeXkrJaGmma7ym0IAwANTnOnpfD/j1WkHtNZM U0dvCsot6k7skKxJuQRRDW9qX+A+wcAAp9eSrxgrg6KzaXQ7kCSAW1soiN9hMIOtcUKQCUq7 AaynPzyWyd17OyREm6Sz+LBxd+tAhQ9IWgHbC4CaAIK5dj/vY0+5i4jqP4zQMZZafWlSVnNL yC2QDsW3OpM0JZav0mv1RWW3GL2/8mhohsdv12PBgqYAhVFiJlJjrFEBHDe5PdEaZ+FFxyP5 Sle3ceZ6+8KANeGkynlrAQx8FOBuKvt3N702wQH83wdG9KFpyHLkWd4vGEWGauRGpxYEQIFm WeK0e+r2LddPWGxcYh8aJ+rBsIhwMDITIq4B6yKM4IUP8gqK2drGR2Cg2bAjwgBd2B8wckC1 WuzLK5A8F5BVPo5kmPuLwvj+eZ7mXpgrY8seXwL503/jeD2iI+9RrACP1+DBt3VH4vVyDg5B +13Zpvi40wHDoXWO3CHmaZOcwxiBSVlVPje9p0PHsbec1YOMDxwW5f5n+l9E6Q7xP49vrmTr hmAtrpwlDITc1WaclvaAp2iAZu0NatCQYUTZ3F8ZQj3gSR5OO5CLs43LvMKQFXuz8Q7pdYcc hXPU5zo7i1nRmuV9jIDQ4P6qYA+Jh2niRjXYXiqZz8we5NvXQvU4sSidQzqrXFcAi2yvMo4g ruhygKKEcFYHl89UpnbOKC10le8nXkBg+YuDUHGFd9eJRf3+49wJi2t0/I6epleKRjKyjaA+ RyRBBMU+bvEr4MvoYvGgKmFq8GiFO4nRhhWGGzS7LCXMyjG/zr7kdUQDrrQJT2EDTH64qSvY +lR3srQCvxfkQYYqZd4HpZq0bk6uIniqrpc+QJuQyfGYlGtPbV/eyXU0MRKsJpN8b9Xow6BX EyCp4tBMrKTNcK5SVMcKVN+POSO3P0ZgAPf9fAkPEL+6HMl9baLSxwMbRaLjyNZIbRvN5492 qEqv8tPs16zjR8jM9CniCFI9jXcdSdZCPp56ZxKUpX2jgcLy01ZZcCOACHB5pzSOc5HNVMnI 2PJiafP2+Zcy07FfyZhHHTBx7AB15EHuRQP1UNbYlrQy4CDifgw0xlctz8wS10NnBlA1utyP EltNlF0dfrSpWY23JAbUjD+ARxFCT2Y5lf1lwkDmlrfQhT6TWfKNmA8ZbuA8RFL92NHYgVd5 6ySzGq5Az/mcNuvjnk3UE9ht/uxQtt2+QnPl9qgAtyeWpwzZzPqj+z1OjpZ90a5UZxo3ROEu O9x4exrYrf6PyM4rKo8BI2X2q4XVQifYmdFRKg5rq8OGGjdfhC02CSPehDqIZoWeKKV/B/qE dFqK+JOSw+6iHSEoAcdCPNeOLRzhvMouIcPd7+3d2cKv6HD/2hprI7I7Xq5w2AxRMh2ioAyL YTecz/EGWuVwnROnHLV69VAM3K8fMJDfxD2x+uv8e8EGp9f4vtgd1o+jum9s3mPalc1+huVu Ebae/aTwbUzk8JjmIzjFqgFDAKxcIuhWOON+QG1ktJPcdKfbpuU5l1N8gHqb1ZMIL8ce9Vrj rDR4tT560XI4eQtWGfDlpjdSqRE6K1ehgaM3h4b8ZWboceDZCMoyx4K+mT9MIAQ1d0Et5PhS Ay/Z8+9M9USXr+xAZGThzd2S34g52bfN88MZh9Ra9yDDR8S1QHINtS67WSvZmZeHsPNE4OrE Rf64p5C+fgBxLmhx3Y46zVODJh/L1vuVrEhasXq8zKfCwFER79EVqTKzXId1N0ANpVI/AsWL 34IqtgSuSleYJ318ew=*Ironport-hdrordr*: A9a23:R+n9YKwAXJzN0DpBtfN2KrPwp71zdoMgy1knxilNoH1uA7Clfq WV9pkmPHDP+VIssR0b6Le90ey7MAvhHXAc2/hmAV+NNDOWz1dAb7sSnrcL+lXbalnDH5dmpO 5dmstFeaDN5e0Qt7eL3ODHKadY/DDdytHYuQ629R4EJnAJV0gj1XYDNu/8KDwJeOBoP/UE/f Gnl7B6TlSbCBIqhgXSPAhnYwEBnbP2fVDdDSLvt3UcmXyzZP+TiYIT43Ojr2gjuvp0ocZGzU H11zbh7qHmmfC2wB3R2ivy6NB5g93807J4db6xtvQ=*Ironport-sdr*: hOOQKyODDHFJznJrxc/uxLdIlF0ipHoTo6vaJepvj08c30iLlirlQNXnDNM7gMQBfgKyKxyE4y 9tyzAcu/aWpYI6Ymg9iBcWpgF8yCoy87YqBybfDrJB4SuI6uSt/+IEMVwKjGvXh/e2i2i/BzQC UDkuqC4aCFyR88+HDAr6Mw3OsG/LTEHGB5X4kkT7CqP6dvNguKdI8QdnyOorCKRjFpAHBr80mu XPIyukHB502h2rA2yEcgQnFBNaJ5Z5i3E8A1jMvysfoBB3n9+SpdzEDm1h6bWdBth51bRL6jmP T944OY06ASr5PKnlyauoeQw9*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):