Evaluating Complex Constant Expressions in TLA+ Toolbox

[rri...@xxxxxxxxx]

Hi folks,

I started learning TLA+ and stumbled upon a problem from the very beginning. I am following the flow of https://learntla.com/ and one of the chapters (https://learntla.com/tla/operators/) says "Remember, you can use the No Behavior Spec option in your TLC model to test various operators and cases." 

Okay, I chose the "No Behavior Spec" option and now I can evaluate simple expression like 5 + 5, which produces a correct result 10. I am trying to play with more complex syntax but cannot make TLA+ to recognize that. For example, it looks like I cannot put something like  SUM(a, b) ==  a + b in the expression evaluator and call SUM(10, 10). I have tried creating a module with contents below:

  ---------------------------- MODULE verification ----------------------------
  EXTENDS Naturals
  SUM(a, b) ==  a + b
  ================================================================

However, SUM(20, 20) still does not work for me in the expression evaluator. The error is "Unknown Operator: 'SUM'". What am I doing wrong?

Thank you in advance!