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

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

module Property
    (Property(..),
5
     showPropertyName,
6
     renameProperty,
Philipp Meyer's avatar
Philipp Meyer committed
7
     PropertyType(..),
8
     PropertyContent(..),
9
     ConstraintProperty(..),
Philipp Meyer's avatar
Philipp Meyer committed
10 11
     Formula(..),
     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
import PopulationProtocol
22

23 24 25 26 27 28 29 30 31 32 33
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
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
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
data Op = Gt | Ge | Eq | Ne | Le | Lt deriving (Eq)
Philipp Meyer's avatar
Philipp Meyer committed
49 50 51

instance Show Op where
        show Gt = ">"
52
        show Ge = "≥"
Philipp Meyer's avatar
Philipp Meyer committed
53
        show Eq = "="
54
        show Ne = "≠"
55
        show Le = "≤"
Philipp Meyer's avatar
Philipp Meyer committed
56 57
        show Lt = "<"

58 59 60 61 62 63
data Formula a =
          FTrue | FFalse
        | LinearInequation (Term a) Op (Term a)
        | Neg (Formula a)
        | Formula a :&: Formula a
        | Formula a :|: Formula a
64
             deriving (Eq)
Philipp Meyer's avatar
Philipp Meyer committed
65 66 67 68

infixr 3 :&:
infixr 2 :|:

69
instance (Show a) => Show (Formula a) where
70 71
        show FTrue = "true"
        show FFalse = "false"
72 73
        show (LinearInequation lhs op rhs) =
            show lhs ++ " " ++ show op ++ " " ++ show rhs
74
        show (Neg p) = "¬" ++ "(" ++ show p ++ ")"
Philipp Meyer's avatar
Philipp Meyer committed
75 76 77
        show (p :&: q) = "(" ++ show p ++ " ∧ " ++ show q ++ ")"
        show (p :|: q) = "(" ++ show p ++ " ∨ " ++ show q ++ ")"

78 79 80 81 82 83 84 85
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
86

87 88
-- TODO: add functions to transform formula to CNF/DNF

89 90
data PropertyType = SafetyType
                  | LivenessType
91 92
                  | ConstraintType

93
data ConstraintProperty = TerminalMarkingsUniqueConsensusConstraint
94
                        | TerminalMarkingReachableConstraint
95

96
instance Show ConstraintProperty where
97
        show TerminalMarkingsUniqueConsensusConstraint = "reachable terminal markings have a unique consensus"
98
        show TerminalMarkingReachableConstraint = "terminal marking reachable"
99

100
data PropertyContent = Safety (Formula State)
101
                  | Liveness (Formula Transition)
102
                  | Constraint ConstraintProperty
Philipp Meyer's avatar
Philipp Meyer committed
103

104 105 106
showPropertyType :: PropertyContent -> String
showPropertyType (Safety _) = "safety"
showPropertyType (Liveness _) = "liveness"
107 108
showPropertyType (Constraint _) = "constraint"

109 110 111
showPropertyContent :: PropertyContent -> String
showPropertyContent (Safety f) = show f
showPropertyContent (Liveness f) = show f
112 113 114 115
showPropertyContent (Constraint c) = show c

instance Show PropertyContent where
        show pc = showPropertyType pc ++ " (" ++ showPropertyContent pc ++ ")"
Philipp Meyer's avatar
Philipp Meyer committed
116

117 118
data Property = Property {
        pname :: String,
119
        pcont :: PropertyContent
120
}
Philipp Meyer's avatar
Philipp Meyer committed
121 122

instance Show Property where
123
        show p =
124 125
            showPropertyName p ++
            " { " ++ showPropertyContent (pcont p) ++ " }"
Philipp Meyer's avatar
Philipp Meyer committed
126

127 128
renameProperty :: (String -> String) -> Property -> Property
renameProperty f (Property pn (Safety pf)) =
129
        Property pn (Safety (fmap (renameState f) pf))
130 131
renameProperty f (Property pn (Liveness pf)) =
        Property pn (Liveness (fmap (renameTransition f) pf))
132
renameProperty _ p = p
133

134
showPropertyName :: Property -> String
135
showPropertyName p = showPropertyType (pcont p) ++ " property" ++
136
               (if null (pname p) then "" else " " ++ show (pname p))
137

138
data PropResult = Satisfied | Unsatisfied | Unknown deriving (Show,Read,Eq)
139 140 141 142 143 144 145 146 147 148 149 150 151

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

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

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

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