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?