11.3.2021, 9:00 - 11:00: Due to updates GitLab may be unavailable for some minutes between 09:00 and 11:00.

Commit b00594bd authored by Philipp Meyer's avatar Philipp Meyer

Added parser for tpn input files

parent d26cf842
place p1 init 1;
place p2;
place p3;
place b1;
place nb1 init 1;
place q1 init 1;
place q2;
place q3;
place q4;
place q5;
place b2;
place nb2 init 1;
trans s1 in p1 nb1 out p2 b1;
trans s2 in p2 b2 out p2 b2;
trans s3 in p2 nb2 out p3 nb2;
trans s4 in p3 b1 out p1 nb1;
trans t1 in q1 nb2 out q2 b2;
trans t2 in q2 b1 out q3 b1;
trans t3 in q3 b2 out q4 nb2;
trans t4 in q4 nb1 out q1 nb1;
trans t5 in q4 b1 out q4 b1;
trans t6 in q2 nb1 out q5 nb1;
trans t7 in q5 b2 out q1 nb2;
......@@ -12,6 +12,7 @@ import Data.Char (toUpper)
import Parser
import qualified Parser.PNET as PNET
import qualified Parser.TPN as TPN
import PetriNet
import Property
import Solver
......@@ -152,7 +153,7 @@ main = do
let parser = case inputFormat opts of
PNET -> PNET.parseContent
LOLA -> error "lola is not supported yet"
TPN -> error "tpn is not supported yet"
TPN -> TPN.parseContent
let properties = [ Property "termination" Liveness FTrue
| proveTermination opts ]
rs <- mapM (checkFile parser (optVerbose opts) properties) files
......
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, [])
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