Nested cartesian product evaluation

[sthiers]

Let the chessboard squares be represented by cartesian product: {"a", "b", "c", "d", "e", "f", "g", "h"} \X (1..8) This correctly evaluates to:

{ <<"a", 1>>,
  <<"a", 2>>,
  <<"a", 3>>,
  <<"a", 4>>, .....}

ie a set of tuples, each tuple representing a square (ex: <<"a",2>> )

Now, let represent all possible pairs of squares:
({"a", "b", "c", "d", "e", "f", "g", "h"} \X (1..8)) \X ({"a", "b", "c", "d", "e", "f", "g", "h"} \X (1..8))

I'd expect to have a set of pairs of squares:

{ <<<<"a", 1>>, <<"a", 1>>>>,
  <<<<"a", 1>>, <<"a", 2>>>>,
  <<<<"a", 1>>, <<"a", 3>>>>,
  <<<<"a", 1>>, <<"a", 4>>>>, ...} 

i.e. a set of 2 elements tuples with whose first and second elements are themselves also tuples, each representing a square. (ex: <<<<"a", 1>>, <<"a", 2>>>>)

Instead, I get something like: ({<<"a", 1>>, <<"a", 2>>, <<"a", 3>>, <<"a", 4>>, ... }, i.e a set of simple "squares".

Strangely, when reducing the expression to (by omitting the 5 last columns "d".."h" in 2nd product) : ({"a", "b", "c", "d", "e", "f", "g", "h"} \X (1..8)) \X ({"a", "b", "c"} \X (1..8))

Then I get the expected result.

Version Notes: On Win10 This is Version 1.5.4 of 06 October 2017 and includes:

• SANY Version 2.1 of 23 July 2017
• TLC Version 2.10 of 28 September 2017
• PlusCal Version 1.8 of 07 December 2015
• TLATeX Version 1.0 of 20 September 2017

Using TLA+-REPL for evaluations

[lemmy]

@sthiers Can you please verify with the most recent nightly build that this problem still exists? Also since you explicitly mention "Evaluate Constant Expression", don't you see the issue when you use the same expressions in your spec?

[sthiers]

Apparently, it works fine directly in a spec with version 1.5.6 of 29 January 2018.

So initial issue could come either from TLA+ version # or from TLA+-REPL ? ( @will62794 another test with updated TLA+ in TLA+-REPL led to same observations)

[will62794]

It's tough to tell definitively, but this seems like it may be a TLC bug. I have tried to evaluate the following expression (using "Evaluate Constant Expression") using the latest nightly build of the Toolbox (1.5.7):

LET n==8 S == (1..n) IN (S \X S) \X (S \X S)

and it produces a result like the following:

{<<1, 1>>, <<1, 2>>, <<1, 3>>, <<1, 4>>, <<1, 5>>, <<1, 6>>,...}

What's weird is that it, as @sthiers pointed out, it seems to produce the correct result when the set size is decreased. So evaluating the same expression but with n==6 the Toolbox shows:

{ <<<<1, 1>>, <<1, 1>>>>,
     <<<<1, 1>>, <<1, 2>>>>,
     <<<<1, 1>>, <<1, 3>>>>,...}

It seems to produce an incorrect result for values n>=7. I haven't explored enough to determine the root cause here. This was an initial attempt at minimizing the bug; I may be able to simplify it further.

[will62794]

Actually, it seems like it may be some kind of issue with the TLC Print operators. Evaluating this expression seems to produce an element of the right "type":

LET n==8 S == (1..n) IN CHOOSE x \in (S \X S) \X (S \X S) : TRUE

Value: <<<<1, 1>>, <<1, 1>>>>

So it would seem to indicate that the underlying set is being constructed in the proper manner.

[lemmy]

The underlying set is indeed constructed correctly and the issue is purely cosmetic. SetOfTuplesValue#toString does not fully construct a set if its size exceeds the bound defined in TLCGlobals.enumBound. Instead, it prints an intermediate set with leaves the innermost \X unevaluated.

E.g. with TLCGlobals.enumBound = 10 and LET S == 1..2 IN (S \X S) \X (S \X S):

({<<1, 1>>, <<1, 2>>, <<2, 1>>, <<2, 2>>} X {<<1, 1>>, <<1, 2>>, <<2, 1>>, <<2, 2>>})

[lemmy]

This issue revealed a regression - introduced with the Toolbox's foundation upgrade to Eclipse e4 in 2004 - such that the evaluate constant expressions and the user output source viewers do not correctly wrap text anymore.