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

*From*: Stephan Merz <stephan.merz@xxxxxxxxx>*Date*: Tue, 20 Oct 2020 13:41:33 +0200*References*: <777d286f-858b-42c2-ac89-1d2eac77f01en@googlegroups.com>

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. Stephan
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/B6601963-34E5-412A-BAB2-3CBEEEC0B736%40gmail.com. |

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

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

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