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

[Markus Kuppe <tlaplus-go...@xxxxxxxxxxx>]

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