24.09., 9:00 - 11:00: Due to updates GitLab will be unavailable for some minutes between 09:00 and 11:00.

Property.hs 6.39 KB
Newer Older
Philipp Meyer's avatar
Philipp Meyer committed
1 2 3 4 5
{-# OPTIONS_GHC -fno-warn-name-shadowing #-}

module Property
    (Property(..),
     Formula(..),
6 7 8
     QuantFormula(..),
     quantifiedVariables,
     innerFormula,
9 10
     negationNormalForm,
     eliminateModulo,
Philipp Meyer's avatar
Philipp Meyer committed
11
     Op(..),
12 13 14 15
     Term(..),
     PropResult(..),
     resultAnd,
     resultOr,
16
     resultNot,
17 18
     resultsAnd,
     resultsOr)
Philipp Meyer's avatar
Philipp Meyer committed
19 20
where

21 22 23 24 25 26 27
data Term a =
          Var a
        | Const Integer
        | Minus (Term a)
        | Term a :+: Term a
        | Term a :-: Term a
        | Term a :*: Term a
28 29
        | Term a :/: Term a -- integer division truncated toward negative infinity
        | Term a :%: Term a -- integer modulos, satisfying (x / y)*y + (x % y) = x
30 31 32 33
        deriving (Eq)

instance (Show a) => Show (Term a) where
        show (Var x) = show x
34
        show (Const c) = show c
35 36 37 38
        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
39 40
        show (t :/: u) = show t ++ " / " ++ show u
        show (t :%: u) = show t ++ " % " ++ show u
Philipp Meyer's avatar
Philipp Meyer committed
41

42 43 44 45 46 47 48
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
49 50
        fmap f (t :/: u) = fmap f t :/: fmap f u
        fmap f (t :%: u) = fmap f t :%: fmap f u
51

52
data Op = Gt | Ge | Eq | Ne | Le | Lt | ModEq Integer | ModNe Integer deriving (Eq)
Philipp Meyer's avatar
Philipp Meyer committed
53 54 55

instance Show Op where
        show Gt = ">"
56
        show Ge = "≥"
Philipp Meyer's avatar
Philipp Meyer committed
57
        show Eq = "="
58
        show Ne = "≠"
59
        show Le = "≤"
Philipp Meyer's avatar
Philipp Meyer committed
60
        show Lt = "<"
61 62 63 64 65 66 67 68 69 70 71 72
        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)
Philipp Meyer's avatar
Philipp Meyer committed
73

74 75 76
data QuantFormula a = ExQuantFormula [a] (Formula a)
             deriving (Eq)

77 78 79 80 81 82
data Formula a =
          FTrue | FFalse
        | LinearInequation (Term a) Op (Term a)
        | Neg (Formula a)
        | Formula a :&: Formula a
        | Formula a :|: Formula a
83
             deriving (Eq)
Philipp Meyer's avatar
Philipp Meyer committed
84 85 86 87

infixr 3 :&:
infixr 2 :|:

88 89 90 91 92 93
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))
negationNormalForm (Neg (LinearInequation u op t)) = LinearInequation u (negateOp op) t
94 95
negationNormalForm (g :&: h) = (negationNormalForm g) :&: (negationNormalForm h)
negationNormalForm (g :|: h) = (negationNormalForm g) :|: (negationNormalForm h)
96 97
negationNormalForm f = f

98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120
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"
eliminateModulo' n makeVar (LinearInequation lhs (ModEq m) rhs) =
        let k = makeVar n
        in  (LinearInequation lhs Eq (rhs :+: ((Const m) :*: (Var k))), [k])
eliminateModulo' n makeVar (LinearInequation lhs (ModNe m) rhs) =
        let j = makeVar (n + 1)
            k = makeVar n
        in  ((LinearInequation lhs Eq (rhs :+: ((Var j) :+: ((Const m) :*: (Var k))))) :&:
            (LinearInequation (Const 0) Lt (Var j)) :&: (LinearInequation (Var j) Lt (Const m)), [k, j])
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, [])

121 122 123 124 125 126 127 128 129 130
quantifiedVariables :: QuantFormula a -> [a]
quantifiedVariables (ExQuantFormula xs _) = xs

innerFormula :: QuantFormula a -> Formula a
innerFormula (ExQuantFormula _ p) = p

instance (Show a) => Show (QuantFormula a) where
        show (ExQuantFormula [] p) = show p
        show (ExQuantFormula ps p) = "∃" ++ unwords (map show ps) ++ ": " ++ show p

131
instance (Show a) => Show (Formula a) where
132 133
        show FTrue = "true"
        show FFalse = "false"
134 135
        show (LinearInequation lhs op rhs) =
            show lhs ++ " " ++ show op ++ " " ++ show rhs
136
        show (Neg p) = "¬" ++ "(" ++ show p ++ ")"
Philipp Meyer's avatar
Philipp Meyer committed
137 138 139
        show (p :&: q) = "(" ++ show p ++ " ∧ " ++ show q ++ ")"
        show (p :|: q) = "(" ++ show p ++ " ∨ " ++ show q ++ ")"

140 141 142
instance Functor QuantFormula where
        fmap f (ExQuantFormula xs p) = ExQuantFormula (fmap f xs) (fmap f p)

143 144 145 146 147 148 149 150
instance Functor Formula where
        fmap _ FTrue = FTrue
        fmap _ FFalse = FFalse
        fmap f (LinearInequation lhs op rhs) =
                LinearInequation (fmap f lhs) op (fmap f rhs)
        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
151

152
data Property = LayeredTermination
Philipp Meyer's avatar
Philipp Meyer committed
153
              | StrongConsensus
154
              | StrongConsensusWithCorrectness
Philipp Meyer's avatar
Philipp Meyer committed
155

Philipp Meyer's avatar
Philipp Meyer committed
156 157 158
instance Show Property where
        show LayeredTermination = "layered termination"
        show StrongConsensus = "strong consensus"
159
        show StrongConsensusWithCorrectness = "strong consensus with correctness"
Philipp Meyer's avatar
Philipp Meyer committed
160

Philipp Meyer's avatar
Philipp Meyer committed
161
data PropResult = Satisfied | Unsatisfied | Unknown deriving (Eq)
Philipp Meyer's avatar
Philipp Meyer committed
162

Philipp Meyer's avatar
Philipp Meyer committed
163 164 165 166
instance Show PropResult where
        show Satisfied = "satisfied"
        show Unsatisfied = "not satisfied"
        show Unknown = "may not be satisfied"
167 168 169 170 171 172 173 174 175 176 177 178 179

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

180 181 182 183 184
resultNot :: PropResult -> PropResult
resultNot Satisfied = Unsatisfied
resultNot Unsatisfied = Unsatisfied
resultNot Unknown = Unknown

185 186 187 188 189
resultsAnd :: [PropResult] -> PropResult
resultsAnd = foldr resultAnd Satisfied

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