How to denote that a set of values should be distinct?

Question

Is there a reasonable way to denote that n elements need to be distinct from each other? Specifically, I have a sig similar to this one:

sig Node {
up: lone Node,
left: lone Node,
right: lone Node,
left_down: lone Node,
right_down: lone Node
}

and want to write a fact, that defines these to be distinct for any given Node. I am fairly certain I could just write it down as NxN matrix, like this:

fact {
all n: Node | n.up != n.left && n.up != n.right && n.up != n.left_down ...
}

but that seems extremely verbose and rather ugly. What is the proper way to do this?

Answer 1

The fact your suggested expresses that each set should be different, not that each set are disjoint. To check that sets are disjoint, you can simply check that their intersection (&) is empty.

You could thus write :

sig Node {
  up: lone Node,
  left: lone Node,
  right: lone Node,
  left_down: lone Node,
  right_down: lone Node
}{
   up & left=none and
   right & left_down=none and
   (up + left )& (right + left_down)=none and
   (up + left + right + left_down)&right_down=none   
}

A less verbose but uglier way of doing things would be by summing up the intersection of each node with those sets and ensure that the sum is always zero or one.

sig Node {
   up: lone Node,
   left: lone Node,
   right: lone Node,
   left_down: lone Node,
   right_down: lone Node
}{
     all n:Node | add[add[add[add[#(n&up),#(n&left)],#(n&right)],#(n&left_down)],#(n&right_down)] in 0+1
}