Understanding complicated signatures in alloy

Question

in the below

sig building{
    abv: Man -> Man
 }
 {
 all m:Man | Above(m,m.abv)
 }

What does the below mean? How is it related to the signature definition? Is this a relation for the sig?

 {
 all m:Man | Above(m,m.abv)
 }

Answer 1

That is called "appended fact", and the meaning is that it must hold for all atoms of the corresponding sig. So, an equivalent fact for your model would be

fact {
  all b: building |
    all m: Man | Above[m, m.(b.abv)]
}

In appended facts you can use the this keyword to refer to the current atom of the corresponding sig, so a clearer way to write your appended fact would be to explicitly write m.(this.abv), as opposed to relying on abv being implicitly expanded to this.abv.