Unexpected result of [S -> T] evaluation

[Hengfeng Wei <hengx...@xxxxxxxxx>]

Hi,

I evaluate [{1,2} -> {1,2}]  in "Evaluate Constant _expression_"

and obtain an unexpected result: {<<1, 1>>, <<1, 2>>, <<2, 1>>, <<2, 2>>}.

The _expression_ [{1,3} -> {1,3}] gives the expected result:

{ (1 :> 1 @@ 3 :> 1),

     (1 :> 1 @@ 3 :> 3),

     (1 :> 3 @@ 3 :> 1),

     (1 :> 3 @@ 3 :> 3) }.

I am using the latest TLA+ Toolbox (Version 1.5.7 of 18 July 2018).

What is wrong with my evaluations?

Hengfeng Wei