(set-logic ALL)

(declare-fun st () Int)
(declare-fun message1 () Bool)
(declare-fun message2 () Bool)
(declare-fun ack () Bool)

(define-fun property1 () Bool
    (=> (and (= st 0) message1) ack)
)

(define-fun property2 () Bool
    (=> (and (= st 1) message2) ack)
)

(define-fun property3 () Bool
    (=> (and (= ack true) (= st 0)) message2)
)

(define-fun property4 () Bool
    (=> (and (= ack true) (= st 1)) message1)
)

(assert (forall ((st Int) (message1 Bool) (message2 Bool) (ack Bool))
    (and (property1) (property2) (property3) (property4))
))

(check-sat)
```

This code defines the variables st, message1, message2, and ack, and then defines four properties to check that the model implements the alternating bit protocol correctly. The properties ensure that the sender sends the correct message based on the control bit, the receiver acknowledges the correct message, and both sender and receiver handle unexpected messages appropriately. Finally, it asserts that all four properties hold for all possible values of the variables and checks the satisfiability of the model.