hwayne
text seems to silently swap between examples
On Writing an Invariant seems to switch silently between examples. It start by using "another spec for finding duplicates that also runs without error", the one where is_unique is set to TRUE. But in the later section Testing Duplicates it seems to be taking the example on the page Writing Specifications in which is_unique gets updated. The first five or seven times I read the page Writing an Invariant I was so confused that I came close to giving up on the whole endeavour, feeling that if I'm not smart enough to understand how the text could possibly apply to the example given on that page I've basically got no chance of ever using this tool.
One consequence of this is that the example under The power of => on that page, which is described as failing, actually succeeds, in the toolbox as well as in the Intellij plugin, even when downloaded from the provided link https://www.learntla.com/_downloads/7e985388d98ea7714e2f4d1f3977bcb7/duplicates.tla and the described fix works too, making it very unclear what is wrong with the explanation of the first one failing since both versions succeed.
