MIST.hs 4.44 KB
Newer Older
1
2
3
4
5
6
7
8
9
10
11
12
13
14
module Parser.MIST
    (parseContent)
where

import Control.Applicative ((<$>),(*>),(<*),(<*>))
import Control.Monad (when)
import Data.List (sortBy, groupBy)
import Data.Function (on)
import Data.Ord (comparing)
import Text.Parsec
import Text.Parsec.Language (LanguageDef, emptyDef)
import qualified Text.Parsec.Token as Token

import Parser
Philipp Meyer's avatar
Philipp Meyer committed
15
import PetriNet (PetriNet,makePetriNetWithTransFromStrings,Place(..))
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
import Property

languageDef :: LanguageDef ()
languageDef =
        emptyDef {
                 Token.commentStart    = "",
                 Token.commentEnd      = "",
                 Token.commentLine     = "#",
                 Token.identStart      = letter <|> char '_',
                 Token.identLetter     = alphaNum <|> oneOf "'_",
                 Token.reservedNames   = ["vars", "rules", "init",
                                          "target", "invariants"],
                 Token.reservedOpNames = ["->", "+", "-", "=", ">="]
                 }

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

identifier :: Parser String
identifier = Token.identifier lexer -- parses an identifier
reserved :: String -> Parser ()
reserved   = Token.reserved   lexer -- parses a reserved name
reservedOp :: String -> Parser ()
reservedOp = Token.reservedOp lexer -- parses an operator
integer :: Parser Integer
integer    = Token.integer    lexer -- parses an integer
semi :: Parser String
semi       = Token.semi       lexer -- parses a semicolon
commaSep :: Parser a -> Parser [a]
commaSep   = Token.commaSep   lexer -- parses a comma separated list
commaSep1 :: Parser a -> Parser [a]
commaSep1  = Token.commaSep1  lexer -- parses a comma separated list
whiteSpace :: Parser ()
whiteSpace = Token.whiteSpace lexer -- parses whitespace


net :: Parser PetriNet
net = do
        reserved "vars"
        ps <- many1 identifier
        reserved "rules"
        ts <- transitions
        reserved "init"
        (is,initTrans) <- initial
Philipp Meyer's avatar
Philipp Meyer committed
60
        return $ makePetriNetWithTransFromStrings "" ps (initTrans ++ ts) is
61
                 (map fst initTrans) [] [] [] []
62
63
64
65
66
67

prop :: Parser Property
prop = do
        reserved "target"
        ineqs <- many1 (commaSep1 ineq)
        _ <- optionMaybe (reserved "invariants" *> invariants)
68
        return $ Property "" $ Safety $
69
70
                    foldl1 (:|:) $ map (foldl1 (:&:)) ineqs

71
ineq :: Parser (Formula Place)
72
73
74
75
ineq = do
        x <- identifier
        reservedOp ">="
        c <- integer
76
        return $ LinearInequation (Var (Place x)) Ge (Const c)
77

Philipp Meyer's avatar
Philipp Meyer committed
78
transitions :: Parser [(String, ([(String, Integer)], [(String, Integer)]))]
79
80
transitions = do
        ts <- many1 transition
Philipp Meyer's avatar
Philipp Meyer committed
81
        return $ map (\(i,(l,r)) -> ("'t" ++ show i,(l,r)))
82
83
84
85
86
87
88
                        ([(1::Integer)..] `zip` ts)

transition :: Parser ([(String, Integer)], [(String, Integer)])
transition = do
        lhs <- commaSep ((,) <$> identifier <* reservedOp ">=" <*> integer)
        reservedOp "->"
        rhs <- commaSep transitionAssignment
89
        let rhs' = map (\xs -> (fst (head xs), sum (map snd xs))) $
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
                   groupBy ((==) `on` fst) $
                   sortBy (comparing fst) $
                   lhs ++ rhs
        _ <- semi
        return (lhs, rhs')

transitionAssignment :: Parser (String, Integer)
transitionAssignment = do
        i1 <- identifier
        reservedOp "="
        i2 <- identifier
        when (i1 /= i2 ++ "'")
            (error ("identifiers not equal: " ++ i1 ++ " /= " ++ i2))
        fac <- (reservedOp "-" *> return (-1)) <|> (reservedOp "+" *> return 1)
        n <- integer
        return (i2,fac*n)

initial :: Parser ([(String, Integer)],
Philipp Meyer's avatar
Philipp Meyer committed
108
                  [(String, ([(String, Integer)], [(String, Integer)]))])
109
110
111
112
initial = do
        xs <- commaSep1 initState
        let inits = [(x,i) | (x,i,_) <- xs]
        let covered = [x | (x,_,True) <- xs]
Philipp Meyer's avatar
Philipp Meyer committed
113
        let initTrans = map (\(i,x) -> ("'init" ++ show i, ([], [(x,1)])))
114
                            ([(1::Integer)..] `zip` covered)
115
        return (inits, initTrans)
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134

initState :: Parser (String, Integer, Bool)
initState = do
        s <- identifier
        cover <- reservedOp "=" *> return False <|>
                reservedOp ">=" *> return True
        i <- integer
        return (s,i,cover)

invariants :: Parser [[(String, Integer)]]
invariants = many1 (commaSep1 ((,) <$> identifier <* reservedOp "=" <*> integer))

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