How to reuse facts by means of modules in Alloy

Question

I have the following specification in Alloy:

sig A {}
sig Q{isA: one A}

fact {
    all c1,c2:Q | c1.isA=c2.isA  => c1=c2   // injective mapping
    all a1:A | some c1:Q | c1.isA=a1   //surjective 
}

In my models the above fact repeats similarly between different signature. I tried to factor out it as a separate module so I created a module as below:

module library/copy [A,Q]

fact {
    all c1,c2:Q | c1.isA=c2.isA  => c1=c2   // injective mapping
    all a1:A | some c1:Q | c1.isA=a1   //surjective 
}

Then I tries to use it as bellow:

module family

open library/copy [Person,QP] 
sig Person {} 
sig QP{isA:Person}
run {} for 4

but Alloy complains that "The name "isA" cannot be found." in the module.

What is wrong with my approach? and Why alloy complains?

Answer 1

In my previous answer I tried to address your "similarly between different signature" point, that is, I thought your main goal was to have a module that somehow enforces that there is a field named isA in the sig associated with parameter Q, and that isA is both injective and surjective. I realize now that what you probably want is reusable predicates that assert that a given binary relation is injective/sujective; this you can achieve in Alloy:

library/copy.als

module copy [Domain, Range]

pred inj[rel: Domain -> Range] {
  all c1,c2: Domain | c1.rel=c2.rel => c1=c2   // injective mapping
}

pred surj[rel: Domain -> Range] {
  all a1: Range | some c1: Domain | c1.rel=a1   //surjective 
}

family.als

open copy[QP, Person] 
sig Person {} 
sig QP{isA:Person}

fact {
  inj[isA]
  surj[isA]
}

run {} for 4

In fact, you can open the built-in util/relation module and use the injective and sujective predicates to achieve the same thing, e.g.:

family.als

open util/relation
sig Person {} 
sig QP{isA:Person}

fact {
  injective[isA, Person]
  surjective[isA, Person]
}

run {} for 4

You can open the util/relation file (File -> Open Sample Models) and see a different way to implement these two predicates. You can then even check that your way of asserting injective/surjective is equivalent to the built-in way:

open copy[QP, Person]
open util/relation

sig Person {} 
sig QP{isA:Person}

check {
  inj[isA] <=> injective[isA, Person]
  surj[isA] <=> surjective[isA, Person]
} for 4 expect 0 // no counterexample is expected to be found