How to get a set in this way in TLA+?

Question

Hello I'm a newbie in TLA+.

I knew that Cartesian product is something like this:  S × T × U = {<<a, b, c>> : a ∈ S, b ∈ T,c ∈ U }.

The result of product is a set of sequence.

And I wonder how can I get a set like this in TLA+,if I have sets S,T and U: {{a, b, c} : a ∈ S, b ∈ T,c ∈ U }.

This set's element should be sets,not sequences.

Thank you.

Answer 1

Just to summarize the excellent answer on the mailing list: insert a colon into the mathematical definition and use \in, then you're there:

A == {1,2,3}
B == {"a","b","c"}
C == {42,23}
Tuples == { <<a,b,c>> : a \in A, b \in B, c \in C} 
Sets == { {a,b,c} : a \in A, b \in B, c \in C}

Creating a model and choosing "evaluate constant expression" you can enter Tuples to get:

{ <<1, "a", 23>>,
     <<1, "a", 42>>,
     <<1, "b", 23>>,
     <<1, "b", 42>>,
     <<1, "c", 23>>,
     <<1, "c", 42>>,
     <<2, "a", 23>>,
     <<2, "a", 42>>,
     <<2, "b", 23>>,
     <<2, "b", 42>>,
     <<2, "c", 23>>,
     <<2, "c", 42>>,
     <<3, "a", 23>>,
     <<3, "a", 42>>,
     <<3, "b", 23>>,
     <<3, "b", 42>>,
     <<3, "c", 23>>,
     <<3, "c", 42>> }

If you try the same with Sets it won't work because TLC can only evaluate homogenous sets but we would need to mix integers and strings here (this is a design decision of TLC, the language itself allows us to express this). Setting B == {100} we get:

{ {1, 23, 100},
     {1, 42, 100},
     {2, 23, 100},
     {2, 42, 100},
     {3, 23, 100},
     {3, 42, 100} }

I can also highly recommend Leslie Lamport's book Specifying Systems. It explains TLA+ in detail and has a chapter on TLC as well.

Answer 2

Maybe I'm misunderstanding your question but I'd think this would work

---- MODULE stack_overflow_question ----

S == {"a"}
T == {"b"}
U == {"c"}
alltogether == S \union T \union U

==== 

At least this is what I get back when I evaluate "alltogether"

Evaluating constant expression:
alltogether

{"a", "b", "c"}