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

Property.hs 5.04 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,
Philipp Meyer's avatar
Philipp Meyer committed
9
     Op(..),
10 11 12 13
     Term(..),
     PropResult(..),
     resultAnd,
     resultOr,
14
     resultNot,
15 16
     resultsAnd,
     resultsOr)
Philipp Meyer's avatar
Philipp Meyer committed
17 18
where

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

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

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

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

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

72 73 74
data QuantFormula a = ExQuantFormula [a] (Formula a)
             deriving (Eq)

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

infixr 3 :&:
infixr 2 :|:

86 87 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
negationNormalForm f = f

94 95 96 97 98 99 100 101 102 103
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

104
instance (Show a) => Show (Formula a) where
105 106
        show FTrue = "true"
        show FFalse = "false"
107 108
        show (LinearInequation lhs op rhs) =
            show lhs ++ " " ++ show op ++ " " ++ show rhs
109
        show (Neg p) = "¬" ++ "(" ++ show p ++ ")"
Philipp Meyer's avatar
Philipp Meyer committed
110 111 112
        show (p :&: q) = "(" ++ show p ++ " ∧ " ++ show q ++ ")"
        show (p :|: q) = "(" ++ show p ++ " ∨ " ++ show q ++ ")"

113 114 115
instance Functor QuantFormula where
        fmap f (ExQuantFormula xs p) = ExQuantFormula (fmap f xs) (fmap f p)

116 117 118 119 120 121 122 123
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
124

125
data Property = LayeredTermination
Philipp Meyer's avatar
Philipp Meyer committed
126
              | StrongConsensus
127
              | StrongConsensusWithCorrectness
Philipp Meyer's avatar
Philipp Meyer committed
128

Philipp Meyer's avatar
Philipp Meyer committed
129 130 131
instance Show Property where
        show LayeredTermination = "layered termination"
        show StrongConsensus = "strong consensus"
132
        show StrongConsensusWithCorrectness = "strong consensus with correctness"
Philipp Meyer's avatar
Philipp Meyer committed
133

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

Philipp Meyer's avatar
Philipp Meyer committed
136 137 138 139
instance Show PropResult where
        show Satisfied = "satisfied"
        show Unsatisfied = "not satisfied"
        show Unknown = "may not be satisfied"
140 141 142 143 144 145 146 147 148 149 150 151 152

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

153 154 155 156 157
resultNot :: PropResult -> PropResult
resultNot Satisfied = Unsatisfied
resultNot Unsatisfied = Unsatisfied
resultNot Unknown = Unknown

158 159 160 161 162
resultsAnd :: [PropResult] -> PropResult
resultsAnd = foldr resultAnd Satisfied

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