PNET.hs 6.14 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
13
14
15
16
17
18
19
20
21
22
23
import Text.Parsec.Language (LanguageDef, emptyDef)
import qualified Text.Parsec.Token as Token

import Parser
import PetriNet (PetriNet,makePetriNet)
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
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
                                          "+", "-", "*", "&&", "||", "!"]
                 }

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)
          )

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] |
                 Arcs [(String,String,Integer)] | Initial [(String,Integer)]

statement :: Parser Statement
statement = Places <$> places <|>
            Transitions <$> transitions <|>
            Arcs <$> arcs <|>
            Initial <$> initial

petriNet :: Parser PetriNet
petriNet = do
            reserved "petri"
            reserved "net"
            name <- option "" ident
            statements <- braces (many statement)
            let (p,t,a,i) = foldl splitStatement ([],[],[],[]) statements
            return $ makePetriNet name p t a i
        where
            splitStatement (ps,ts,as,is) stmnt = case stmnt of
                  Places p -> (p ++ ps,ts,as,is)
                  Transitions t -> (ps,t ++ ts,as,is)
                  Arcs a -> (ps,ts,a ++ as,is)
                  Initial i -> (ps,ts,as,i ++ is)

127
128
129
130
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 )
131

132
133
134
135
136
137
138
139
140
141
142
termOperatorTable :: [[Operator String () Identity Term]]
termOperatorTable =
        [ [ prefix "-" Minus ]
        , [ binary "*" (:*:) AssocLeft ]
        , [ binary "+" (:+:) AssocLeft, binary "-" (:-:) AssocLeft ]
        ]

termAtom :: Parser Term
termAtom =  parens term
        <|> (Const <$> integer)
        <|> (Var <$> ident)
143
144

term :: Parser Term
145
term = buildExpressionParser termOperatorTable termAtom <?> "term"
146
147
148
149
150

parseOp :: Parser Op
parseOp = (reservedOp "<" *> return Lt) <|>
          (reservedOp "<=" *> return Le) <|>
          (reservedOp "=" *> return Eq) <|>
151
          (reservedOp "!=" *> return Ne) <|>
152
153
154
          (reservedOp ">" *> return Gt) <|>
          (reservedOp ">=" *> return Ge)

155
156
linIneq :: Parser Formula
linIneq = do
157
158
159
160
161
        lhs <- term
        op <- parseOp
        rhs <- term
        return (Atom (LinIneq lhs op rhs))

162
163
164
165
166
167
formOperatorTable :: [[Operator String () Identity Formula]]
formOperatorTable =
        [ [ prefix "!" Neg ]
        , [ binary "&&" (:&:) AssocRight ]
        , [ binary "||" (:|:) AssocRight ]
        ]
168

169
170
171
172
173
formAtom :: Parser Formula
formAtom =  parens formula
        <|> (reserved "true" *> return FTrue)
        <|> (reserved "false" *> return FFalse)
        <|> linIneq
174
175

formula :: Parser Formula
176
formula = buildExpressionParser formOperatorTable formAtom <?> "formula"
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197

propertyType :: Parser PropertyType
propertyType =
        (reserved "safety" *> return Safety) <|>
        (reserved "liveness" *> return Liveness)

property :: Parser Property
property = do
        pt <- propertyType
        reserved "property"
        name <- option "" ident
        form <- braces formula
        return Property { pname=name, ptype=pt, pformula=form }

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