PNET.hs 7.73 KB
Newer Older
1
2
3
4
module Parser.PNET
    (parseContent)
where

5
6
import Control.Applicative ((<*),(*>),(<$>))
import Data.Functor.Identity
7
import Text.Parsec
8
import Text.Parsec.Expr
9
10
11
12
import Text.Parsec.Language (LanguageDef, emptyDef)
import qualified Text.Parsec.Token as Token

import Parser
Philipp Meyer's avatar
Philipp Meyer committed
13
import PetriNet (PetriNet,makePetriNetFromStrings,Place(..),Transition(..))
14
15
16
17
18
19
20
21
22
23
import Property

languageDef :: LanguageDef ()
languageDef =
        emptyDef {
                 Token.commentStart    = "/*",
                 Token.commentEnd      = "*/",
                 Token.commentLine     = "//",
                 Token.identStart      = letter <|> char '_',
                 Token.identLetter     = alphaNum <|> char '_',
24
                 Token.reservedNames   = ["true", "false"],
25
                 Token.reservedOpNames = ["->", "<", "<=", "=", "!=", ">=", ">",
26
27
28
29
30
31
32
33
34
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
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
                                          "+", "-", "*", "&&", "||", "!"]
                 }

lexer :: Token.TokenParser ()
lexer = Token.makeTokenParser languageDef

identifier :: Parser String
identifier = Token.identifier lexer -- parses an identifier
stringLiteral :: Parser String
stringLiteral = Token.stringLiteral lexer -- parses a string literal
reserved :: String -> Parser ()
reserved   = Token.reserved   lexer -- parses a reserved name
reservedOp :: String -> Parser ()
reservedOp = Token.reservedOp lexer -- parses an operator
brackets :: Parser a -> Parser a
brackets   = Token.brackets   lexer -- parses p surrounded by brackets
braces :: Parser a -> Parser a
braces     = Token.braces     lexer -- parses p surrounded by braces
parens :: Parser a -> Parser a
parens     = Token.parens     lexer -- parses p surrounded by parenthesis
natural :: Parser Integer
natural    = Token.natural    lexer -- parses a natural number
integer :: Parser Integer
integer    = Token.integer    lexer -- parses an integer
comma :: Parser String
comma      = Token.comma       lexer -- parses a comma
whiteSpace :: Parser ()
whiteSpace = Token.whiteSpace lexer -- parses whitespace


optionalCommaSep :: Parser a -> Parser [a]
optionalCommaSep p = many (p <* optional comma)

singleOrList :: Parser a -> Parser [a]
singleOrList p = braces (optionalCommaSep p) <|> (:[]) <$> p

numberOption :: Parser Integer
numberOption = option 1 (brackets natural)

ident :: Parser String
ident = (identifier <|> stringLiteral) <?> "identifier"

identList :: Parser [String]
identList = singleOrList ident

places :: Parser [String]
places = reserved "places" *> identList

transitions :: Parser [String]
transitions = reserved "transitions" *> identList

initial :: Parser [(String,Integer)]
initial = reserved "initial" *> singleOrList (do
            n <- ident
            i <- numberOption
            return (n,i)
          )

84
85
86
87
88
89
trap :: Parser [String]
trap = reserved "trap" *> identList

siphon :: Parser [String]
siphon = reserved "siphon" *> identList

90
91
92
93
94
95
yesStates :: Parser [String]
yesStates = reserved "yes" *> identList

noStates :: Parser [String]
noStates = reserved "no" *> identList

96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
arc :: Parser [(String,String,Integer)]
arc = do
        lhs <- identList
        rhsList <- many1 (do
                reservedOp "->"
                w <- numberOption
                ids <- identList
                return (ids,w)
            )
        return $ fst $ foldl makeArc ([],lhs) rhsList
      where
        makeArc (as,lhs) (rhs,w) = ([(l,r,w) | l <- lhs, r <- rhs] ++ as, rhs)

arcs :: Parser [(String,String,Integer)]
arcs = do
        reserved "arcs"
        as <- singleOrList arc
        return $ concat as

data Statement = Places [String] | Transitions [String] |
116
                 Arcs [(String,String,Integer)] | Initial [(String,Integer)] |
117
118
                 TrapStatement [String] | SiphonStatement [String] |
                 YesStatement [String] | NoStatement [String]
119
120
121
122
123

statement :: Parser Statement
statement = Places <$> places <|>
            Transitions <$> transitions <|>
            Arcs <$> arcs <|>
124
125
            Initial <$> initial <|>
            TrapStatement <$> trap <|>
126
127
128
            SiphonStatement <$> siphon <|>
            YesStatement <$> yesStates <|>
            NoStatement <$> noStates
129
130
131
132
133
134
135

petriNet :: Parser PetriNet
petriNet = do
            reserved "petri"
            reserved "net"
            name <- option "" ident
            statements <- braces (many statement)
136
137
            let (p,t,a,i,traps,siphons,yesStates,noStates) = foldl splitStatement ([],[],[],[],[],[],[],[]) statements
            return $ makePetriNetFromStrings name p t a i [] traps siphons yesStates noStates
138
        where
139
140
141
142
143
144
145
146
147
            splitStatement (ps,ts,as,is,traps,siphons,ys,ns) stmnt = case stmnt of
                  Places p -> (p ++ ps,ts,as,is,traps,siphons,ys,ns)
                  Transitions t -> (ps,t ++ ts,as,is,traps,siphons,ys,ns)
                  Arcs a -> (ps,ts,a ++ as,is,traps,siphons,ys,ns)
                  Initial i -> (ps,ts,as,i ++ is,traps,siphons,ys,ns)
                  TrapStatement trap -> (ps,ts,as,is,trap:traps,siphons,ys,ns)
                  SiphonStatement siphon -> (ps,ts,as,is,traps,siphon:siphons,ys,ns)
                  YesStatement y -> (ps,ts,as,is,traps,siphons,y ++ ys,ns)
                  NoStatement n -> (ps,ts,as,is,traps,siphons,ys,n ++ ns)
148

149
150
151
152
binary :: String -> (a -> a -> a) -> Assoc -> Operator String () Identity a
binary name fun = Infix  ( reservedOp name *> return fun )
prefix :: String -> (a -> a) -> Operator String () Identity a
prefix name fun = Prefix ( reservedOp name *> return fun )
153

154
termOperatorTable :: [[Operator String () Identity (Term String)]]
155
156
157
158
159
160
termOperatorTable =
        [ [ prefix "-" Minus ]
        , [ binary "*" (:*:) AssocLeft ]
        , [ binary "+" (:+:) AssocLeft, binary "-" (:-:) AssocLeft ]
        ]

161
termAtom :: Parser (Term String)
162
termAtom =  (Var <$> ident)
163
        <|> (Const <$> integer)
164
165
        <|> parens term
        <?> "basic term"
166

167
term :: Parser (Term String)
168
term = buildExpressionParser termOperatorTable termAtom <?> "term"
169
170
171
172
173

parseOp :: Parser Op
parseOp = (reservedOp "<" *> return Lt) <|>
          (reservedOp "<=" *> return Le) <|>
          (reservedOp "=" *> return Eq) <|>
174
          (reservedOp "!=" *> return Ne) <|>
175
176
177
          (reservedOp ">" *> return Gt) <|>
          (reservedOp ">=" *> return Ge)

178
linIneq :: Parser (Formula String)
179
linIneq = do
180
181
182
        lhs <- term
        op <- parseOp
        rhs <- term
183
        return (LinearInequation lhs op rhs)
184

185
formOperatorTable :: [[Operator String () Identity (Formula String)]]
186
187
188
189
190
formOperatorTable =
        [ [ prefix "!" Neg ]
        , [ binary "&&" (:&:) AssocRight ]
        , [ binary "||" (:|:) AssocRight ]
        ]
191

192
formAtom :: Parser (Formula String)
193
formAtom =  try linIneq
194
195
        <|> (reserved "true" *> return FTrue)
        <|> (reserved "false" *> return FFalse)
196
197
        <|> parens formula
        <?> "basic formula"
198

199
formula :: Parser (Formula String)
200
formula = buildExpressionParser formOperatorTable formAtom <?> "formula"
201
202
203

propertyType :: Parser PropertyType
propertyType =
204
205
206
207
        (reserved "safety" *> return SafetyType) <|>
        (reserved "liveness" *> return LivenessType) <|>
        (reserved "structural" *> return StructuralType)

208
209
210
211
212
213

property :: Parser Property
property = do
        pt <- propertyType
        reserved "property"
        name <- option "" ident
214
215
216
        case pt of
            SafetyType -> do
                form <- braces formula
217
218
                return Property
                    { pname=name, pcont=Safety (fmap Place form) }
219
220
            LivenessType -> do
                form <- braces formula
221
                return Property { pname=name, pcont=Liveness (fmap Transition form) }
222
            StructuralType -> error "structural property not supported for pnet"
223
224
225
226
227
228
229
230

parseContent :: Parser (PetriNet,[Property])
parseContent = do
        whiteSpace
        net <- petriNet
        properties <- many property
        eof
        return (net, properties)