module main {

    type side_t = enum { Left, Right };
    type object_t = enum { None, Ferryman, Goat, Cabbage, Wolf };

    var ferryman : side_t;
    var goat : side_t;
    var cabbage : side_t;
    var wolf : side_t;
    var carry : object_t;

    procedure cross_ferry(obj: object_t)
        modifies ferryman, goat, cabbage, wolf, carry;
    {
        assume(ferryman == Left);
        assume(carry == None || carry == obj);
        assume(obj != None);

        ferryman' = Right;
        carry' = obj;

        case
            obj == Goat : { goat' = Right; }
            obj == Cabbage : { cabbage' = Right; }
            obj == Wolf : { wolf' = Right; }
        esac
    }

    procedure check_conflict()
    {
        assert !(goat == cabbage && goat != ferryman);
        assert !(goat == wolf && goat != ferryman);
    }

    init {
        ferryman = Left;
        goat = Left;
        cabbage = Left;
        wolf = Left;
        carry = None;
    }

    goal {
        goat == Right && cabbage == Right && wolf == Right
    }

    transition {
        if (ferryman == Left) {
            // Try crossing with different objects
            cross_ferry(Goat);
            check_conflict();
            cross_ferry(Cabbage);
            check_conflict();
            cross_ferry(Wolf);
            check_conflict();
        }
    }
}
