{-# LANGUAGE ScopedTypeVariables #-}
import Yices.Painless.Language
import Prelude hiding (and)
main = print =<< solve p
-- Currently, need to derive Int, then translate in and out.
data PC = Sleeping | Trying | Critical
deriving (Show, Enum)
p x1 x2 z1 z2 (w1 :: Exp Int) (w2 :: Exp Int) =
and
[ x1 ==* x2
, x1 ==* z1
, x2 ==* fromIntegral (fromEnum Critical)
, x2 ==* z2
, x2 ==* w1
, x1 ==* fromIntegral (fromEnum Trying)
]
{-
-- (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))
-}