tlaplus / vscode-tlaplus

TLA+ language support for Visual Studio Code
MIT License
357 stars 33 forks source link

Evaluating constant expression yields wrong result for this expression #176

Closed arnaudbos closed 3 years ago

arnaudbos commented 4 years ago

Using the "Evaluate expression" or "Evaluate selected expression" I've tried this expression for some reason, and it did yield a wrong representation of the result in the Output window.

>> [1..5 -> {[a |-> {"a"}]}]
{<<[a |-> {"a"}], [a |-> {"a"}], [a |-> {"a"}]>>}

instead of

{<<[a |-> {"a"}], [a |-> {"a"}], [a |-> {"a"}], [a |-> {"a"}], [a |-> {"a"}]>>}

I said that only the representation is wrong because the domain is correct

>> DOMAIN CHOOSE x \in [1..5 -> {[a |-> {"a"}]}] : TRUE
{1, 2, 3, 4, 5}

It may be an evaluation error for this specific expression, or some representation error maybe.

The output is actually similar for any number of elements in the inner function. But if the value is not a set then the 5 elements of the resulting set are correctly rendered:

>> [1..5 -> {[a |-> "a"]}]
{<<[a |-> "a"], [a |-> "a"], [a |-> "a"], [a |-> "a"], [a |-> "a"]>>}

This error does not occur in the TLA+ Toolbox.

At first glance I did not find a quick way to test this using the tla2tools.jar (the embedded one doesn't seem to be the latest released version) because I have no idea how to use it.
If you'd like more details or if you want me to give this bugfix a try I'd be happy to help, but I could use some help with setting up a command-line repro-case (a documentation link maybe?) and/or pointers to thing to look at.

And thanks for the great plugin by the way.

lemmy commented 4 years ago

Fixed in https://github.com/alygin/vscode-tlaplus/pull/177

alygin commented 4 years ago

@arnaudbos, thanks for the report, and @lemmy, thanks for the fix! Fix is available in the 1.5.2-alpha.1 prerelease

alygin commented 3 years ago

Fix published in v1.5.2