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

*From*: Hillel Wayne <hwayne@xxxxxxxxx>*Date*: Tue, 24 Oct 2023 23:16:53 -0500*References*: <8c448736-b5e8-4855-a094-3c80ad617a94n@googlegroups.com>*User-agent*: Mozilla Thunderbird

Hi Chris,

Here's a quick toy model:

`VARIABLES x, y`

`Swap ==
/\ x' = y
/\ y' = x
`

If `vars == {x, y}`, then after `Swap `we have `vars'
= {x', y'} = {y, x}`. Since sets are unordered, we have `vars'
= vars`, or `UNCHANGED vars`. But clearly the state
of the system changed!

With `vars == <<x, y>>`, after `Swap`
we have `vars' = <<y, x>>`. Since order
matters in sequences, `vars' # vars` and we get the
expected behavior.

H

On 10/24/2023 6:16 PM, Chris Ortiz
wrote:

Hi tlaplus group,--

I am just curious with the convention why vars is defined as tuples of variables for UNCHANGED, <<A>>_vars, [A]_vars, [][Next]_vars, WF_vars and SF_vars. My understanding is that tuples preserved ordering of elements. Maybe I am still confused or still having a hang over with Programming Language, but I like to understand why tuple is the selected convention for such variables for those semantics, instead of set. Sometimes it confused me to make sure I follow the ordering from how I defined them in vars up to the way I removed variables in my UNCHANGED _expression_.

Thanks,Zitro--

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/8c448736-b5e8-4855-a094-3c80ad617a94n%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/09ad7dea-f272-498c-86ba-9837702dc9b2%40gmail.com.

**Follow-Ups**:**Re: [tlaplus] Why vars is defined as tuples instead of set***From:*Chris Ortiz

**References**:**[tlaplus] Why vars is defined as tuples instead of set***From:*Chris Ortiz

- Prev by Date:
**[tlaplus] Re: Using TLC to model check "rule-based expert systems"** - Next by Date:
**Re: [tlaplus] pluscal: with vs local variable - change in distinct states for action** - Previous by thread:
**[tlaplus] Why vars is defined as tuples instead of set** - Next by thread:
**Re: [tlaplus] Why vars is defined as tuples instead of set** - Index(es):