[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.
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.