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

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).


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?


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,

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.