(define-type pc (scalar sleeping trying critical))
(define f::(-> pc pc))
(define x1::pc)
(define x2::pc)
(define x3::pc)
(define x4::pc)
(define x5::pc)
(define x6::pc)
(define x7::pc)
(define x8::pc)

(assert (/= x1 x2))
(assert (= x1 x3))
(assert (= x3 x6))
(assert (= x2 x4))
(assert (= x4 x5))
(assert (= x4 x7))
(check)