Fusion of built-in math functions does not work in imported files

Question

I have an alloy model in avlTree.als. This model uses integer arithmetic, in particular the plus and minus functions. This model has some statements in it, and I can use them just fine using the graphical interface of the alloy analyzer.

I have another alloy model in test.als. This model imports avlTree (using "open avlTree") and then has some relationship statements in the avlTree model. But when I try to run these statements in the Alloy Analyzer GUI, I get the following message:

A syntax error occurred:

Unable to find the name plus.

And the syntax error link leads me to my avlTree model. It seems that using the integer math model when using avlTree works fine when I run this model myself, but it breaks when I try to import it into another model. Is there a fix for this?

I am running Alloy 4.2.

Answer 1

Yes, this is a mistake, but there is a quick workaround that should explicitly open the integer module by writing

open util/integer 

at the beginning of your avlTree.als file. After that, you can open avlTree and check its claims from other modules.