Farmer crossing as first exercise As a first step into the world of Alloy, I've done my own version of the Fox/Chicken/Grain problem. I'd be grateful for any comments (also, is there a better place to do this?).
I thought it worth separating out the Farmer from the other items so I don't have to keep removing it from the set of items.
open util/ordering[Time]

sig Time {}

enum Place {Near, Far}

abstract sig Locatable { location: Place one -&gt; Time }
abstract sig Edible extends Locatable {} 
one sig Fox, Chicken, Grain extends Edible {}
one sig Farmer extends Locatable {}

pred init(t: Time) { Locatable.location.t = Near }

pred done(t: Time) { Locatable.location.t = Far }

pred stayPut(t, t': Time, edibles: set Edible) {
    all e : edibles | e.location.t = e.location.t'
}

pred carryAcross(t, t' : Time) {
    one e: Edible {
        e.location.t = Farmer.location.t
        e.location.t' = Farmer.location.t'
        stayPut[t, t', Edible - e]
    }
}

pred crossRiver(t, t' : Time) {
    stayPut[t, t', Edible]
}

pred nextCrossing(t, t' : Time) {
    Farmer.location.t' != Farmer.location.t
    carryAcross[t, t'] or crossRiver[t, t']
}

pred eats [a, b: Edible] { a-&gt;b in Fox-&gt;Chicken + Chicken-&gt;Grain }

fact ProtectFromEating {
    all p, q: Edible, t: Time |
    p.eats[q] and p.location.t = q.location.t =&gt; q.location.t = Farmer.location.t
}

fact Traces {
    first.init
    all t: Time - last | let t' = t.next |
        done[t] or nextCrossing [t, t']
}

fact Done {
    some t: Time | done[t]
}

run {} for 8 Time
I am personally not a fan of the Time pattern, it gets messy quickly. There is an extension in the works, called electrum that allows you to use variables.
Overall your solution seems too detailed. The magic of alloy is that you only have to say what you want to achieve. I.e. the animals should always be safe and and somehow they need to end up on the other side. I.e. you don't care about the crossing itself that much as long as you ensure there is never a lunch happening.
My personal favorite solution for this problem is:
open util/ordering[Crossing]
enum Object { Farmer, Chicken, Grain, Fox }

let eats = Chicken-&gt;Grain + Fox-&gt;Chicken
let safe[place] = Farmer in place or (no place.eats &amp; place)

sig Crossing {
    near, far : set Object,
    carry :  Object
} {
    near = Object - far
    safe[near] 
    safe[far]
}

run {
    first.near = Object
    no first.far
    all c : Crossing - last, c': c.next {
        Farmer in c.near implies { 
            c'.far = c.far + c.carry + Farmer
        } else {
            c'.near = c.near + c.carry + Farmer
        }
    }
    some c : Crossing | c.far = Object
} for 8

Peter Kriens @pkriens