Search code examples
alloy

Alloy - Irreflexivity

I just started using Alloy. I have a question about the following minimal example:

module test

abstract sig MySig {    
  my_rel : set MySig
}

//fact my_rel_irrefl {no iden & my_rel }   // this works
fact my_rel_irrelfl {my_rel not in iden} // this does not work

run {}

Why is the second my_rel_irrelfl not working? My thinking was that, e.g.

MySig = {N0,N1,N2} iden = {(N0,N0),(N1,N1),(N2,N2)}

If there is an element (x,x), where x in MySig in the relation my_rel then it has to be in iden as well.

However, I get this model:

model found by alloy

I.e. one where my_rel is reflexive.

Solution

  • my_rel not in iden says that my_rel is not a subset of iden. Since N0 -> N1 in my_rel and N0 -> N1 not in iden, my_rel isn't a subset and the fact still holds.