Main.hs 803 Bytes
Newer Older
1
2
module Main where

Philipp Meyer's avatar
Philipp Meyer committed
3
4
5
import System.Environment (getArgs)

import Parser (parseFile)
6
7
import PetriNet
import Property
8
import Solver
9

10
11
12
13
14
checkProperty :: PetriNet -> Property -> IO String
checkProperty net p = do
        r <- checkSat net p
        return (if r then "Property not satisfied"
                     else "Property satisfied")
Philipp Meyer's avatar
Philipp Meyer committed
15

16
main :: IO ()
Philipp Meyer's avatar
Philipp Meyer committed
17
18
19
main = do
        args <- getArgs
        let file = head args
20
21
22
        putStrLn "Safety and Liveness Analysis of Petri Nets with SMT solvers"
        putStrLn $ "Reading \"" ++ file ++ "\""
        (net,properties) <- parseFile file
23
        putStrLn $ "Analyzing " ++ showName net
24
25
        mapM_ (\p -> do
                  putStrLn $ "Checking " ++ show p
26
27
                  r <- checkProperty net p
                  putStrLn r
28
              ) properties
Philipp Meyer's avatar
Philipp Meyer committed
29