From 1cca0e05370c783be51461c33eeccc12ee0be4c0 Mon Sep 17 00:00:00 2001 From: Philipp Meyer Date: Wed, 9 Jul 2014 15:06:42 +0200 Subject: [PATCH] Extended parser and grammar to allow more liberal terms --- src/Main.hs | 3 +- src/Parser/PNET.hs | 64 ++++++++++++++++++++++--------------------- src/Property.hs | 30 ++++++++++---------- src/Solver/Formula.hs | 10 +++++-- 4 files changed, 57 insertions(+), 50 deletions(-) diff --git a/src/Main.hs b/src/Main.hs index d833f5ef..74d2e3c5 100644 --- a/src/Main.hs +++ b/src/Main.hs @@ -137,13 +137,14 @@ checkFile parser verbosity refine implicitProperties file = do "Places: " ++ show (length $ places net) ++ "\n" ++ "Transitions: " ++ show (length $ transitions net) let addedProperties = map (makeImplicitProperty net) implicitProperties + print properties rs <- mapM (checkProperty verbosity net refine) (addedProperties ++ properties) verbosePut verbosity 0 "" return $ and rs placeOp :: Op -> (String, Integer) -> Formula -placeOp op (p,w) = Atom $ LinIneq (Term [Var 1 p]) op (Term [Const w]) +placeOp op (p,w) = Atom $ LinIneq (Var p) op (Const w) makeImplicitProperty :: PetriNet -> ImplicitProperty -> Property makeImplicitProperty _ Termination = Property "termination" Liveness FTrue diff --git a/src/Parser/PNET.hs b/src/Parser/PNET.hs index 35534d35..cac51e11 100644 --- a/src/Parser/PNET.hs +++ b/src/Parser/PNET.hs @@ -2,8 +2,10 @@ module Parser.PNET (parseContent) where -import Control.Applicative ((<*),(*>),(<*>),(<$>)) +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 @@ -20,7 +22,7 @@ languageDef = Token.identStart = letter <|> char '_', Token.identLetter = alphaNum <|> char '_', Token.reservedNames = ["true", "false"], - Token.reservedOpNames = ["->", "<", "<=", "=", ">=", ">", + Token.reservedOpNames = ["->", "<", "<=", "=", "!=", ">=", ">", "+", "-", "*", "&&", "||", "!"] } @@ -122,23 +124,31 @@ petriNet = do Arcs a -> (ps,ts,a ++ as,is) Initial i -> (ps,ts,as,i ++ is) -preFactor :: Parser Integer -preFactor = (reservedOp "-" *> return (-1)) <|> - (reservedOp "+" *> return 1) +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 ) -linAtom :: Integer -> Parser LinAtom -linAtom fac = ( integer >>= \lhs -> - option (Const (fac*lhs)) $ Var (fac*lhs) <$> (reservedOp "*" *> ident) - ) <|> Var fac <$> ident +termOperatorTable :: [[Operator String () Identity Term]] +termOperatorTable = + [ [ prefix "-" Minus ] + , [ binary "*" (:*:) AssocLeft ] + , [ binary "+" (:+:) AssocLeft, binary "-" (:-:) AssocLeft ] + ] + +termAtom :: Parser Term +termAtom = parens term + <|> (Const <$> integer) + <|> (Var <$> ident) term :: Parser Term -term = Term <$> ((:) <$> (option 1 preFactor >>= linAtom) <*> - many (preFactor >>= linAtom)) +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) @@ -149,29 +159,21 @@ linIneq = do rhs <- term return (Atom (LinIneq lhs op rhs)) -atom :: Parser Formula -atom = (reserved "true" *> return FTrue) <|> - (reserved "false" *> return FFalse) <|> - linIneq - -parensForm :: Parser Formula -parensForm = atom <|> parens formula - -negation :: Parser Formula -negation = (Neg <$> (reservedOp "!" *> negation)) <|> parensForm - -conjunction :: Parser Formula -conjunction = do - lhs <- negation - option lhs ((lhs :&:) <$> (reservedOp "&&" *> conjunction)) +formOperatorTable :: [[Operator String () Identity Formula]] +formOperatorTable = + [ [ prefix "!" Neg ] + , [ binary "&&" (:&:) AssocRight ] + , [ binary "||" (:|:) AssocRight ] + ] -disjunction :: Parser Formula -disjunction = do - lhs <- conjunction - option lhs ((lhs :|:) <$> (reservedOp "||" *> disjunction)) +formAtom :: Parser Formula +formAtom = parens formula + <|> (reserved "true" *> return FTrue) + <|> (reserved "false" *> return FFalse) + <|> linIneq formula :: Parser Formula -formula = disjunction +formula = buildExpressionParser formOperatorTable formAtom "formula" propertyType :: Parser PropertyType propertyType = diff --git a/src/Property.hs b/src/Property.hs index 8cdc6142..b63eba02 100644 --- a/src/Property.hs +++ b/src/Property.hs @@ -7,31 +7,31 @@ module Property Formula(..), LinearInequation(..), Op(..), - Term(..), - LinAtom(..)) + Term(..)) where -import Data.List (intercalate) - -data LinAtom = Var Integer String | Const Integer - -instance Show LinAtom where - show (Var c x) | c == 1 = x - show (Var c x) | c == -1 = "-" ++ x - show (Var c x) = show c ++ "*" ++ x - show (Const c) = show c - -data Term = Term [LinAtom] +data Term = Var String + | Const Integer + | Minus Term + | Term :+: Term + | Term :-: Term + | Term :*: Term instance Show Term where - show (Term xs) = intercalate " + " (map show xs) + show (Var x) = x + show (Const c) = show c + show (Minus t) = "-(" ++ show t ++ ")" + show (t :+: u) = show t ++ " + " ++ show u + show (t :-: u) = show t ++ " - " ++ show u + show (t :*: u) = "(" ++ show t ++ ") * (" ++ show u ++ ")" -data Op = Gt | Ge | Eq | Le | Lt +data Op = Gt | Ge | Eq | Ne | Le | Lt instance Show Op where show Gt = ">" show Ge = "≥" show Eq = "=" + show Ne = "≠" show Le = "≤" show Lt = "<" diff --git a/src/Solver/Formula.hs b/src/Solver/Formula.hs index ca552fc9..1fb4c578 100644 --- a/src/Solver/Formula.hs +++ b/src/Solver/Formula.hs @@ -8,14 +8,18 @@ import Property import Solver evaluateTerm :: Term -> ModelSI -> SInteger -evaluateTerm (Term xs) m = sum $ map evaluateLinAtom xs - where evaluateLinAtom (Var c x) = literal c * mVal m x - evaluateLinAtom (Const c) = literal c +evaluateTerm (Var x) m = mVal m x +evaluateTerm (Const c) _ = literal c +evaluateTerm (Minus t) m = - evaluateTerm t m +evaluateTerm (t :+: u) m = evaluateTerm t m + evaluateTerm u m +evaluateTerm (t :-: u) m = evaluateTerm t m - evaluateTerm u m +evaluateTerm (t :*: u) m = evaluateTerm t m * evaluateTerm u m opToFunction :: Op -> SInteger -> SInteger -> SBool opToFunction Gt = (.>) opToFunction Ge = (.>=) opToFunction Eq = (.==) +opToFunction Ne = (./=) opToFunction Le = (.<=) opToFunction Lt = (.<) -- GitLab