
(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 (= st 0)) message2)
)

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

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

(check-sat)