Commit 177c0295 authored by Philipp Meyer's avatar Philipp Meyer

Added parser for petri nets

parent 8f4f526f
......@@ -19,7 +19,9 @@ source-repository head
executable slapnet
main-is: Main.hs
-- other-modules:
other-modules:
PetriNet
Parser
-- other-extensions:
build-depends: base >=4.6 && <4.7, sbv, parsec
hs-source-dirs: src
......
module Main where
import System.Environment (getArgs)
import Parser (parseFile)
main :: IO ()
main = putStrLn "Safety and Liveness Analysis of Petri Nets with SMT solvers"
main = do
args <- getArgs
putStrLn "Safety and Liveness Analysis of Petri Nets with SMT solvers"
let file = head args
net <- parseFile file
print net
module Parser
(parseString, parseFile)
where
import Control.Applicative ((<*))
import Control.Monad (liftM)
import Text.Parsec
import Text.Parsec.Language (LanguageDef, emptyDef)
import qualified Text.Parsec.Token as Token
import PetriNet (PetriNet,makePetriNet)
type Parser u a = Parsec String u a
languageDef :: LanguageDef u
languageDef =
emptyDef {
Token.commentStart = "/*",
Token.commentEnd = "*/",
Token.commentLine = "//",
Token.identStart = letter <|> char '_',
Token.identLetter = alphaNum <|> char '_',
Token.reservedNames = [],
Token.reservedOpNames = ["->", "<", "<=", "=", ">=", ">",
"+", "-", "*", "&", "|", "!"]
}
lexer :: Token.TokenParser u
lexer = Token.makeTokenParser languageDef
identifier :: Parser u String
identifier = Token.identifier lexer -- parses an identifier
stringLiteral :: Parser u String
stringLiteral = Token.stringLiteral lexer -- parses a string literal
reserved :: String -> Parser u ()
reserved = Token.reserved lexer -- parses a reserved name
reservedOp :: String -> Parser u ()
reservedOp = Token.reservedOp lexer -- parses an operator
brackets :: Parser u a -> Parser u a
brackets = Token.brackets lexer -- parses p surrounded by brackets
braces :: Parser u a -> Parser u a
braces = Token.braces lexer -- parses p surrounded by braces
natural :: Parser u Integer
natural = Token.natural lexer -- parses a natural number
comma :: Parser u String
comma = Token.comma lexer -- parses a comma
whiteSpace :: Parser u ()
whiteSpace = Token.whiteSpace lexer -- parses whitespace
optionalCommaSep :: Parser u a -> Parser u [a]
optionalCommaSep p = many (p <* optional comma)
singleOrList :: Parser u a -> Parser u [a]
singleOrList p = braces (optionalCommaSep p) <|> liftM (:[]) p
numberOption :: Parser u Integer
numberOption = option 1 (brackets natural)
ident :: Parser u String
ident = (identifier <|> stringLiteral) <?> "identifier"
identList :: Parser u [String]
identList = singleOrList ident
places :: Parser u [String]
places = reserved "places" >> identList
transitions :: Parser u [String]
transitions = reserved "transitions" >> identList
initial :: Parser u [(String,Integer)]
initial = reserved "initial" >> singleOrList (do
n <- ident
i <- numberOption
return (n,i)
)
arc :: Parser u [(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 u [(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 u Statement
statement = liftM Places places <|>
liftM Transitions transitions <|>
liftM Arcs arcs <|>
liftM Initial initial
petriNet :: Parser u PetriNet
petriNet = do
whiteSpace
reserved "petri"
reserved "net"
name <- option "" ident
statements <- braces (many statement)
eof
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)
parseString :: String -> PetriNet
parseString str =
case parse petriNet "" str of
Left e -> error $ show e
Right r -> r
parseFile :: String -> IO PetriNet
parseFile file = do
contents <- readFile file
case parse petriNet file contents of
Left e -> print e >> fail "parse error"
Right r -> return r
{-# OPTIONS_GHC -fno-warn-name-shadowing #-}
module PetriNet
(PetriNet,name,places,transitions,
makePetriNet)
where
data PetriNet = PetriNet {
name :: String,
places :: [String],
transitions :: [String],
arcs :: [(String,String,Integer)],
initial :: [(String,Integer)]
}
instance Show PetriNet where
show net = "Petri net " ++ name net ++ "\n" ++
"Places: " ++ unwords (places net) ++ "\n" ++
"Transitions: " ++ unwords (transitions net) ++ "\n" ++
"Arcs:\n" ++ unlines
(map (\(l,r,w) -> l ++ " ->" ++
(if w /= 1 then "[" ++ show w ++ "]" else []) ++
" " ++ r)
(arcs net)) ++
"Initial: " ++ unwords
(map (\(n,i) -> n ++
(if i /= 1 then "[" ++ show i ++ "]" else []))
(initial net))
makePetriNet :: String -> [String] -> [String] ->
[(String, String,Integer)] -> [(String, Integer)] -> PetriNet
makePetriNet name places transitions arcs initial =
PetriNet { name=name, places=places, transitions=transitions,
arcs=arcs, initial=initial }
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment