#define SIZEOF(i) dom[i].length
#define OFFTOP(i, off) dom[i].disc[SIZEOF(i) - off]
#define TOP(i) OFFTOP(i, 1)

#define CAN_MOVE(src, dst) \
    SIZEOF(src) > 0 && \
    (SIZEOF(dst) == 0 || TOP(src) < TOP(dst))

#define MOVE(src, dst) \
    atomic { \
        printf("%d: %d -> %d\n", TOP(src), src, dst); \
        OFFTOP(dst, 0) = TOP(src); \
        SIZEOF(dst)++; \
        SIZEOF(src)-- \
    }

typedef Stick {
    byte disc[4];
    byte length;
};

Stick dom[3];

active proctype P() {
    do
    :: CAN_MOVE(0, 1) -> MOVE(0, 1)
    :: CAN_MOVE(0, 2) -> MOVE(0, 2)
    :: CAN_MOVE(1, 0) -> MOVE(1, 0)
    :: CAN_MOVE(1, 2) -> MOVE(1, 2)
    :: CAN_MOVE(2, 0) -> MOVE(2, 0)
    :: CAN_MOVE(2, 1) -> MOVE(2, 1)
    od
}

init {
    dom[0].length = 4;
    dom[0].disc[0] = 4;
    dom[0].disc[1] = 3;
    dom[0].disc[2] = 2;
    dom[0].disc[3] = 1;
}

ltl goal { !<>(SIZEOF(1) == 4) }