yices-painless-0.1.1: tests/examples/ex3.hs

{-# 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))
-}