
module main {
    type Side;
    const left : Side;
    const right : Side;

    // Variables representing locations
    var ferryman : Side;
    var goat : Side;
    var cabbage : Side;
    var wolf : Side;
    var carry : Side;

    // Initial state
    init
    {
        ferryman = left;
        goat = left;
        cabbage = left;
        wolf = left;
        carry = left;
    }

    // Transition relation
    next
    {
        ferryman' = carry';
        wolf' = ite(carry = wolf, carry', wolf);
        goat' = ite(carry = goat, carry', goat);
        cabbage' = ite(carry = cabbage, carry', cabbage);
        carry' = ite(carry = left, right, left);
    }

    // Safety condition: goat and cabbage or goat and wolf must not be alone on one side
    constraint
    {
        (goat = cabbage => ferryman = goat) && (goat = wolf => ferryman = goat);
    }

    // Goal state
    define goalState : bool {
        ferryman = right && goat = right && cabbage = right && wolf = right;
    }

    // Reachability property: Can we achieve the goal state without violating constraints?
    control {
        check;
        synth invariant;
    }
}