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

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



Hi Robert,

I see now.
And your guess about {(1:>1 @@ 2:>1), (1:>1 @@ 2:>2), (1:>2 @@ 2:>1), (1:>2 @@ 2:>2)} is confirmed by the Toolbox.

Thanks.

Best regards,
Hengfeng Wei

On Saturday, August 18, 2018 at 11:11:32 PM UTC+8, Robert Beers wrote:

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 <heng...@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...@googlegroups.com.
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.