TPN.hs 2.85 KB
Newer Older
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
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
module Parser.TPN
    (parseContent)
where

import Control.Applicative ((*>))
import Control.Arrow ((&&&))
import Text.Parsec
import Text.Parsec.Language (LanguageDef, emptyDef)
import qualified Text.Parsec.Token as Token
import Data.List (group,sort,genericLength)

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 '_',
                 Token.reservedNames   = ["place", "trans", "init",
                                          "in", "out"],
                 Token.reservedOpNames = ["~"]
                 }

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
natural :: Parser Integer
natural    = Token.natural    lexer -- parses a natural number
semi :: Parser String
semi       = Token.semi       lexer -- parses a semicolonü
whiteSpace :: Parser ()
whiteSpace = Token.whiteSpace lexer -- parses whitespace


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

place :: Parser (String, Maybe Integer)
place = do
        reserved "place"
        p <- ident
        initial <- optionMaybe (reserved "init" *> natural)
        _ <- semi
        return (p, initial)

adjacencyList :: Parser [(String, Integer)]
adjacencyList = do
        xs <- many1 ident
        return $ map (head &&& genericLength) $ group $ sort xs

transition :: Parser (String, [(String, Integer)], [(String, Integer)])
transition = do
        reserved "trans"
        t <- ident
        _ <- optionMaybe (reservedOp "~" *> ident)
        input <- option [] (reserved "in" *> adjacencyList)
        output <- option [] (reserved "out" *> adjacencyList)
        _ <- semi
        return (t, input, output)

petriNet :: Parser PetriNet
petriNet = do
        ps <- many place
        ts <- many transition
        let places = [ p | (p,_) <- ps ]
            transitions = [ t | (t,_,_) <- ts ]
            initial = [ (p,i) | (p,Just i) <- ps ]
            arcs = [ (i,t,w) | (t,is,_) <- ts, (i,w) <- is ] ++
                   [ (t,o,w) | (t,_,os) <- ts, (o,w) <- os ]
        return $ makePetriNet "" places transitions arcs initial

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