How can one express that a relationship must not be cyclic?

Question

Consider a upgrades relationship:

I need to make sure that upgrades cannot be circular. How can I do that in Alloy?

Answer 1

It is sufficient to enforce transitivity and antireflexivity.

fact {
  no a: Item | a in a.upgrades
}

fact{
  all a,b,c: Item |
  a in b.upgrades and b in c.upgrades implies
  a in c.upgrades
}

Answer 2

From your example, I infer that the upgrades relation is not intended to be transitive: in the example, a diamond sword upgrades a stone sword, and a stone sword upgrades a wooden sword, but the pair WoodSword -> DiamondSword is not in the upgrades relation.

So what you want to say is something like

fact upgrades_acyclic {
  no x : univ | x in x.^upgrades
}

Some modelers prefer the more succinct formulation in terms of relations:

fact upgrades_acyclic { no ^upgrades & iden }