(define-type pc (scalar sleeping trying critical))
(define x1::pc)
(define x2::pc)
(define z1::pc)
(define z2::pc)
(define w1::pc)
(define w2::pc)

(assert (= x1 x2))
(assert (= x1 z1))
(assert (= x2 critical))
(assert (= x2 z2))
(assert (= z2 w1))
(assert (= x1 trying))