Added parser for lola input

examples/lamport.lola

+PLACE
+    p1, p2, p3,         b1, nb1,
+    q1, q2, q3, q4, q5, b2, nb2;
+
+MARKING
+    p1, q1, nb1, nb2;
+
+TRANSITION s1
+    CONSUME p1, nb1;
+    PRODUCE p2,  b1;
+
+TRANSITION s2
+    CONSUME p2,  b2;
+    PRODUCE p2,  b2;
+
+TRANSITION s3
+    CONSUME p2, nb2;
+    PRODUCE p3, nb2;
+
+TRANSITION s4
+    CONSUME p3,  b1;
+    PRODUCE p1, nb1;
+
+TRANSITION t1
+    CONSUME q1, nb2;
+    PRODUCE q2,  b2;
+
+TRANSITION t2
+    CONSUME q2,  b1;
+    PRODUCE q3,  b1;
+
+TRANSITION t3
+    CONSUME q3,  b2;
+    PRODUCE q4, nb2;
+
+TRANSITION t4
+    CONSUME q4, nb1;
+    PRODUCE q1, nb1;
+
+TRANSITION t5
+    CONSUME q4,  b1;
+    PRODUCE q4,  b1;
+
+TRANSITION t6
+    CONSUME q2, nb1;
+    PRODUCE q5, nb1;
+
+TRANSITION t7
+    CONSUME q5,  b2;
+    PRODUCE q1, nb2;

src/Main.hs

@@ -11,6 +11,7 @@ import Control.Applicative
 
 import Parser
 import qualified Parser.PNET as PNET
+import qualified Parser.LOLA as LOLA
 import qualified Parser.TPN as TPN
 import PetriNet
 import Property
@@ -83,6 +84,7 @@ checkFile parser verbose addedProperties file = do
         (net,properties) <- parseFile parser file
         putStrLn $ "Analyzing " ++ showNetName net
         when verbose (do
+                print net
                 putStrLn $ "Places: " ++ show (length  $ places net)
                 putStrLn $ "Transitions: " ++ show (length $ transitions net)
             )
@@ -154,7 +156,7 @@ main = do
                 when (null files) (exitErrorWith "No input file given")
                 let parser = case inputFormat opts of
                                  PNET -> PNET.parseContent
-                                 LOLA -> error "lola is not supported yet"
+                                 LOLA -> LOLA.parseContent
                                  TPN -> TPN.parseContent
                 let properties = [ Property "termination" Liveness FTrue
                                  | proveTermination opts ]

src/Parser/LOLA.hs

+module Parser.LOLA
+    (parseContent)
+where
+
+import Control.Applicative ((*>),(<*))
+import Text.Parsec
+import Text.Parsec.Language (LanguageDef, emptyDef)
+import qualified Text.Parsec.Token as Token
+
+import Parser
+import PetriNet (PetriNet,makePetriNetWithTrans)
+import Property
+
+languageDef :: LanguageDef ()
+languageDef =
+        emptyDef {
+                 Token.commentStart    = "{",
+                 Token.commentEnd      = "}",
+                 Token.commentLine     = "",
+                 Token.identStart      = noneOf ",;:(){}\t \n\r",
+                 Token.identLetter     = noneOf ",;:(){}\t \n\r",
+                 Token.reservedNames   = ["PLACE", "MARKING", "SAFE",
+                                          "TRANSITION", "CONSUME", "PRODUCE",
+                                          "STRONG", "WEAK", "FAIR"],
+                 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
+integer :: Parser Integer
+integer    = Token.integer    lexer -- parses an integer
+colon :: Parser String
+colon      = Token.colon      lexer -- parses a colon
+semi :: Parser String
+semi       = Token.semi       lexer -- parses a semicolon
+commaSep1 :: Parser a -> Parser [a]
+commaSep1  = Token.commaSep1  lexer -- parses a comma separated list
+whiteSpace :: Parser ()
+whiteSpace = Token.whiteSpace lexer -- parses whitespace
+
+
+ident :: Parser String
+ident = (identifier <|> fmap show integer) <?> "identifier"
+
+net :: Parser PetriNet
+net = do
+        reserved "PLACE"
+        ps <- placeLists
+        reserved "MARKING"
+        initial <- option [] markingList
+        _ <- semi
+        ts <- many1 transition
+        return $ makePetriNetWithTrans "" ps ts initial
+
+placeLists :: Parser [String]
+placeLists =
+        fmap concat (many1 (do
+            _ <- optionMaybe (reserved "SAFE" *> option 1 integer <* colon)
+            ps <- placeList
+            _ <- semi
+            return ps
+        ))
+
+placeList :: Parser [String]
+placeList = commaSep1 ident
+
+markingList :: Parser [(String, Integer)]
+markingList = commaSep1 marking
+
+marking :: Parser (String, Integer)
+marking = do
+        s <- ident
+        i <- option 1 (colon *> integer)
+        return (s, i)
+
+transition :: Parser (String, [(String, Integer)], [(String, Integer)])
+transition = do
+        reserved "TRANSITION"
+        t <- ident
+        _ <- optionMaybe ((reserved "STRONG" <|> reserved "WEAK") <*
+                          reserved "FAIR")
+        reserved "CONSUME"
+        input <- option [] arcList
+        _ <- semi
+        reserved "PRODUCE"
+        output <- option [] arcList
+        _ <- semi
+        return (t, input, output)
+
+arcList :: Parser [(String, Integer)]
+arcList = commaSep1 arc
+
+arc :: Parser (String, Integer)
+arc = do
+        x <- ident
+        w <- option 1 (colon *> integer)
+        return (x, w)
+
+parseContent :: Parser (PetriNet,[Property])
+parseContent = do
+        whiteSpace
+        n <- net
+        eof
+        return (n, [])

src/Parser/TPN.hs

@@ -10,7 +10,7 @@ import qualified Text.Parsec.Token as Token
 import Data.List (group,sort,genericLength)
 
 import Parser
-import PetriNet (PetriNet,makePetriNet)
+import PetriNet (PetriNet,makePetriNetWithTrans)
 import Property
 
 languageDef :: LanguageDef ()
@@ -40,7 +40,7 @@ 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ü
+semi       = Token.semi       lexer -- parses a semicolon
 whiteSpace :: Parser ()
 whiteSpace = Token.whiteSpace lexer -- parses whitespace
 
@@ -76,11 +76,8 @@ 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
+        return $ makePetriNetWithTrans "" places ts initial
 
 parseContent :: Parser (PetriNet,[Property])
 parseContent = do

src/PetriNet.hs

@@ -3,7 +3,7 @@
 module PetriNet
     (PetriNet,showNetName,places,transitions,initial,
      pre,lpre,post,lpost,initials,
-     makePetriNet)
+     makePetriNet,makePetriNetWithTrans)
 where
 
 import qualified Data.Map as M
@@ -68,3 +68,11 @@ makePetriNet name places transitions arcs initial =
               in  m''
             addArc (lNew,rNew) (lOld,rOld) = (lNew ++ lOld,rNew ++ rOld)
 
+makePetriNetWithTrans :: String -> [String] ->
+        [(String, [(String, Integer)], [(String, Integer)])] ->
+        [(String, Integer)] -> PetriNet
+makePetriNetWithTrans name places ts initial =
+        let transitions = [ t | (t,_,_) <- ts ]
+            arcs = [ (i,t,w) | (t,is,_) <- ts, (i,w) <- is ] ++
+                   [ (t,o,w) | (t,_,os) <- ts, (o,w) <- os ]
+        in  makePetriNet name places transitions arcs initial