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