summaryrefslogtreecommitdiff
path: root/tests/examples/ex3.hs
blob: 886f8f983b6bdd6860c1d12dfe861bbb2f0bc194 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
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))
-}