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