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

*From*: Alexander Ivaniuk <rri...@xxxxxxxxx>*Date*: Fri, 19 Oct 2018 10:55:04 -0700*References*: <4d923a57-514b-4486-8122-62d7ff983271@googlegroups.com> <019cd1d7-4b02-3fe5-66c5-ee99d0c0f413@lemmster.de>

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.

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

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

**Re: [tlaplus] Evaluating Complex Constant Expressions in TLA+ Toolbox***From:*Markus Kuppe

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