**diff options**

Diffstat (limited to 'tests/examples/ex3.hs')

-rw-r--r-- | tests/examples/ex3.hs | 38 |

1 files changed, 38 insertions, 0 deletions

diff --git a/tests/examples/ex3.hs b/tests/examples/ex3.hs new file mode 100644 index 0000000..886f8f9 --- /dev/null +++ b/tests/examples/ex3.hs @@ -0,0 +1,38 @@ +{-# 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)) +-} |