module main {
    var st: boolean;
    var message1, message2: boolean;
    var ack: boolean;

    init {
        st = false;
        message1 = false;
        message2 = false;
        ack = false;
    }

    next {
        if (!st) {
            if (message1) {
                message2' = message2;
            } else {
                message2' = true;
            }
        } else {
            message2' = message2;
        }
        if (message2) {
            message1' = false;
        } else {
            message1' = message1;
        }
        if (message1) {
            st' = !st;
        } else {
            st' = st;
        }
        if ((!st) && message2) {
            ack' = true;
        } else {
            ack' = ack;
        }
    }

    control {
        v = unroll(5);
        check;
        print_results;
        v.print_cex(st,message1,message2,ack);
    }
}
