How do you use "No Behavior Spec" to test an operator?

[axelson]

On the operators page there is this reminder:

Remember, you can use the “No Behavior Spec” option in your TLC model to test various operators and cases.

Which conceptually makes sense, but if I try to put the operator definition (Neq(a,b) == a /= b ) directly in the "Evaluate Constant Expression" section then I get an error. Similarly if I put the operator definition in the PLUSCAL algorithm I get a compilation error. I suppose this is because an operator is a TLA+ concept rather than a PLUSCAL concept.

But at this point in the tutorial we haven't written any actual TLA+ code yet and I'm a bit unsure how to best do so. I can add the operator definition in the middle of the TLA+ block but that wouldn't be the best place since it will get overridden upon the next PLUSCAL translation. I guess the best place would be before or after the BEGIN TRANSLATION or END TRANSLATION statements?

By the way I'm very much enjoying the tutorial so far. I'm asking these questions to further my edification as well as improve the tutorial for everyone else. For this particular issue I think that either I'd remove the tip block or add a new section that will actually run the user through adding an operator definition to their TLA file (and telling them where it should go).

[hwayne]

Good catch. An operator is a definition, not an expression. LET Neq(a,b) == a /= b IN Neq(1,2) is valid because that's an expression. I'll review and see if there's a better way to make that distinction. I'll also move the "Integrating with PlusCal" block higher on the page.

[axelson]

Yeah, I think moving the "Integrating with PlusCal" section higher on the page is the main change that is needed.

[OussamLK]

if I try to put the operator definition (Neq(a,b) == a /= b ) directly in the "Evaluate Constant Expression" section then I get an error.

I got stuck here as well, the notion of "expression" is still not defined at this point in the tutorial, and I did spend some time trying to run the examples given in the "Operators" section. I guess the fix is not to suggest running the examples in No Behavior Spec

Tip.
Remember, you can use the “No Behavior Spec” option in your TLC model to test various operators and cases.