Added parsing of lola formulas and added an option

to detect deadlocks unless a formula is satisfied

src/Main.hs

@@ -23,9 +23,8 @@ import Solver.SComponent
 
 data InputFormat = PNET | LOLA | TPN deriving (Show,Read)
 
--- TODO: Change NoDeadlockOutOf to NoDeadlockUnless=FILE
 data ImplicitProperty = Termination
-                      | NoDeadlock | NoDeadlockOutOf String
+                      | NoDeadlock | NoDeadlockUnless String
                       | Safe | Bounded Integer
                       deriving (Show,Read)
 
@@ -72,12 +71,13 @@ options =
                }))
         "Prove that there is no deadlock"
 
-        , Option "" ["no-deadlock-out-of"]
+        , Option "" ["no-deadlock-unless"]
         (ReqArg (\arg opt -> Right opt {
-                           optProperties = NoDeadlockOutOf arg : optProperties opt
+                           optProperties = NoDeadlockUnless arg : optProperties opt
                 })
-                "PLACE")
-        "Prove that there is no deadlock unless PLACE is marked"
+                "FILE")
+        ("Prove that there is no deadlock unless the\n" ++
+         "formula given in FILE is satisfied")
 
         , Option "" ["safe"]
         (NoArg (\opt -> Right opt {
@@ -136,7 +136,7 @@ checkFile parser verbosity refine implicitProperties file = do
         verbosePut verbosity 2 $
                 "Places: " ++ show (length  $ places net) ++ "\n" ++
                 "Transitions: " ++ show (length $ transitions net)
-        let addedProperties = map (makeImplicitProperty net) implicitProperties
+        addedProperties <- mapM (makeImplicitProperty net) implicitProperties
         print properties
         rs <- mapM (checkProperty verbosity net refine)
                   (addedProperties ++ properties)
@@ -146,22 +146,26 @@ checkFile parser verbosity refine implicitProperties file = do
 placeOp :: Op -> (String, Integer) -> Formula
 placeOp op (p,w) = Atom $ LinIneq (Var p) op (Const w)
 
-makeImplicitProperty :: PetriNet -> ImplicitProperty -> Property
-makeImplicitProperty _ Termination = Property "termination" Liveness FTrue
+makeImplicitProperty :: PetriNet -> ImplicitProperty -> IO Property
+makeImplicitProperty _ Termination =
+        return $ Property "termination" Liveness FTrue
 makeImplicitProperty net NoDeadlock =
-        Property "no deadlock" Safety $
+        return $ Property "no deadlock" Safety $
             foldl (:&:) FTrue
                 (map (foldl (:|:) FFalse . map (placeOp Lt) . lpre net)
                      (transitions net))
-makeImplicitProperty net (NoDeadlockOutOf pl) =
-        Property ("no deadlock out of " ++ pl) Safety $
-            placeOp Lt (pl,1) :&: pformula (makeImplicitProperty net NoDeadlock)
+makeImplicitProperty net (NoDeadlockUnless file) = do
+        nodeadlock <- makeImplicitProperty net NoDeadlock
+        property <- parseFile LOLA.parseFormula file
+        return $ Property "no deadlock unless" Safety $
+            Neg property :&: pformula nodeadlock
 makeImplicitProperty net (Bounded k) =
-        Property (show k ++ "-bounded") Safety $
+        return $ Property (show k ++ "-bounded") Safety $
             foldl (:|:) FFalse
                 (map (\p -> placeOp Gt (p,k)) (places net))
-makeImplicitProperty net Safe =
-        Property "safe" Safety $ pformula (makeImplicitProperty net (Bounded 1))
+makeImplicitProperty net Safe = do
+        bounded <- makeImplicitProperty net (Bounded 1)
+        return $ Property "safe" Safety $ pformula bounded
 
 checkProperty :: Int -> PetriNet -> Bool -> Property -> IO Bool
 checkProperty verbosity net refine p = do

src/Parser/LOLA.hs

 module Parser.LOLA
-    (parseContent)
+    (module Parser.LOLAFormula,
+     parseContent)
 where
 
 import Control.Applicative ((*>),(<*))
@@ -8,6 +9,7 @@ import Text.Parsec.Language (LanguageDef, emptyDef)
 import qualified Text.Parsec.Token as Token
 
 import Parser
+import Parser.LOLAFormula
 import PetriNet (PetriNet,makePetriNetWithTrans)
 import Property
 

src/Parser/LOLAFormula.hs

+module Parser.LOLAFormula
+    (parseFormula)
+where
+
+import Control.Applicative ((*>),(<$>))
+import Data.Functor.Identity
+import Text.Parsec
+import Text.Parsec.Expr
+import Text.Parsec.Language (LanguageDef, emptyDef)
+import qualified Text.Parsec.Token as Token
+
+import Parser
+import Property
+
+languageDef :: LanguageDef ()
+languageDef =
+        emptyDef {
+                 Token.commentStart    = "{",
+                 Token.commentEnd      = "}",
+                 Token.commentLine     = "",
+                 Token.identStart      = noneOf ",;:(){}\t \n\r0123456789",
+                 Token.identLetter     = noneOf ",;:(){}\t \n\r0123456789",
+                 Token.reservedNames   = ["FORMULA", "TRUE", "FALSE",
+                                          "NOT", "AND", "OR"],
+                 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
+parens :: Parser a -> Parser a
+parens     = Token.parens     lexer -- parses p surrounded by parenthesis
+integer :: Parser Integer
+integer    = Token.integer    lexer -- parses an integer
+whiteSpace :: Parser ()
+whiteSpace = Token.whiteSpace lexer -- parses whitespace
+
+
+binary :: String -> (a -> a -> a) -> Assoc -> Operator String () Identity a
+binary name fun = Infix  ( reservedOp name *> return fun )
+prefix :: String -> (a -> a) -> Operator String () Identity a
+prefix name fun = Prefix ( reservedOp name *> return fun )
+
+termOperatorTable :: [[Operator String () Identity Term]]
+termOperatorTable =
+        [ [ prefix "-" Minus ]
+        , [ binary "*" (:*:) AssocLeft ]
+        , [ binary "+" (:+:) AssocLeft, binary "-" (:-:) AssocLeft ]
+        ]
+
+termAtom :: Parser Term
+termAtom =  (Var <$> identifier)
+        <|> (Const <$> integer)
+        <|> parens term
+        <?> "basic term"
+
+term :: Parser Term
+term = buildExpressionParser termOperatorTable termAtom <?> "term"
+
+parseOp :: Parser Op
+parseOp = (reservedOp "<" *> return Lt) <|>
+          (reservedOp "<=" *> return Le) <|>
+          (reservedOp "=" *> return Eq) <|>
+          (reservedOp "!=" *> return Ne) <|>
+          (reservedOp ">" *> return Gt) <|>
+          (reservedOp ">=" *> return Ge)
+
+linIneq :: Parser Formula
+linIneq = do
+        lhs <- term
+        op <- parseOp
+        rhs <- term
+        return (Atom (LinIneq lhs op rhs))
+
+binaryName :: String -> (a -> a -> a) -> Assoc -> Operator String () Identity a
+binaryName name fun = Infix  ( reserved name *> return fun )
+prefixName :: String -> (a -> a) -> Operator String () Identity a
+prefixName name fun = Prefix ( reserved name *> return fun )
+
+formOperatorTable :: [[Operator String () Identity Formula]]
+formOperatorTable =
+        [ [ prefixName "NOT" Neg ]
+        , [ binaryName "AND" (:&:) AssocRight ]
+        , [ binaryName "OR"  (:|:) AssocRight ]
+        ]
+
+formAtom :: Parser Formula
+formAtom =  try linIneq
+        <|> (reserved "TRUE" *> return FTrue)
+        <|> (reserved "FALSE" *> return FFalse)
+        <|> parens formula
+        <?> "basic formula"
+
+formula :: Parser Formula
+formula = buildExpressionParser formOperatorTable formAtom <?> "formula"
+
+parseFormula :: Parser Formula
+parseFormula = do
+        whiteSpace
+        reserved "FORMULA"
+        f <- formula
+        eof
+        return f