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
Description: PNG image
