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

Thank you for the pointer! I was able to resolve the issue.

I created another module called "test" and imported that into "verification".

At this point, I tried to run evaluation of a constant _expression_ in "verification". That failed again so I imported "test" into "bankAccount" module that is one of the official examples and ran the bankAccount model. After that, I was able to evaluate SUM(10, 10) in both "bankAccount" and "verification". I supposed the problem was that "verification" did not trigger compilation of "test" at first since the model was empty (or I made a mistake again).

Alexander

On Fri, Oct 19, 2018 at 10:38 AM Markus Kuppe <tlaplus-go...@xxxxxxxxxxx> wrote:

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

--
You received this message because you are subscribed to a topic in the Google Groups "tlaplus" group.
To unsubscribe from this topic, visit https://groups.google.com/d/topic/tlaplus/ouHFPoQO5Go/unsubscribe.
To unsubscribe from this group and all its topics, send an email to tlaplus+u...@xxxxxxxxxxxxxxxx.
To post to this group, send email to tla...@xxxxxxxxxxxxxxxx.
Visit this group at https://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.