Notice to GitKraken users: A vulnerability has been found in the SSH key generation of GitKraken versions 7.6.0 to 8.0.0 (https://www.gitkraken.com/blog/weak-ssh-key-fix). If you use GitKraken and have generated a SSH key using one of these versions, please remove it both from your local workstation and from your LRZ GitLab profile.

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

Property.hs 4.92 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 PetriNet
22
23
import Structure

24
25
26
27
28
29
30
31
32
33
34
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
35
        show (Const c) = show c
36
37
38
39
        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
40

41
42
43
44
45
46
47
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
48

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

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

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

infixr 3 :&:
infixr 2 :|:

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

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

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

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

data ConstraintProperty = UniqueTerminalMarkingConstraint
96
                        | NonConsensusStateConstraint
97

98
99
instance Show ConstraintProperty where
        show UniqueTerminalMarkingConstraint = "unique terminal marking"
100
        show NonConsensusStateConstraint = "non-consensus state"
101

102
103
data PropertyContent = Safety (Formula Place)
                  | Liveness (Formula Transition)
104
                  | Structural Structure
105
                  | Constraint ConstraintProperty
Philipp Meyer's avatar
Philipp Meyer committed
106

107
108
109
110
showPropertyType :: PropertyContent -> String
showPropertyType (Safety _) = "safety"
showPropertyType (Liveness _) = "liveness"
showPropertyType (Structural _) = "structural"
111
112
showPropertyType (Constraint _) = "constraint"

113
114
115
116
showPropertyContent :: PropertyContent -> String
showPropertyContent (Safety f) = show f
showPropertyContent (Liveness f) = show f
showPropertyContent (Structural s) = show s
117
118
119
120
showPropertyContent (Constraint c) = show c

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

122
123
data Property = Property {
        pname :: String,
124
        pcont :: PropertyContent
125
}
Philipp Meyer's avatar
Philipp Meyer committed
126
127

instance Show Property where
128
        show p =
129
130
            showPropertyName p ++
            " { " ++ showPropertyContent (pcont p) ++ " }"
Philipp Meyer's avatar
Philipp Meyer committed
131

132
133
134
135
136
renameProperty :: (String -> String) -> Property -> Property
renameProperty f (Property pn (Safety pf)) =
        Property pn (Safety (fmap (renamePlace f) pf))
renameProperty f (Property pn (Liveness pf)) =
        Property pn (Liveness (fmap (renameTransition f) pf))
137
renameProperty _ p = p
138

139
showPropertyName :: Property -> String
140
showPropertyName p = showPropertyType (pcont p) ++ " property" ++
141
               (if null (pname p) then "" else " " ++ show (pname p))
142

143
data PropResult = Satisfied | Unsatisfied | Unknown deriving (Show,Read,Eq)
144
145
146
147
148
149
150
151
152
153
154
155
156

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

157
158
159
160
161
resultNot :: PropResult -> PropResult
resultNot Satisfied = Unsatisfied
resultNot Unsatisfied = Unsatisfied
resultNot Unknown = Unknown

162
163
164
165
166
resultsAnd :: [PropResult] -> PropResult
resultsAnd = foldr resultAnd Satisfied

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