[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

*From*: rri...@xxxxxxxxx*Date*: Fri, 19 Oct 2018 10:21:26 -0700 (PDT)

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!

**Follow-Ups**:**Re: [tlaplus] Evaluating Complex Constant Expressions in TLA+ Toolbox***From:*Markus Kuppe

- Prev by Date:
**Re: [tlaplus] Possible TLC false positives bug** - Next by Date:
**Re: [tlaplus] Evaluating Complex Constant Expressions in TLA+ Toolbox** - Previous by thread:
**[tlaplus] Re: Practical TLA+ now out** - Next by thread:
**Re: [tlaplus] Evaluating Complex Constant Expressions in TLA+ Toolbox** - Index(es):