Extended parser and grammar to allow more liberal terms

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

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 =

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 = "<"
 

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 = (.<)