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

Property.hs 4.31 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
     rename,
Philipp Meyer's avatar
Philipp Meyer committed
7
     PropertyType(..),
8
     PropertyContent(..),
Philipp Meyer's avatar
Philipp Meyer committed
9 10 11
     Formula(..),
     LinearInequation(..),
     Op(..),
12 13 14 15 16 17
     Term(..),
     PropResult(..),
     resultAnd,
     resultOr,
     resultsAnd,
     resultsOr)
Philipp Meyer's avatar
Philipp Meyer committed
18 19
where

20 21
import Structure

22 23 24 25 26 27
data Term = Var String
          | Const Integer
          | Minus Term
          | Term :+: Term
          | Term :-: Term
          | Term :*: Term
Philipp Meyer's avatar
Philipp Meyer committed
28 29

instance Show Term where
30 31
        show (Var x) = x
        show (Const c) = show c
32 33 34 35
        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
36

37 38 39 40 41 42 43 44
renameTerm :: (String -> String) -> Term -> Term
renameTerm f (Var x) = Var (f x)
renameTerm _ (Const c) = Const c
renameTerm f (Minus t) = Minus (renameTerm f t)
renameTerm f (t :+: u) = renameTerm f t :+: renameTerm f u
renameTerm f (t :-: u) = renameTerm f t :-: renameTerm f u
renameTerm f (t :*: u) = renameTerm f t :*: renameTerm f u

45
data Op = Gt | Ge | Eq | Ne | Le | Lt
Philipp Meyer's avatar
Philipp Meyer committed
46 47 48

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

55
-- TODO: merge LinIneq constructor into Formula
Philipp Meyer's avatar
Philipp Meyer committed
56 57 58 59 60
data LinearInequation = LinIneq Term Op Term

instance Show LinearInequation where
        show (LinIneq lhs op rhs) = show lhs ++ " " ++ show op ++ " " ++ show rhs

61 62 63 64
renameLinIneq :: (String -> String) -> LinearInequation -> LinearInequation
renameLinIneq f (LinIneq lhs op rhs) =
        LinIneq (renameTerm f lhs) op (renameTerm f rhs)

65 66
data Formula = FTrue | FFalse
             | Atom LinearInequation
Philipp Meyer's avatar
Philipp Meyer committed
67 68 69 70 71 72 73 74
             | Neg Formula
             | Formula :&: Formula
             | Formula :|: Formula

infixr 3 :&:
infixr 2 :|:

instance Show Formula where
75 76
        show FTrue = "true"
        show FFalse = "false"
Philipp Meyer's avatar
Philipp Meyer committed
77
        show (Atom a) = show a
78
        show (Neg p) = "¬" ++ "(" ++ show p ++ ")"
Philipp Meyer's avatar
Philipp Meyer committed
79 80 81
        show (p :&: q) = "(" ++ show p ++ " ∧ " ++ show q ++ ")"
        show (p :|: q) = "(" ++ show p ++ " ∨ " ++ show q ++ ")"

82 83 84 85 86 87 88 89
renameFormula :: (String -> String) -> Formula -> Formula
renameFormula _ FTrue = FTrue
renameFormula _ FFalse = FFalse
renameFormula f (Atom a) = Atom (renameLinIneq f a)
renameFormula f (Neg p) = Neg (renameFormula f p)
renameFormula f (p :&: q) = renameFormula f p :&: renameFormula f q
renameFormula f (p :|: q) = renameFormula f p :|: renameFormula f q

90 91 92 93 94 95 96
data PropertyType = SafetyType
                  | LivenessType
                  | StructuralType

data PropertyContent = Safety Formula
                  | Liveness Formula
                  | Structural Structure
Philipp Meyer's avatar
Philipp Meyer committed
97

98 99 100 101 102 103 104 105 106
showPropertyType :: PropertyContent -> String
showPropertyType (Safety _) = "safety"
showPropertyType (Liveness _) = "liveness"
showPropertyType (Structural _) = "structural"

showPropertyContent :: PropertyContent -> String
showPropertyContent (Safety f) = show f
showPropertyContent (Liveness f) = show f
showPropertyContent (Structural s) = show s
Philipp Meyer's avatar
Philipp Meyer committed
107

108 109
data Property = Property {
        pname :: String,
110
        pcont :: PropertyContent
111
}
Philipp Meyer's avatar
Philipp Meyer committed
112 113

instance Show Property where
114
        show p =
115 116
            showPropertyName p ++
            " { " ++ showPropertyContent (pcont p) ++ " }"
Philipp Meyer's avatar
Philipp Meyer committed
117

118
rename :: (String -> String) -> Property -> Property
119 120 121
rename f (Property pn (Safety pf)) = Property pn (Safety (renameFormula f pf))
rename f (Property pn (Liveness pf)) = Property pn (Liveness (renameFormula f pf))
rename _ (Property pn (Structural pc)) = Property pn (Structural pc)
122

123
showPropertyName :: Property -> String
124
showPropertyName p = showPropertyType (pcont p) ++ " property" ++
125
               (if null (pname p) then "" else " " ++ show (pname p))
126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145

data PropResult = Satisfied | Unsatisfied | Unknown

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

resultsAnd :: [PropResult] -> PropResult
resultsAnd = foldr resultAnd Satisfied

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