Ran into an issue with the last example in the "Using the Toolbox" section

[axelson]

Hi! Me again.

On the final step of the "Using the Toolbox" section you are instructed to add the following string to the "Evaluate Constant Expression" section of the "Model Checking Results" tab:

CHOOSE x \in {1, 2, 3} : x*x = 4

However, upon doing so I get the following error:

Multiply-defined symbol 'x': this definition or declaration conflicts with the one at line 11, col 11 to line 11, col 11 of module integers.

Changing to code to use the y variable results in the correct response of 2.

CHOOSE y \in {1, 2, 3} : y*y = 4

It appears that the definition of x in "Evaluate Constant Expression" conflicts with the value of x in the PLUSCAL algorithm. And the tutorial could be fixed by either instructing the user to remove the code from their algorithm or change the new definition to use the variable y instead of x.

[hwayne]

Having them try y instead of x seems less onerous, so I'll go with that. Thank you!

[axelson]

Great, thanks!