Alloy : Graph coloring

Question

Here are the signatures :

abstract sig Color{}
lone sig Red, Blue, Yellow, Green extends Color{}

abstract sig Vertex{
  couleur: Color
}

abstract sig Digraph{
   vertices: set Vertex,
   edges: set(Vertex -> Vertex)
}
fact{
   vertices.couleur != edges.couleur
}

I get an error saying that I can't use "!=" between 2 expressions that aren't the same arity. I get why, but I don't know how I can solve this.
What I want to do is, forbidding the two vertices color to be the same in an edge. Any ideas ?

ivcha ivcha · Accepted Answer · 2016-09-22T22:23:48

The answer is very simple: the expression vertices.couleur != edges.couleur does not typecheck since vertices and edges, and thus also the operands of !=, are of different arity. (Essentially, you are trying to compare a set of Color to a set of (Color -> Vertex).)

As an example, if you take the image of the edges relation (by projecting it onto the universal set), you will not get the error:

fact {
   vertices.couleur != edges.univ.couleur
}

(For more info about the basic operators in Alloy, it would be useful to check the tutorial and/or the Alloy book.)

Alloy : Graph coloring

1 Answers