{-# LANGUAGE MultiParamTypeClasses #-}

import Yices.Painless.Language
import Prelude hiding (and)

main = print =<< solve p

data PC = Sleeping | Trying | Critical
    deriving (Show, Enum, Bounded)

class Y a b where
    lift :: a -> Exp b

instance Y PC Int where
    lift t = (fromIntegral (fromEnum t) :: Exp Int)

------------------------------------------------------------------------

p ::
    (Exp Int -> Exp Int) ->
    (Exp Int -> Exp Int) ->
    Exp Int -> Exp Int -> Exp Int ->
    Exp Int -> Exp Int -> Exp Int -> Exp Bool

p f g x1 x2 x3
      x4 x5 x6 =
         -- set the range
         and [ x >=* (lift (minBound :: PC)) &&*
               x <=* (lift (maxBound :: PC)) | x <- [x1,x2,x3,x4,x5,x6] ]
        &&*
         and [ x1 ==* x3
             , x3 ==* x2
             , g (f x1) /=* g (f x2) ]