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