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

Property.hs 2.05 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,
Philipp Meyer's avatar
Philipp Meyer committed
6 7 8 9
     PropertyType(..),
     Formula(..),
     LinearInequation(..),
     Op(..),
10
     Term(..))
Philipp Meyer's avatar
Philipp Meyer committed
11 12
where

13 14 15 16 17 18
data Term = Var String
          | Const Integer
          | Minus Term
          | Term :+: Term
          | Term :-: Term
          | Term :*: Term
Philipp Meyer's avatar
Philipp Meyer committed
19 20

instance Show Term where
21 22
        show (Var x) = x
        show (Const c) = show c
23 24 25 26
        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
27

28
data Op = Gt | Ge | Eq | Ne | Le | Lt
Philipp Meyer's avatar
Philipp Meyer committed
29 30 31

instance Show Op where
        show Gt = ">"
32
        show Ge = "≥"
Philipp Meyer's avatar
Philipp Meyer committed
33
        show Eq = "="
34
        show Ne = "≠"
35
        show Le = "≤"
Philipp Meyer's avatar
Philipp Meyer committed
36 37
        show Lt = "<"

38
-- TODO: merge LinIneq constructor into Formula
Philipp Meyer's avatar
Philipp Meyer committed
39 40 41 42 43
data LinearInequation = LinIneq Term Op Term

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

44 45
data Formula = FTrue | FFalse
             | Atom LinearInequation
Philipp Meyer's avatar
Philipp Meyer committed
46 47 48 49 50 51 52 53
             | Neg Formula
             | Formula :&: Formula
             | Formula :|: Formula

infixr 3 :&:
infixr 2 :|:

instance Show Formula where
54 55
        show FTrue = "true"
        show FFalse = "false"
Philipp Meyer's avatar
Philipp Meyer committed
56
        show (Atom a) = show a
57
        show (Neg p) = "¬" ++ "(" ++ show p ++ ")"
Philipp Meyer's avatar
Philipp Meyer committed
58 59 60 61 62 63 64 65 66
        show (p :&: q) = "(" ++ show p ++ " ∧ " ++ show q ++ ")"
        show (p :|: q) = "(" ++ show p ++ " ∨ " ++ show q ++ ")"

data PropertyType = Safety | Liveness

instance Show PropertyType where
        show Safety = "safety"
        show Liveness = "liveness"

67 68 69 70 71
data Property = Property {
        pname :: String,
        ptype :: PropertyType,
        pformula :: Formula
}
Philipp Meyer's avatar
Philipp Meyer committed
72 73

instance Show Property where
74
        show p =
75
            showPropertyName p ++ " { " ++ show (pformula p) ++ " }"
Philipp Meyer's avatar
Philipp Meyer committed
76

77
showPropertyName :: Property -> String
78
showPropertyName p = show (ptype p) ++ " property" ++
79
               (if null (pname p) then "" else " " ++ show (pname p))