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

*From*: Markus Kuppe <tlaplus-go...@xxxxxxxxxxx>*Date*: Fri, 19 Oct 2018 10:38:43 -0700*References*: <4d923a57-514b-4486-8122-62d7ff983271@googlegroups.com>

On 19.10.18 10:21, rri...@xxxxxxxxx wrote: > 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? Hi, is "verification" the root module of the specification for which you created the TLC model? Have a look at the attached screenshot: The spec is called "HillelWayne.tla" for which the module "HillelWayne" is the root module. The module "fsadfa" is an additional module. The TLC model "Model_1" for spec "HillelWayne.tla" knows nothing about the module "fsadfa" and thus reports "Unknown Operator: SUM. If you have the (root) module "HillelWayne" extend "fsadfa", Model_1 will be able to resolve the operator SUM. Hope this helps, Markus

**Attachment:
Screenshot from 2018-10-19 10-30-54.png**

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

**References**:**Evaluating Complex Constant Expressions in TLA+ Toolbox***From:*rri . . .

- Prev by Date:
**Evaluating Complex Constant Expressions in TLA+ Toolbox** - Next by Date:
**Re: [tlaplus] Evaluating Complex Constant Expressions in TLA+ Toolbox** - Previous by thread:
**Evaluating Complex Constant Expressions in TLA+ Toolbox** - Next by thread:
**Re: [tlaplus] Evaluating Complex Constant Expressions in TLA+ Toolbox** - Index(es):