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

*From*: "'Alex Weisberger' via tlaplus" <tlaplus@xxxxxxxxxxxxxxxx>*Date*: Tue, 20 Oct 2020 05:40:43 -0700 (PDT)*References*: <777d286f-858b-42c2-ac89-1d2eac77f01en@googlegroups.com> <B6601963-34E5-412A-BAB2-3CBEEEC0B736@gmail.com> <8e33ff4b-097b-43a8-b58a-e35010782ae2n@googlegroups.com>

Do records work for this use case?

If you use a record with a name for the value of each set, you can do:

r == [s1: S1, s2: S2, ... sn: Sn].

r == [s1: S1, s2: S2, ... sn: Sn].

This does give you the Cartesian product of all of the sets S1-Sn, but instead of plain tuples it assigns a name to each value that would be in the tuple,

i.e. if S1 = {1,2,3} and S2 = {4,5,6} then [s1 |-> 1, s2 |-> 4] \in [s1: S1, s2: S2].

On Tuesday, October 20, 2020 at 8:09:16 AM UTC-4 mrynd...@xxxxxxxxx wrote:

Okay, so I wasn't specific enough. I know that \X in TLA+ is not commutative and in fact not even associative.I wanted something that would give me:Cartesian({{1, 2}, {3, 4}, {5}}) = {{1, 3, 5}, {1, 4, 5}, {2, 3, 5}, {2, 4, 5}}Your last definition works in TLC. Thanks Stephan!Is the `Range` operator defined somewhere in official/builtin modules?Range(f) == { f[x] : x \in DOMAIN f }Regarding overriding in Java, is it recommended only for to performance reasons?wtorek, 20 października 2020 o 13:41:38 UTC+2 Stephan Merz napisał(a):Hello,your problem is not well specified because {S1, S2} = {S2, S1} but S1 \X S2 is different from S2 \X S1. Also, I don't understand your remark about the output: the cartesian product is a set, but its elements are sequences.Assuming that your operator takes a *sequence* of sets, i.e. Cartesian(<<S1, S2, ..., Sn>>), you can write the following in TLA+.Range(S) == { S[i] : i \in 1 .. Len(S) }Cartesian(S) ==LET U == UNION Range(S)IN {s \in Seq(U) : /\ Len(s) = Len(S)/\ \A i \in 1 .. Len(s) : s[i] \in S[i]}However, TLC will not be available to interpret this because of the quantification over the infinite set Set(U). The following should work in principle (I haven't actually tried):Cartesian(S) ==LET U == UNION Range(S)FSeq == [ (1 .. Len(s)) -> U ]IN {s \in FSeq : \A i \in 1 .. Len(s) : s[i] \in S[i]}However, you probably want to override this operator definition by a Java method.StephanOn 20 Oct 2020, at 13:27, Mariusz Ryndzionek <mrynd...@xxxxxxxxx> wrote:Hello,I need n-ary Cartesian product operator. Something that would do:Cartesian({S1, S2, .., Sn}) = S1 \X S2 \X .. SnThe output shouldn't necessarily be sequences. Sets will do.Is there already something like this in TLA+?Regards,Mariusz--

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+u...@xxxxxxxxxxxxxxxx.

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/777d286f-858b-42c2-ac89-1d2eac77f01en%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/f8373cf0-fceb-480e-b939-57a0610bc81fn%40googlegroups.com.

**Follow-Ups**:**Re: [tlaplus] n-ary Cartesian product***From:*Mariusz Ryndzionek

**References**:**[tlaplus] n-ary Cartesian product***From:*Mariusz Ryndzionek

**Re: [tlaplus] n-ary Cartesian product***From:*Stephan Merz

**Re: [tlaplus] n-ary Cartesian product***From:*Mariusz Ryndzionek

- Prev by Date:
**Re: [tlaplus] n-ary Cartesian product** - Next by Date:
**Re: [tlaplus] n-ary Cartesian product** - Previous by thread:
**Re: [tlaplus] n-ary Cartesian product** - Next by thread:
**Re: [tlaplus] n-ary Cartesian product** - Index(es):