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

Re: [tlaplus] Evaluating Complex Constant Expressions in TLA+ Toolbox

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?


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,

Attachment: Screenshot from 2018-10-19 10-30-54.png
Description: PNG image