Re: [tlaplus] Unexpected result of [S -> T] evaluation

Hi,

Did you receive an answer to this yet? In case you did not, what you are seeing is the pretty printer reducing the first _expression_ to a shorter sequence representation.

The term "<<1, 1>>", which is a sequence, is the set of mappings 1 to 1 and 2 to 1, which is equivalent to "(1:>1 @@ 2:>1)". In this case, the pretty printer realizes that the left-hand sides of the mappings are the same as what they would be in a sequence and reduces the output to sequence form.

It think if you evaluated "{(1:>1 @@ 2:>1), (1:>1 @@ 2:>2), (1:>2 @@ 2:>1), (1:>2 @@ 2:>2)}" it would print the set of sequences you saw. (I don't have the toolbox handy to check myself, but I think it would do that.)

Hope my information is accurate and helps you,

Robert

On Sat, Aug 18, 2018 at 1:05 AM Hengfeng Wei <hengx...@xxxxxxxxx> wrote:

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 are wrong with my evaluations?

--
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 post to this group, send email to tla...@xxxxxxxxxxxxxxxx.
Visit this group at https://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.