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

Added output of input file in main

parent c4a94af6
...@@ -3,12 +3,22 @@ module Main where ...@@ -3,12 +3,22 @@ module Main where
import System.Environment (getArgs) import System.Environment (getArgs)
import Parser (parseFile) import Parser (parseFile)
import PetriNet
import Property
checkProperty :: PetriNet -> Property -> Bool
checkProperty net p = True
main :: IO () main :: IO ()
main = do main = do
args <- getArgs args <- getArgs
putStrLn "Safety and Liveness Analysis of Petri Nets with SMT solvers"
let file = head args let file = head args
net <- parseFile file putStrLn "Safety and Liveness Analysis of Petri Nets with SMT solvers"
print net putStrLn $ "Reading \"" ++ file ++ "\""
(net,properties) <- parseFile file
putStrLn $ "Analyzing " ++ show net
mapM_ (\p -> do
putStrLn $ "Checking " ++ show p
putStrLn $ show $ checkProperty net p
) properties
...@@ -14,10 +14,11 @@ data PetriNet = PetriNet { ...@@ -14,10 +14,11 @@ data PetriNet = PetriNet {
} }
instance Show PetriNet where instance Show PetriNet where
show net = "Petri net " ++ name net ++ "\n" ++ show net = "Petri net" ++
"Places: " ++ unwords (places net) ++ "\n" ++ (if null (name net) then "" else " " ++ show (name net)) ++
"Transitions: " ++ unwords (transitions net) ++ "\n" ++ "\nPlaces: " ++ unwords (places net) ++
"Arcs:\n" ++ unlines "\nTransitions: " ++ unwords (transitions net) ++
"\nArcs:\n" ++ unlines
(map (\(l,r,w) -> l ++ " ->" ++ (map (\(l,r,w) -> l ++ " ->" ++
(if w /= 1 then "[" ++ show w ++ "]" else []) ++ (if w /= 1 then "[" ++ show w ++ "]" else []) ++
" " ++ r) " " ++ r)
......
...@@ -29,9 +29,9 @@ data Op = Gt | Ge | Eq | Le | Lt ...@@ -29,9 +29,9 @@ data Op = Gt | Ge | Eq | Le | Lt
instance Show Op where instance Show Op where
show Gt = ">" show Gt = ">"
show Ge = ">=" show Ge = ""
show Eq = "=" show Eq = "="
show Le = "<=" show Le = ""
show Lt = "<" show Lt = "<"
data LinearInequation = LinIneq Term Op Term data LinearInequation = LinIneq Term Op Term
...@@ -62,6 +62,8 @@ instance Show PropertyType where ...@@ -62,6 +62,8 @@ instance Show PropertyType where
data Property = Property String PropertyType Formula data Property = Property String PropertyType Formula
instance Show Property where instance Show Property where
show (Property name ptype formula) = show ptype ++ " " ++ show name ++ show (Property name ptype formula) =
" { " ++ show formula ++ " }" show ptype ++ " property " ++
(if null name then "" else show name ++ " ") ++
"{ " ++ show formula ++ " }"
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