Commit dda24412 authored by Philipp Meyer's avatar Philipp Meyer
Browse files

Small changes to property and formula syntax

parent d262f8ac
...@@ -5,9 +5,13 @@ import System.Environment (getArgs) ...@@ -5,9 +5,13 @@ import System.Environment (getArgs)
import Parser (parseFile) import Parser (parseFile)
import PetriNet import PetriNet
import Property import Property
import Solver
checkProperty :: PetriNet -> Property -> Bool checkProperty :: PetriNet -> Property -> IO String
checkProperty net p = True checkProperty net p = do
r <- checkSat net p
return (if r then "Property not satisfied"
else "Property satisfied")
main :: IO () main :: IO ()
main = do main = do
...@@ -19,6 +23,7 @@ main = do ...@@ -19,6 +23,7 @@ main = do
putStrLn $ "Analyzing " ++ showName net putStrLn $ "Analyzing " ++ showName net
mapM_ (\p -> do mapM_ (\p -> do
putStrLn $ "Checking " ++ show p putStrLn $ "Checking " ++ show p
putStrLn $ show $ checkProperty net p r <- checkProperty net p
putStrLn r
) properties ) properties
...@@ -22,7 +22,7 @@ languageDef = ...@@ -22,7 +22,7 @@ languageDef =
Token.identLetter = alphaNum <|> char '_', Token.identLetter = alphaNum <|> char '_',
Token.reservedNames = [], Token.reservedNames = [],
Token.reservedOpNames = ["->", "<", "<=", "=", ">=", ">", Token.reservedOpNames = ["->", "<", "<=", "=", ">=", ">",
"+", "-", "*", "&", "|", "!"] "+", "-", "*", "&&", "||", "!"]
} }
lexer :: Token.TokenParser u lexer :: Token.TokenParser u
...@@ -158,12 +158,12 @@ negation = (Neg <$> (reservedOp "!" *> negation)) <|> parensForm ...@@ -158,12 +158,12 @@ negation = (Neg <$> (reservedOp "!" *> negation)) <|> parensForm
conjunction :: Parser u Formula conjunction :: Parser u Formula
conjunction = do conjunction = do
lhs <- negation lhs <- negation
option lhs ((lhs :&:) <$> (reservedOp "&" *> conjunction)) option lhs ((lhs :&:) <$> (reservedOp "&&" *> conjunction))
disjunction :: Parser u Formula disjunction :: Parser u Formula
disjunction = do disjunction = do
lhs <- conjunction lhs <- conjunction
option lhs ((lhs :|:) <$> (reservedOp "|" *> disjunction)) option lhs ((lhs :|:) <$> (reservedOp "||" *> disjunction))
formula :: Parser u Formula formula :: Parser u Formula
formula = disjunction formula = disjunction
...@@ -175,11 +175,11 @@ propertyType = ...@@ -175,11 +175,11 @@ propertyType =
property :: Parser u Property property :: Parser u Property
property = do property = do
ptype <- propertyType pt <- propertyType
reserved "property" reserved "property"
name <- option "" ident name <- option "" ident
pformulas <- braces formula form <- braces formula
return $ Property name ptype pformulas return Property { pname=name, ptype=pt, pformula=form }
parseContent :: Parser u (PetriNet,[Property]) parseContent :: Parser u (PetriNet,[Property])
parseContent = do parseContent = do
......
...@@ -49,7 +49,7 @@ infixr 2 :|: ...@@ -49,7 +49,7 @@ infixr 2 :|:
instance Show Formula where instance Show Formula where
show (Atom a) = show a show (Atom a) = show a
show (Neg p) = "¬" ++ show p show (Neg p) = "¬" ++ "(" ++ show p ++ ")"
show (p :&: q) = "(" ++ show p ++ " ∧ " ++ show q ++ ")" show (p :&: q) = "(" ++ show p ++ " ∧ " ++ show q ++ ")"
show (p :|: q) = "(" ++ show p ++ " ∨ " ++ show q ++ ")" show (p :|: q) = "(" ++ show p ++ " ∨ " ++ show q ++ ")"
...@@ -59,11 +59,15 @@ instance Show PropertyType where ...@@ -59,11 +59,15 @@ instance Show PropertyType where
show Safety = "safety" show Safety = "safety"
show Liveness = "liveness" show Liveness = "liveness"
data Property = Property String PropertyType Formula data Property = Property {
pname :: String,
ptype :: PropertyType,
pformula :: Formula
}
instance Show Property where instance Show Property where
show (Property name ptype formula) = show p =
show ptype ++ " property " ++ show (ptype p) ++ " property " ++
(if null name then "" else show name ++ " ") ++ (if null (pname p) then "" else show (pname p) ++ " ") ++
"{ " ++ show formula ++ " }" "{ " ++ show (pformula p) ++ " }"
...@@ -48,9 +48,9 @@ buildModel net = do ...@@ -48,9 +48,9 @@ buildModel net = do
return $ M.fromList (vars `zip` syms) return $ M.fromList (vars `zip` syms)
checkConstraints :: PetriNet -> Property -> Symbolic SBool checkConstraints :: PetriNet -> Property -> Symbolic SBool
checkConstraints net (Property _ _ f) = do checkConstraints net p = do
model <- buildModel net model <- buildModel net
evaluateFormula model f evaluateFormula model (pformula p)
checkSat :: PetriNet -> Property -> IO Bool checkSat :: PetriNet -> Property -> IO Bool
checkSat net p = do checkSat net p = do
......
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