Property.hs 5.48 KB
Newer Older
1 2 3 4 5
{-# OPTIONS_GHC -fno-warn-name-shadowing #-}

module Property
    (Property(..),
     Formula(..),
6 7
     negationNormalForm,
     eliminateModulo,
8
     Op(..),
9 10 11 12
     Term(..),
     PropResult(..),
     resultAnd,
     resultOr,
13
     resultNot,
14 15
     resultsAnd,
     resultsOr)
16 17
where

18 19 20 21 22 23 24 25 26 27 28
data Term a =
          Var a
        | Const Integer
        | Minus (Term a)
        | Term a :+: Term a
        | Term a :-: Term a
        | Term a :*: Term a
        deriving (Eq)

instance (Show a) => Show (Term a) where
        show (Var x) = show x
29
        show (Const c) = show c
30 31 32 33
        show (Minus t) = "-" ++ show t
        show (t :+: u) = "(" ++ show t ++ " + " ++ show u ++ ")"
        show (t :-: u) = "(" ++ show t ++ " - " ++ show u ++ ")"
        show (t :*: u) = show t ++ " * " ++ show u
34

35 36 37 38 39 40 41
instance Functor Term where
        fmap f (Var x) = Var (f x)
        fmap _ (Const c) = Const c
        fmap f (Minus t) = Minus (fmap f t)
        fmap f (t :+: u) = fmap f t :+: fmap f u
        fmap f (t :-: u) = fmap f t :-: fmap f u
        fmap f (t :*: u) = fmap f t :*: fmap f u
42

43
data Op = Gt | Ge | Eq | Ne | Le | Lt | ModEq Integer | ModNe Integer deriving (Eq)
44 45 46

instance Show Op where
        show Gt = ">"
47
        show Ge = "≥"
48
        show Eq = "="
49
        show Ne = "≠"
50
        show Le = "≤"
51
        show Lt = "<"
52 53 54 55 56 57 58 59 60 61 62 63
        show (ModEq m) = "≡_" ++ show m
        show (ModNe m) = "≢_" ++ show m

negateOp :: Op -> Op
negateOp Gt = Le
negateOp Ge = Lt
negateOp Eq = Ne
negateOp Ne = Eq
negateOp Le = Gt
negateOp Lt = Ge
negateOp (ModEq m) = (ModNe m)
negateOp (ModNe m) = (ModEq m)
64

65 66
data Formula a =
          FTrue | FFalse
67
        | Equation (Term a) Op (Term a)
68 69 70
        | Neg (Formula a)
        | Formula a :&: Formula a
        | Formula a :|: Formula a
71
             deriving (Eq)
72 73 74 75

infixr 3 :&:
infixr 2 :|:

76 77 78 79 80
negationNormalForm :: Formula a -> Formula a
negationNormalForm (Neg (FTrue)) = FFalse
negationNormalForm (Neg (FFalse)) = FTrue
negationNormalForm (Neg (g :&: h)) = (negationNormalForm (Neg g)) :|: (negationNormalForm (Neg h))
negationNormalForm (Neg (g :|: h)) = (negationNormalForm (Neg g)) :&: (negationNormalForm (Neg h))
81
negationNormalForm (Neg (Equation u op t)) = Equation u (negateOp op) t
82
negationNormalForm (Neg (Neg g)) = negationNormalForm g
83 84
negationNormalForm (g :&: h) = (negationNormalForm g) :&: (negationNormalForm h)
negationNormalForm (g :|: h) = (negationNormalForm g) :|: (negationNormalForm h)
85
negationNormalForm f@(Equation _ _ _) = f
86 87
negationNormalForm FTrue = FTrue
negationNormalForm FFalse = FFalse
88

89 90 91 92 93
eliminateModulo :: (Int -> a) -> Formula a -> (Formula a, [a])
eliminateModulo = eliminateModulo' 0

eliminateModulo' :: Int -> (Int -> a) -> Formula a -> (Formula a, [a])
eliminateModulo' _ _ (Neg g) = error "Formula not in negation normal form: cannot eliminate modulo"
94
eliminateModulo' n makeVar (Equation lhs (ModEq m) rhs) =
95
        let k = makeVar n
96 97
        in  (Equation lhs Eq (rhs :+: ((Const m) :*: (Var k))), [k])
eliminateModulo' n makeVar (Equation lhs (ModNe m) rhs) =
98 99
        let j = makeVar (n + 1)
            k = makeVar n
100 101
        in  ((Equation lhs Eq (rhs :+: ((Var j) :+: ((Const m) :*: (Var k))))) :&:
            (Equation (Const 0) Lt (Var j)) :&: (Equation (Var j) Lt (Const m)), [k, j])
102 103 104 105 106 107 108 109 110 111
eliminateModulo' n makeVar (g :|: h) =
        let (g', ag) = eliminateModulo' n makeVar g
            (h', ah) = eliminateModulo' (n + length ag) makeVar h
        in  (g' :|: h', ag ++ ah)
eliminateModulo' n makeVar (g :&: h) =
        let (g', ag) = eliminateModulo' n makeVar g
            (h', ah) = eliminateModulo' (n + length ag) makeVar h
        in  (g' :&: h', ag ++ ah)
eliminateModulo' _ _ f = (f, [])

112
instance (Show a) => Show (Formula a) where
113 114
        show FTrue = "true"
        show FFalse = "false"
115
        show (Equation lhs op rhs) =
116
            show lhs ++ " " ++ show op ++ " " ++ show rhs
117
        show (Neg p) = "¬" ++ "(" ++ show p ++ ")"
118 119 120
        show (p :&: q) = "(" ++ show p ++ " ∧ " ++ show q ++ ")"
        show (p :|: q) = "(" ++ show p ++ " ∨ " ++ show q ++ ")"

121 122 123
instance Functor Formula where
        fmap _ FTrue = FTrue
        fmap _ FFalse = FFalse
124 125
        fmap f (Equation lhs op rhs) =
                Equation (fmap f lhs) op (fmap f rhs)
126 127 128
        fmap f (Neg p) = Neg (fmap f p)
        fmap f (p :&: q) = fmap f p :&: fmap f q
        fmap f (p :|: q) = fmap f p :|: fmap f q
129

130
data Property = LayeredTermination
131
              | StrongConsensus
132
              | StrongConsensusWithCorrectness
133

134 135 136
instance Show Property where
        show LayeredTermination = "layered termination"
        show StrongConsensus = "strong consensus"
137
        show StrongConsensusWithCorrectness = "strong consensus with correctness"
138

139
data PropResult = Satisfied | Unsatisfied | Unknown deriving (Eq)
140

141 142 143 144
instance Show PropResult where
        show Satisfied = "satisfied"
        show Unsatisfied = "not satisfied"
        show Unknown = "may not be satisfied"
145 146 147 148 149 150 151 152 153 154 155 156 157

resultAnd :: PropResult -> PropResult -> PropResult
resultAnd Satisfied x = x
resultAnd Unsatisfied _ = Unsatisfied
resultAnd _ Unsatisfied = Unsatisfied
resultAnd Unknown _ = Unknown

resultOr :: PropResult -> PropResult -> PropResult
resultOr Satisfied _ = Satisfied
resultOr _ Satisfied = Satisfied
resultOr Unsatisfied x = x
resultOr Unknown _ = Unknown

158 159 160 161 162
resultNot :: PropResult -> PropResult
resultNot Satisfied = Unsatisfied
resultNot Unsatisfied = Unsatisfied
resultNot Unknown = Unknown

163 164 165 166 167
resultsAnd :: [PropResult] -> PropResult
resultsAnd = foldr resultAnd Satisfied

resultsOr :: [PropResult] -> PropResult
resultsOr = foldr resultOr Unsatisfied