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

Re: [tlaplus] Initial state doesn't satisfy type invariant

It took me some time to see that [(SUBSET A) -> B] is not the same as UNION {[X -> B] : X \in SUBSET A}, so I thought I'd write them out here for clarity in case someone else stumbles on it. Apologies for the verbosity -- though it seems obvious now, I didn't start out that way and had to work through it.

Consider A = 1..2 and B = {"a", "b"} 

Then [(SUBSET A) -> B] is the set of all mappings that assign an element of B to each element of SUBSET(A). For the given A, there are 4 subsets - {}, {1}, {2}, {1,2}. So the cardinality of this set is Cardinality(B) ^ Cardinality(SUBSET A) = 2^4 = 16 .. where each of these subsets of A can be assigned either "a" or "b". Now for the obvious thing - all the functions in this set have the same domain.

{[X -> B] : X \in SUBSET A} is the set of sets of functions whose domain is from SUBSET(A) and whose range is B. So this is -

{ [{} -> B], [{1} -> B], [{2} -> B], [{1,2} -> B] }

The first is {<< >>} (the singleton set with the empty tuple)
The second is {<<"a">>,<<"b">>}
The third is {(2 :> "a"), (2 :> "b")}
The fourth is {<<"a","a">>,<<"a","b">>,<<"b","a">>,<<"b","b">>}

The main thing to notice here is that the domains of the functions are all not the same.

Let S1 = [SUBSET(A) -> B] and S2 = UNION {[X -> B] : X \in SUBSET A},

So the cardinality of S2 is 9 .. whereas for S1 is 16.

{DOMAIN X : X \in S1} = {{{}, {1}, {2}, {1, 2}}} (cardinality 1, since all the functions in S1 have the same domain of cardinality 2^Cardinality(A) = 4)
{DOMAIN X : X \in S2} = {{}, {1}, {2}, {1, 2}} (cardinality 4, since the functions can have one of 4 possible domains, each of which is a subset of A)

Hope this helps somebody like me.

On Tuesday, December 8, 2020 at 11:02:49 AM UTC+5:30 t...@xxxxxxxxxxxxxx wrote:
Yes. The second is what I’m now using.

Thank you for the help.

On Dec 8, 2020, at 12:19 AM, Srikumar Subramanian <srikumar.s...@xxxxxxxxxxxx> wrote:

I guess you meant this? -

edges_stack \in Seq(UNION {[X -> Nodes] : X \in SUBSET Labels})

or perhaps -

edges_stack \in Seq(UNION {[X -> Nodes] : X \in {1..n : n \in Labels}})


This mail contains confidential information intended only for the individual(s) named. If you’re not the named addressee, don’t disseminate, distribute or copy this e-mail. Please notify the sender immediately and delete it from your system.If you wish not to receive such e-mails you may reply with text “Unsubscribe”.

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/cd36eaeb-0e53-40cf-a5c5-0fd5895d3793n%40googlegroups.com.