Farmer crossing as first exercise
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