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

Property.hs 1.68 KB
Newer Older
Philipp Meyer's avatar
Philipp Meyer committed
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31
{-# OPTIONS_GHC -fno-warn-name-shadowing #-}

module Property
    (Property(..),
     PropertyType(..),
     Formula(..),
     LinearInequation(..),
     Op(..),
     Term(..),
     LinAtom(..))
where

import Data.List (intercalate)

data LinAtom = Var Integer String | Const Integer

instance Show LinAtom where
        show (Var c x) | c == 1 = x
        show (Var c x) | c == -1 = "-" ++ x
        show (Var c x) = show c ++ "*" ++ x
        show (Const c) = show c

data Term = Term [LinAtom]

instance Show Term where
        show (Term xs) = intercalate " + " (map show xs)

data Op = Gt | Ge | Eq | Le | Lt

instance Show Op where
        show Gt = ">"
32
        show Ge = "≥"
Philipp Meyer's avatar
Philipp Meyer committed
33
        show Eq = "="
34
        show Le = "≤"
Philipp Meyer's avatar
Philipp Meyer committed
35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64
        show Lt = "<"

data LinearInequation = LinIneq Term Op Term

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

data Formula = Atom LinearInequation
             | Neg Formula
             | Formula :&: Formula
             | Formula :|: Formula

infixr 3 :&:
infixr 2 :|:

instance Show Formula where
        show (Atom a) = show a
        show (Neg p) = "¬" ++ show p
        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"

data Property = Property String PropertyType Formula

instance Show Property where
65 66 67 68
        show (Property name ptype formula) =
            show ptype ++ " property " ++
            (if null name then "" else show name ++ " ") ++
            "{ " ++ show formula ++ " }"
Philipp Meyer's avatar
Philipp Meyer committed
69