Evaluating Complex Constant Expressions in TLA+ Toolbox

[rri...@gmail.com]

Hi folks,

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?

Thank you in advance!

[Markus Kuppe]

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

[Alexander Ivaniuk]

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

--
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...@googlegroups.com.
To post to this group, send email to tla...@googlegroups.com.
Visit this group at https://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.

[Markus Kuppe]

On 19.10.18 10:55, Alexander Ivaniuk wrote:
> Thank you for the pointer! I was able to resolve the issue. 
>
> I created another module called "test" and imported that into
> "verification". 

> image.png 

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

"All problems in computer science can be solved by another level of
indirection" (D. Wheeler)


It sounds as if bankAccount is your root module. If you extend
verification and/or test in backAccount, the model will resolve all
operators in verification and test.

By the way, in TLA+ nothing gets "compiled".

Cheers
Markus