module main {

    type state_t = enum { SENDER_0, RECEIVER_0, SENDER_1, RECEIVER_1 };

    var st : state_t;
    var message1 : boolean; // message bit
    var message2 : boolean; // control bit
    var ack : boolean; // acknowledgement bit

    const DATA_BIT = 0;
    const CONTROL_BIT_0 = 0;
    const CONTROL_BIT_1 = 1;

    init {
        st = SENDER_0;
        message1 = DATA_BIT;
        message2 = CONTROL_BIT_0;
        ack = false;
    }

    procedure sender()
        modifies st;
        modifies message2;
    {
        assume(st == SENDER_0 && message2 == CONTROL_BIT_0);
        st := RECEIVER_0;
        message2 := CONTROL_BIT_1;
    }

    procedure receiver()
        modifies st;
        modifies message2;
    {
        assume(st == RECEIVER_0 && message2 == CONTROL_BIT_0);
        st := SENDER_1;
        message2 := CONTROL_BIT_0;
    }

    procedure sender_resend()
        modifies st;
    {
        assume(st == SENDER_1 && message2 == CONTROL_BIT_0);
        st := RECEIVER_1;
    }

    procedure receiver_resend()
        modifies st;
    {
        assume(st == RECEIVER_1 && message2 == CONTROL_BIT_1);
        st := SENDER_0;
    }

    next {
        if st == SENDER_0 {
            sender();
        } else if st == RECEIVER_0 {
            receiver();
        } else if st == SENDER_1 {
            sender_resend();
        } else if st == RECEIVER_1 {
            receiver_resend();
        }
    }

    procedure check_acknowledgement()
    {
        if st == RECEIVER_0 && message1 == DATA_BIT && message2 == CONTROL_BIT_0 {
            ack := true;
        } else if st == RECEIVER_1 && message1 == DATA_BIT && message2 == CONTROL_BIT_1 {
            ack := true;
        } else {
            ack := false;
        }
    }

    control {
        check_acknowledgement();
        assert ack;
    }

}
