using the add function in a modular project

Question

I have modeled my project in alloy, and I want to separate the run part from the modeled part of my project. In some fact and predicate I use the add function in cardinality comparison. Here is an example :

#relation1 = add[ #(relation2), 1]

When the run part and the model part are in the same file all work successfully.

But when I separate them in 2 files, I have the following syntax error :

The name "add" cannot be found.

I thought it needed to open the integer module where there is an add function, so I have opened it it the header of the model part. But then the runtime ask me to specify the scope of this/Univ.

You must specify a scope for sig "this/Univ"

Here is an example : first the model in one module

module solo

open util/ordering [A] as chain
//open util/integer

sig A{ b : set B}

fact {  all a : A - chain/last | #(a.next.b) = add[ #(a.b), 2]}

sig B{}

then the run part in another module :

module due

open solo

run {#(solo/chain/first.b) = 2 }for 10 B, 5 A

when I call it like this I have the "the name add cannot be found" error. When I uncomment the integer module opening, I have the "You must specify a scope for sig "this/Univ"" error.

What should I do that to make it works?

Answer 1

If I'm not mistaken + is the union operator and thus can't be used to perform additions.

Which version of alloy are you using ?

I think the add[Int,Int] function was added recently, before it used to be plus[int,int].

You might want to try plus[Int,Int] and see if it solves your problem. Else it would be nice to have access to your models. Maybe the error comes from elsewhere.